theorem Frourio.mulHaar_apply (s : Set ℝ) (hs : MeasurableSet s) : mulHaar s = ∫⁻ (x : ℝ) in s ∩ Set.Ioi 0, ENNReal.ofReal (1 / x)

noncomputable instance Frourio.instNormedAddCommGroupSubtypeAEEqFunRealComplexWithDensityMulHaarOfRealHPowHSubHMulOfNatMemAddSubgroupHσ (σ : ℝ) : NormedAddCommGroup ↥(Hσ σ)

Equations

• Frourio.instNormedAddCommGroupSubtypeAEEqFunRealComplexWithDensityMulHaarOfRealHPowHSubHMulOfNatMemAddSubgroupHσ σ = inferInstance

noncomputable instance Frourio.instNormedSpaceComplexSubtypeAEEqFunRealWithDensityMulHaarOfRealHPowHSubHMulOfNatMemAddSubgroupHσ (σ : ℝ) : NormedSpace ℂ ↥(Hσ σ)

Equations

• Frourio.instNormedSpaceComplexSubtypeAEEqFunRealWithDensityMulHaarOfRealHPowHSubHMulOfNatMemAddSubgroupHσ σ = inferInstance

theorem Frourio.Lp_norm_sq_as_lintegral {ν : MeasureTheory.Measure ℝ} (f : ↥(MeasureTheory.Lp ℂ 2 ν)) : ‖f‖ ^ 2 = (∫⁻ (x : ℝ), ↑‖↑↑f x‖₊ ^ 2 ∂ν).toReal

theorem Frourio.lintegral_withDensity_expand {g wσ : ℝ → ENNReal} (hg : Measurable g) (hwσ : Measurable wσ) : ∫⁻ (x : ℝ), g x ∂mulHaar.withDensity wσ = ∫⁻ (x : ℝ), g x * wσ x ∂mulHaar

theorem Frourio.lintegral_mulHaar_expand {g : ℝ → ENNReal} (hg : Measurable g) : ∫⁻ (x : ℝ), g x ∂mulHaar = ∫⁻ (x : ℝ) in Set.Ioi 0, g x * ENNReal.ofReal (1 / x)

theorem Frourio.weight_product_simplify (σ x : ℝ) (hx : x ∈ Set.Ioi 0) : ENNReal.ofReal (x ^ (2 * σ - 1)) * ENNReal.ofReal (1 / x) = ENNReal.ofReal (x ^ (2 * σ - 1) / x)

theorem Frourio.Hσ_norm_squared {σ : ℝ} (f : ↥(Hσ σ)) : ‖f‖ ^ 2 = (∫⁻ (x : ℝ) in Set.Ioi 0, ↑‖Hσ.toFun f x‖₊ ^ 2 * ENNReal.ofReal (x ^ (2 * σ - 1) / x)).toReal

theorem Frourio.zeroLatticeSpacing_pos {φ : ℝ} (hφ : 1 < φ) : 0 < zeroLatticeSpacing φ

theorem Frourio.log_preimage_inter_Ioi_eq_exp_image {s : Set ℝ} : Real.log ⁻¹' s ∩ Set.Ioi 0 = Real.exp '' s

Helper lemma: The preimage of s under log, intersected with (0,∞), equals exp(s)

theorem Frourio.volume_exp_image_eq_integral {s : Set ℝ} (hs : MeasurableSet s) : MeasureTheory.volume (Real.exp '' s) = ∫⁻ (t : ℝ) in s, ENNReal.ofReal (Real.exp t)

Helper lemma: For a measurable set s, the volume of exp(s) equals the integral of exp over s.

theorem Frourio.exp_surjective_onto_Ioi : Set.SurjOn Real.exp Set.univ (Set.Ioi 0)

Helper lemma: exp maps ℝ onto (0,∞)

theorem Frourio.measurableSet_exp_image {s : Set ℝ} (hs : MeasurableSet s) : MeasurableSet (Real.exp '' s)

Helper lemma: The image of a measurable set under exp is measurable

theorem Frourio.map_log_restrict_Ioi_eq_withDensity_exp : MeasureTheory.Measure.map Real.log (MeasureTheory.volume.restrict (Set.Ioi 0)) = MeasureTheory.volume.withDensity fun (t : ℝ) => ENNReal.ofReal (Real.exp t)

Pushforward of Lebesgue measure on (0,∞) by log equals Lebesgue on ℝ weighted by the density exp. Concretely: This is the change-of-variables formula for x = exp t at the level of measures.

Change of Variables Lemmas for Mellin-Plancherel

These lemmas establish the key change of variables formulas needed for the logarithmic pullback map from L²(ℝ) to Hσ.

theorem Frourio.lintegral_change_of_variables_exp {α : ℝ} {f : ℝ → ENNReal} (hf : Measurable f) : ∫⁻ (x : ℝ) in Set.Ioi 0, f (Real.log x) * ENNReal.ofReal (x ^ α) ∂MeasureTheory.volume.restrict (Set.Ioi 0) = ∫⁻ (t : ℝ), f t * ENNReal.ofReal (Real.exp (α * t + t))

Change of variables formula: x = exp(t) for integration over (0,∞). For a measurable function f and real α, we have: ∫₀^∞ f(log x) · x^α dx = ∫₋∞^∞ f(t) · exp((α + 1) · t) dt

theorem Frourio.lintegral_log_substitute {f : ℝ → ENNReal} (hf : Measurable f) : ∫⁻ (x : ℝ) in Set.Ioi 0, f (Real.log x) * ENNReal.ofReal x⁻¹ ∂MeasureTheory.volume.restrict (Set.Ioi 0) = ∫⁻ (t : ℝ), f t

Special case for α = -1: ∫₀^∞ f(log x) · x⁻¹ dx = ∫₋∞^∞ f(t) dt

theorem Frourio.mulHaar_eq_volume_div_x : mulHaar = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (1 / x)

Relationship between mulHaar measure and volume with density 1/x

theorem Frourio.norm_cpow_real (x σ : ℝ) (hx : 0 < x) : ‖↑x ^ (-↑σ)‖₊ = x.toNNReal.rpow (-σ)

For positive real x and real σ, the norm of x^(-σ) as a complex number equals x^(-σ)

Small helper lemmas used in local algebraic cancellations

theorem Frourio.coe_nnnorm_mul (a b : ℂ) : ↑‖a * b‖₊ = ↑‖a‖₊ * ↑‖b‖₊

Auxiliary placeholder embedding from L²(ℝ) (Lebesgue) into Hσ. In the present phase, this acts as the zero map to keep the API flowing. It will be replaced by the genuine logarithmic pullback inverse in P3.

theorem Frourio.hwσ_meas_for_optimization (σ : ℝ) (wσ : ℝ → ENNReal) (hwσ : wσ = fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) : Measurable wσ

theorem Frourio.hx_cancel_for_optimization (σ x : ℝ) (hx' : 0 < x) (wσ : ℝ → ENNReal) (hwσ : wσ = fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) : ↑‖x ^ (2⁻¹ - σ)‖₊ * (↑‖x ^ (2⁻¹ - σ)‖₊ * wσ x) = 1

theorem Frourio.hg_meas_for_optimization (σ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (g : ℝ → ℂ) (hg_def : g = fun (x : ℝ) => if x_1 : 0 < x then ↑↑f (Real.log x) * ↑x ^ (-(↑σ - ↑(1 / 2))) else 0) : Measurable fun (x : ℝ) => ↑‖g x‖₊ ^ 2

theorem Frourio.expand_withDensity (g : ℝ → ℂ) (wσ : ℝ → ENNReal) (hg_meas : Measurable fun (x : ℝ) => ↑‖g x‖₊ ^ 2) (hwσ_meas : Measurable wσ) : ∫⁻ (x : ℝ), ↑‖g x‖₊ ^ 2 ∂mulHaar.withDensity wσ = ∫⁻ (x : ℝ), ↑‖g x‖₊ ^ 2 * wσ x ∂mulHaar

noncomputable def Frourio.toHσ_ofL2 (σ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↥(Hσ σ)

Map an L²(ℝ) function to an element of Hσ. Implementation via logarithmic pullback: f(t) ↦ f(log x) with appropriate measure adjustment. For f ∈ L²(ℝ), we define g(x) = f(log x) · x^(-σ) which lies in Hσ.

Equations

• Frourio.toHσ_ofL2 σ f = MeasureTheory.MemLp.toLp (fun (x : ℝ) => if hx : 0 < x then ↑↑f (Real.log x) * ↑x ^ (-(↑σ - ↑(1 / 2))) else 0) ⋯