theorem Frourio.lp2_holder_bound (f : ℝ → ℂ) (s : Set ℝ) (hs : MeasurableSet s) : ∫⁻ (x : ℝ) in s, ↑‖f x‖₊ ^ 2 ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume ^ 2

Basic L² bound for functions on measurable sets

theorem Frourio.ennreal_pow_mul_le_of_le {a b c d : ENNReal} (h1 : a ≤ b) (h2 : c < d) (n : ℕ) : a ^ n * c ≤ b ^ n * d

Helper lemma for multiplying inequalities with ENNReal powers

theorem Frourio.l2_integral_volume_bound (f_L2 : ℝ → ℂ) (s : Set ℝ) (hs_meas : MeasurableSet s) : ∫⁻ (x : ℝ) in s, ↑‖f_L2 x‖₊ ^ 2 ≤ MeasureTheory.eLpNorm f_L2 2 MeasureTheory.volume ^ 2

The L² integral over a subset is bounded by the total L² norm squared

theorem Frourio.measure_continuity_closed_ball {R : ℝ} (h_empty_measure : MeasureTheory.volume (⋂ (n : ℕ), {x : ℝ | ↑n < ‖x‖} ∩ Metric.closedBall 0 R) = 0) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.volume ({x : ℝ | ↑n < ‖x‖} ∩ Metric.closedBall 0 R)) Filter.atTop (nhds 0)

Helper lemma for measure continuity on closed balls

theorem Frourio.tendsto_tail_measure_closed_ball_zero (R : ℝ) : R > 0 → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.volume ({x : ℝ | ↑n < ‖x‖} ∩ Metric.closedBall 0 R)) Filter.atTop (nhds 0)

The measure of tail sets intersected with closed balls tends to zero

theorem Frourio.measurableSet_tail_norm (R : ℝ) : MeasurableSet {x : ℝ | R < ‖x‖}

The tail set {x : ℝ | R < ‖x‖} is measurable for every real R.

theorem Frourio.tail_set_subset {R₁ R₂ : ℝ} (hR : R₁ ≤ R₂) : {x : ℝ | R₂ < ‖x‖} ⊆ {x : ℝ | R₁ < ‖x‖}

If R₁ ≤ R₂, then the tail sets are nested: {‖x‖ > R₂} ⊆ {‖x‖ > R₁}.

theorem Frourio.indicator_le_indicator_of_subset {α : Type u_1} {s t : Set α} (h_subset : s ⊆ t) (f : α → ENNReal) : s.indicator f ≤ t.indicator f

For nonnegative functions, the indicators of nested sets satisfy a pointwise inequality.

theorem Frourio.tail_integral_mono (f : ℝ → ℂ) {R₁ R₂ : ℝ} (hR : R₁ ≤ R₂) : ∫⁻ (x : ℝ) in {x : ℝ | R₂ < ‖x‖}, ↑‖f x‖₊ ^ 2 ≤ ∫⁻ (x : ℝ) in {x : ℝ | R₁ < ‖x‖}, ↑‖f x‖₊ ^ 2

Increasing the tail radius can only decrease the tail integral.

theorem Frourio.tail_integral_le_total (f : ℝ → ℂ) (R : ℝ) : ∫⁻ (x : ℝ) in {x : ℝ | R < ‖x‖}, ↑‖f x‖₊ ^ 2 ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume ^ 2

Every tail integral is bounded by the full L² norm squared.

theorem Frourio.l2_tail_integral_small (f_L2 : ℝ → ℂ) (h_finite : MeasureTheory.eLpNorm f_L2 2 MeasureTheory.volume < ⊤) (δ : ℝ) (hδ : 0 < δ) : ∃ R₀ ≥ 1, ∀ R ≥ R₀, ∫⁻ (x : ℝ) in {x : ℝ | R < ‖x‖}, ↑‖f_L2 x‖₊ ^ 2 < ENNReal.ofReal δ

Tail integral of L² functions can be made arbitrarily small

theorem Frourio.truncation_error_eq_tail_norm (f : ℝ → ℂ) (_hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (R : ℝ) (_hR : 0 < R) : MeasureTheory.eLpNorm (f - fun (x : ℝ) => if ‖x‖ ≤ R then f x else 0) 2 MeasureTheory.volume = (∫⁻ (x : ℝ) in {x : ℝ | R < ‖x‖}, ↑‖f x‖₊ ^ 2) ^ (1 / 2)

The L² norm of the difference between a function and its truncation equals the square root of the tail integral

theorem Frourio.l2_truncation_approximation (f_L2 : ℝ → ℂ) (hf : MeasureTheory.MemLp f_L2 2 MeasureTheory.volume) (ε : ℝ) (hε : 0 < ε) : ∃ R > 0, MeasureTheory.eLpNorm (f_L2 - fun (x : ℝ) => if ‖x‖ ≤ R then f_L2 x else 0) 2 MeasureTheory.volume < ENNReal.ofReal ε

Smooth compactly supported functions are dense in L²(ℝ)

theorem Frourio.truncated_function_memLp (f : ℝ → ℂ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (R : ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => if ‖x‖ ≤ R then f x else 0) 2 MeasureTheory.volume

If f is in L² and we truncate it to a ball, the result is still in L²

theorem Frourio.simple_function_approximation_compact_support (f : ℝ → ℂ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hf_compact : HasCompactSupport f) (ε : ℝ) (hε : 0 < ε) : ∃ (s_simple : MeasureTheory.SimpleFunc ℝ ℂ), HasCompactSupport ⇑s_simple ∧ MeasureTheory.eLpNorm (fun (x : ℝ) => f x - s_simple x) 2 MeasureTheory.volume < ENNReal.ofReal ε

Simple functions with compact support are dense in L² functions with compact support

theorem Frourio.volume_tsupport_lt_top {f : ℝ → ℂ} (hf : HasCompactSupport f) : MeasureTheory.volume (tsupport f) < ⊤

The Lebesgue measure of the topological support of a compactly supported function is finite.

theorem Frourio.continuous_bound_on_tsupport {f : ℝ → ℂ} (hf_cont : Continuous f) (hf_support : HasCompactSupport f) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ tsupport f, ‖f x‖ ≤ C

A continuous function with compact support admits a uniform bound on its topological support.

theorem Frourio.schwartz_density_weighted_logpull (σ : ℝ) (f : ↥(Hσ σ)) (h_weighted_L2 : MeasureTheory.MemLp (fun (t : ℝ) => LogPull σ f t * Complex.exp (↑(1 / 2) * ↑t)) 2 MeasureTheory.volume) (ε : ℝ) : ε > 0 → ∃ (φ : SchwartzMap ℝ ℂ), MeasureTheory.eLpNorm (fun (t : ℝ) => LogPull σ f t * Complex.exp (↑(1 / 2) * ↑t) - φ t) 2 MeasureTheory.volume < ENNReal.ofReal ε

Schwartz functions are dense in L² for the weighted LogPull function

theorem Frourio.mellin_logpull_fourierIntegral (σ τ : ℝ) (f : ↥(Hσ σ)) : mellinTransform (↑↑f) (↑σ + Complex.I * ↑τ) = fourierIntegral (fun (t : ℝ) => LogPull σ f t * Complex.exp (↑(1 / 2) * ↑t)) (-τ / (2 * Real.pi))

Connection between LogPull L² norm and Mellin transform L² norm This states the Parseval-type equality for the Mellin transform. Note: The actual proof requires implementing the Fourier-Plancherel theorem for the specific weighted LogPull function.

theorem Frourio.logpull_mellin_l2_relation (σ : ℝ) (f : ↥(Hσ σ)) (h_weighted_L2 : MeasureTheory.MemLp (fun (t : ℝ) => LogPull σ f t * Complex.exp (↑(1 / 2) * ↑t)) 2 MeasureTheory.volume) (h_integrable : MeasureTheory.Integrable (fun (t : ℝ) => LogPull σ f t * Complex.exp (↑(1 / 2) * ↑t)) MeasureTheory.volume) : ∫ (t : ℝ), ‖LogPull σ f t‖ ^ 2 * Real.exp t = 1 / (2 * Real.pi) * ∫ (τ : ℝ), ‖mellinTransform (↑↑f) (↑σ + Complex.I * ↑τ)‖ ^ 2

theorem Frourio.plancherel_constant_is_one (σ : ℝ) (f : ↥(Hσ σ)) : ∃ C > 0, ∫ (τ : ℝ), ‖LogPull σ f τ‖ ^ 2 = C * ‖f‖ ^ 2 ∧ C = 1

The Plancherel constant for our normalization is 1

theorem Frourio.plancherel_constant_unique (σ : ℝ) (f : ↥(Hσ σ)) (C₁ C₂ : ℝ) (h₁_pos : C₁ > 0) (h₂_pos : C₂ > 0) (h₁_eq : ∫ (τ : ℝ), ‖LogPull σ f τ‖ ^ 2 = C₁ * ‖f‖ ^ 2) (h₂_eq : ∫ (τ : ℝ), ‖LogPull σ f τ‖ ^ 2 = C₂ * ‖f‖ ^ 2) : C₁ = C₂

Uniqueness of the Plancherel constant

theorem Frourio.mellin_parseval_formula (σ : ℝ) : ∃ C > 0, ∀ (f : ↥(Hσ σ)), ∫⁻ (x : ℝ) in Set.Ioi 0, ENNReal.ofReal (‖↑↑f x‖ ^ 2 * x ^ (2 * σ - 1)) < ⊤ → MeasureTheory.Integrable (fun (t : ℝ) => LogPull σ f t * Complex.exp (↑(1 / 2) * ↑t)) MeasureTheory.volume → ∫⁻ (x : ℝ) in Set.Ioi 0, ENNReal.ofReal (‖↑↑f x‖ ^ 2 * x ^ (2 * σ - 1)) = ENNReal.ofReal (C * ∫ (τ : ℝ), ‖mellinTransform (↑↑f) (↑σ + Complex.I * ↑τ)‖ ^ 2)

Explicit Mellin-Parseval formula (with necessary L² condition) This relates the Hσ norm to the L² norm of the Mellin transform on vertical lines. NOTE: The correct formulation requires relating weighted norms properly.

IMPORTANT: This theorem requires additional integrability condition for the weighted LogPull function to apply the Fourier-Plancherel theorem. This aligns with plan.md Phase 1 goals.

theorem Frourio.mellin_kernel_integrable_on_critical_line (σ : ℝ) (f : ↥(Hσ σ)) (τ : ℝ) (hf_L2 : has_weighted_L2_norm σ f) : MeasureTheory.Integrable (fun (t : ℝ) => ↑↑f t * ↑t ^ (↑σ + Complex.I * ↑τ - 1)) (MeasureTheory.volume.restrict (Set.Ioi 0))

Integrability of Mellin kernel for functions in Hσ on the critical line Re(s) = σ This holds specifically when s = σ + iτ for real τ

theorem Frourio.mellin_transform_linear_critical_line (σ : ℝ) (h k : ↥(Hσ σ)) (c : ℂ) (τ : ℝ) (hh_L2 : has_weighted_L2_norm σ h) (hk_L2 : has_weighted_L2_norm σ k) : mellinTransform (↑↑h + c • ↑↑k) (↑σ + Complex.I * ↑τ) = mellinTransform (↑↑h) (↑σ + Complex.I * ↑τ) + c * mellinTransform (↑↑k) (↑σ + Complex.I * ↑τ)

Alternative version: Linearity on the critical line Re(s) = σ

theorem Frourio.mellin_polarization_pointwise (F G : ℂ) : ↑‖F + G‖ ^ 2 - ↑‖F - G‖ ^ 2 - Complex.I * ↑‖F + Complex.I * G‖ ^ 2 + Complex.I * ↑‖F - Complex.I * G‖ ^ 2 = 4 * ((starRingEnd ℂ) F * G)

Polarization identity for Mellin transforms

theorem Frourio.parseval_identity_equivalence (σ : ℝ) : ∃ C > 0, ∀ (f g : ↥(Hσ σ)), has_weighted_L2_norm σ f → has_weighted_L2_norm σ g → inner ℂ f g = ↑C * ∫ (τ : ℝ), (starRingEnd ℂ) (mellinTransform (↑↑f) (↑σ + Complex.I * ↑τ)) * mellinTransform (↑↑g) (↑σ + Complex.I * ↑τ)

The Mellin-Plancherel formula relates to Fourier-Parseval

theorem Frourio.mellin_isometry_normalized (σ : ℝ) : ∃ (C : ℝ) (U : ↥(Hσ σ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), C > 0 ∧ ∀ (f : ↥(Hσ σ)), ‖U f‖ = C * ‖f‖ ∧ ↑↑(U f) = fun (τ : ℝ) => mellinTransform (↑↑f) (↑σ + Complex.I * ↑τ)

The Mellin transform preserves the L² structure up to normalization

theorem Frourio.mellin_fourier_parseval_connection (σ : ℝ) (f : ↥(Hσ σ)) : let g := fun (t : ℝ) => ↑↑f (Real.exp t) * Complex.exp ((↑σ - 1 / 2) * ↑t); ∃ (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume), ‖f‖ ^ 2 = ‖MeasureTheory.MemLp.toLp g hg‖ ^ 2

Connection between Mellin-Parseval and Fourier-Parseval

theorem Frourio.mellin_fourier_unitary_equivalence (σ : ℝ) : ∃ (V : ↥(Hσ σ) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), ∀ (f : ↥(Hσ σ)) (τ : ℝ), ∃ (c : ℂ), c ≠ 0 ∧ mellinTransform (↑↑f) (↑σ + Complex.I * ↑τ) = c * ↑↑(V f) τ

The Mellin transform is unitarily equivalent to Fourier transform

theorem Frourio.mellin_convolution_parseval (σ : ℝ) (f g : ↥(Hσ σ)) : ∫ (τ : ℝ), mellinTransform (↑↑f) (↑σ + Complex.I * ↑τ) * (starRingEnd ℂ) (mellinTransform (↑↑g) (↑σ + Complex.I * ↑τ)) = 2 * ↑Real.pi * ∫ (x : ℝ) in Set.Ioi 0, ↑↑f x * (starRingEnd ℂ) (↑↑g x) * ↑x ^ (2 * ↑σ - 1)

Mellin convolution theorem via Parseval

theorem Frourio.mellin_energy_conservation (σ : ℝ) (f : ↥(Hσ σ)) : ∫ (x : ℝ) in Set.Ioi 0, ‖↑↑f x‖ ^ 2 * x ^ (2 * σ - 1) = 1 / (2 * Real.pi) * ∫ (τ : ℝ), ‖mellinTransform (↑↑f) (↑σ + Complex.I * ↑τ)‖ ^ 2

Energy conservation in Mellin space