Weighted L² Hilbert Spaces for Mellin Transform Theory

This file implements the weighted L² spaces Hσ that are central to the Mellin transform formulation of Frourio mathematics. These spaces are L²((0,∞), x^(2σ-1) dx) with respect to the multiplicative Haar measure.

Main Definitions

• weightFunction: The weight function x^(2σ-1) for the measure
• weightedMeasure: The weighted measure x^(2σ-1) * (dx/x)
• Inner product structure on Hσ
• Completeness of Hσ

Main Theorems

• Hσ.completeSpace: Hσ is a complete metric space
• weightedMeasure_finite_conditions: Characterization of when the weighted measure is finite
• schwartz_dense_in_Hσ: Schwartz functions are dense in Hσ

noncomputable def Frourio.weightFunction (σ : ℝ) : ℝ → ENNReal

The weight function for the weighted L² space

Equations

• Frourio.weightFunction σ x = if x > 0 then ENNReal.ofReal (x ^ (2 * σ - 1)) else 0

theorem Frourio.weightFunction_measurable (σ : ℝ) : Measurable (weightFunction σ)

noncomputable def Frourio.weightedMeasure (σ : ℝ) : MeasureTheory.Measure ℝ

The weighted measure for Hσ

Equations

• Frourio.weightedMeasure σ = mulHaar.withDensity (Frourio.weightFunction σ)

theorem Frourio.weightedMeasure_apply (σ : ℝ) (s : Set ℝ) (hs : MeasurableSet s) : (weightedMeasure σ) s = ∫⁻ (x : ℝ) in s ∩ Set.Ioi 0, ENNReal.ofReal (x ^ (2 * σ - 2))

noncomputable instance Frourio.Hσ.innerProductSpace (σ : ℝ) : InnerProductSpace ℂ ↥(Hσ σ)

Inner product on Hσ inherited from L² structure

Equations

• Frourio.Hσ.innerProductSpace σ = inferInstance

theorem Frourio.Hσ_inner_def (σ : ℝ) (f g : ↥(Hσ σ)) : inner ℂ f g = ∫ (x : ℝ), (starRingEnd ℂ) (Hσ.toFun f x) * Hσ.toFun g x ∂mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))

The inner product on Hσ is the L2 inner product with weighted measure

theorem Frourio.Hσ_inner_conj_symm (σ : ℝ) (f g : ↥(Hσ σ)) : inner ℂ f g = (starRingEnd ℂ) (inner ℂ g f)

The inner product conjugate symmetry in Hσ

theorem Frourio.Hσ.norm_squared (σ : ℝ) (f : ↥(Hσ σ)) : ‖f‖ ^ 2 = (∫⁻ (x : ℝ), ↑‖Hσ.toFun f x‖₊ ^ 2 ∂mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))).toReal

instance Frourio.Hσ.completeSpace (σ : ℝ) : CompleteSpace ↥(Hσ σ)

Hσ is a complete metric space

theorem Frourio.Hσ.cauchy_complete (σ : ℝ) (f : ℕ → ↥(Hσ σ)) (hf : CauchySeq f) : ∃ (g : ↥(Hσ σ)), Filter.Tendsto f Filter.atTop (nhds g)

Cauchy sequences in Hσ converge

theorem Frourio.weightedMeasure_finite_on_bounded (σ a b : ℝ) (ha : 0 < a) (hb : a < b) : (weightedMeasure σ) (Set.Ioo a b) < ⊤

Conditions for the weighted measure to be finite on bounded sets

theorem Frourio.weightedMeasure_Ioc_zero_one_lt_top {σ : ℝ} (hσ : 1 / 2 < σ) : (weightedMeasure σ) (Set.Ioc 0 1) < ⊤

instance Frourio.weightedMeasure_isLocallyFinite (σ : ℝ) [Fact (1 / 2 < σ)] : MeasureTheory.IsLocallyFiniteMeasure (weightedMeasure σ)

instance Frourio.mulHaar_sigmaFinite : MeasureTheory.SigmaFinite mulHaar

mulHaar is sigma-finite

instance Frourio.weightedMeasure_sigmaFinite (σ : ℝ) : MeasureTheory.SigmaFinite (weightedMeasure σ)

The weighted measure is sigma-finite

theorem Frourio.weightedMeasure_global_infinite (σ : ℝ) : (weightedMeasure σ) (Set.Ioi 0) = ⊤

The global weighted measure is always infinite. We postpone the analytic divergence proof for a future refinement.

theorem Frourio.exists_simple_func_approximation {σ : ℝ} (f' : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (ε : ℝ) (hε : 0 < ε) : ∃ (s : ↥(MeasureTheory.Lp.simpleFunc ℂ 2 (weightedMeasure σ))), dist (↑s) f' < ε

theorem Frourio.eLpNorm_indicator_le_simple {σ : ℝ} (f : ℝ → ℂ) (S : Set ℝ) : MeasurableSet S → MeasureTheory.eLpNorm (S.indicator f) 2 (weightedMeasure σ) ≤ MeasureTheory.eLpNorm f 2 (weightedMeasure σ)

Helper lemma: eLpNorm of indicator function is at most the original

theorem Frourio.measurable_extended_mollifier (δ : ℝ) : Measurable fun (t : ℝ) => if t ∈ Set.Ioo (-δ) δ then Real.exp (-1 / (δ ^ 2 - t ^ 2)) else 0

Measurability of the extended mollifier function

theorem Frourio.indicator_toSimpleFunc_aestrongly_measurable {σ : ℝ} (s : ↥(MeasureTheory.Lp.simpleFunc ℂ 2 (weightedMeasure σ))) (S : Set ℝ) (hS : MeasurableSet S) : MeasureTheory.AEStronglyMeasurable (S.indicator ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc s)) (weightedMeasure σ)

Helper lemma: The indicator of toSimpleFunc on a measurable set is AE strongly measurable

theorem Frourio.truncated_simple_func_mem_Lp {σ : ℝ} (s : ↥(MeasureTheory.Lp.simpleFunc ℂ 2 (weightedMeasure σ))) (n : ℕ) : let truncate := fun (x : ℝ) => if 1 / ↑n < x ∧ x < ↑n then (MeasureTheory.Lp.simpleFunc.toSimpleFunc s) x else 0; MeasureTheory.MemLp truncate 2 (weightedMeasure σ)

Helper lemma: A truncated simple function with compact support is in L²

theorem Frourio.mollifier_extended_continuous (δ' : ℝ) : 0 < δ' → ContinuousOn (fun (s : ℝ) => if |s| < δ' then Real.exp (-1 / (δ' ^ 2 - s ^ 2)) else 0) (Set.uIcc (-δ') δ')

theorem Frourio.integral_Ioo_eq_intervalIntegral (δ : ℝ) (hδ_pos : 0 < δ) : let f_extended := fun (t : ℝ) => if t ∈ Set.Ioo (-δ) δ then Real.exp (-1 / (δ ^ 2 - t ^ 2)) else 0; ∫ (t : ℝ) in Set.Ioo (-δ) δ, Real.exp (-1 / (δ ^ 2 - t ^ 2)) = ∫ (t : ℝ) in -δ..δ, f_extended t

The integral of exp(-1/(δ²-t²)) over the open interval (-δ, δ) equals its interval integral over [-δ, δ] with extended function

theorem Frourio.mollifier_normalization_positive (δ : ℝ) (hδ_pos : 0 < δ) : 0 < ∫ (t : ℝ) in Set.Ioo (-δ) δ, Real.exp (-1 / (δ ^ 2 - t ^ 2))

The normalization constant for the mollifier is positive

theorem Frourio.mollifier_smooth_at_boundary (δ : ℝ) : 0 < δ → let Z := ∫ (t : ℝ) in Set.Ioo (-δ) δ, Real.exp (-1 / (δ ^ 2 - t ^ 2)); let φ := fun (y : ℝ) => if |y| < δ then Real.exp (-1 / (δ ^ 2 - y ^ 2)) / Z else 0; ContDiffAt ℝ (↑⊤) φ δ ∧ ContDiffAt ℝ (↑⊤) φ (-δ)

The mollifier function is smooth at both boundary points

theorem Frourio.truncated_shifted_measurable {σ : ℝ} {n : ℕ} (x : ℝ) (s : ↥(MeasureTheory.Lp.simpleFunc ℂ 2 (weightedMeasure σ))) : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => if 1 / ↑n < x - y ∧ x - y < ↑n then (MeasureTheory.Lp.simpleFunc.toSimpleFunc s) (x - y) else 0) MeasureTheory.volume

Measurability of truncated shifted simple function using toSimpleFunc

theorem Frourio.convolution_smooth_of_smooth_compsupp_and_integrable {φ f : ℝ → ℂ} (hφ_smooth : ContDiff ℝ (↑⊤) φ) (hφ_supp : HasCompactSupport φ) (hf_integrable : ∀ (x : ℝ), MeasureTheory.Integrable (fun (y : ℝ) => f (x - y)) MeasureTheory.volume) : ContDiff ℝ ↑⊤ fun (x : ℝ) => ∫ (y : ℝ), φ y * f (x - y)

Convolution of a smooth function with compact support and an integrable function is smooth

theorem Frourio.smooth_mollifier_convolution_truncated {δ : ℝ} {n : ℕ} {σ : ℝ} (φ_δ : ℝ → ℝ) (s : ↥(MeasureTheory.Lp.simpleFunc ℂ 2 (weightedMeasure σ))) (hφ_smooth : ContDiff ℝ (↑⊤) φ_δ) (hφ_supp : ∀ (y : ℝ), |y| > δ → φ_δ y = 0) (hδ_pos : 0 < δ) : ContDiff ℝ ↑⊤ fun (x : ℝ) => ∫ (y : ℝ), ↑(φ_δ y) * if 1 / ↑n < x - y ∧ x - y < ↑n then (MeasureTheory.Lp.simpleFunc.toSimpleFunc s) (x - y) else 0

Convolution of smooth mollifier with truncated simple function is smooth

theorem Frourio.convolution_mollifier_truncated_has_compact_support {δ : ℝ} {n : ℕ} (φ_δ : ℝ → ℝ) (truncate : ℝ → ℂ) (hφ_supp : ∀ (y : ℝ), |y| > δ → φ_δ y = 0) (hδ_pos : 0 < δ) (hn_pos : 0 < n) (h_truncate_supp : ∀ x ∉ Set.Ioo (1 / ↑n) ↑n, truncate x = 0) : ∃ R > 0, ∀ x ≥ R, ∫ (y : ℝ), ↑(φ_δ y) * truncate (x - y) = 0

Convolution of mollifier with truncated function has compact support

theorem Frourio.convolution_mollifier_truncated_zero_outside_support {δ : ℝ} {n : ℕ} (φ_δ : ℝ → ℝ) (truncate : ℝ → ℂ) (hφ_supp : ∀ (y : ℝ), |y| > δ → φ_δ y = 0) (h_truncate_supp : ∀ x ∉ Set.Ioo (1 / ↑n) ↑n, truncate x = 0) (x : ℝ) : x < 1 / ↑n - δ → ∫ (y : ℝ), ↑(φ_δ y) * truncate (x - y) = 0

Convolution of mollifier with truncated function vanishes outside support

theorem Frourio.smooth_convolution_measurable {σ : ℝ} (smooth_func : ℝ → ℂ) (h_smooth : ContDiff ℝ (↑⊤) smooth_func) : MeasureTheory.AEStronglyMeasurable smooth_func (weightedMeasure σ)

Smooth convolution with compact support is measurable

theorem Frourio.convolution_vanishes_on_nonpositive {δ : ℝ} {n : ℕ} (φ_δ : ℝ → ℝ) (truncate : ℝ → ℂ) (hφ_supp : ∀ (y : ℝ), |y| > δ → φ_δ y = 0) (hδ_small : δ ≤ 1 / ↑n) (h_truncate_supp : ∀ x ∉ Set.Ioo (1 / ↑n) ↑n, truncate x = 0) (x : ℝ) : x ≤ 0 → ∫ (y : ℝ), ↑(φ_δ y) * truncate (x - y) = 0

The convolution of a mollifier with a truncated function vanishes on (-∞, 0] when δ is sufficiently small

theorem Frourio.smooth_compact_support_memLp {σ : ℝ} (smooth_func : ℝ → ℂ) (h_smooth : ContDiff ℝ (↑⊤) smooth_func) (h_support : ∃ R > 0, ∀ x ≥ R, smooth_func x = 0) (h_support_left : ∀ x ≤ 0, smooth_func x = 0) (h_support_away_zero : ∃ a > 0, ∀ x ∈ Set.Ioo 0 a, smooth_func x = 0) : MeasureTheory.MemLp smooth_func 2 (weightedMeasure σ)

Smooth function with compact support away from 0 is in L²

theorem Frourio.smooth_mollifier_convolution_memLp {σ δ : ℝ} {n : ℕ} (φ_δ : ℝ → ℝ) (s : ↥(MeasureTheory.Lp.simpleFunc ℂ 2 (weightedMeasure σ))) (hφ_smooth : ContDiff ℝ (↑⊤) φ_δ) (hφ_supp : ∀ (y : ℝ), |y| > δ → φ_δ y = 0) (hδ_pos : 0 < δ) (hn_pos : 0 < n) (hδ_bound : δ < 1 / ↑n) : MeasureTheory.MemLp (fun (x : ℝ) => ∫ (y : ℝ), ↑(φ_δ y) * if 1 / ↑n < x - y ∧ x - y < ↑n then (MeasureTheory.Lp.simpleFunc.toSimpleFunc s) (x - y) else 0) 2 (weightedMeasure σ)

Smooth functions that are convolutions of mollifiers with truncated simple functions are in L²