@[simp]

theorem Frourio.ennorm_sq_eq_ofReal_norm_sq (z : ℂ) : ‖z‖ₑ ^ 2 = ENNReal.ofReal (‖z‖ ^ 2)

Helper identity converting the squared extended norm to an ENNReal.ofReal quadratic.

@[simp]

theorem Frourio.norm_norm_sq (z : ℂ) : ‖‖z‖ ^ 2‖ = ‖z‖ ^ 2

theorem Frourio.lp_restricted_aestronglyMeasurable {σ : ℝ} (s : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (R : ℝ) : MeasureTheory.AEStronglyMeasurable (↑↑s) (MeasureTheory.volume.restrict (Set.Ioc 0 R))

Helper lemma: Lp function restricted to a set is AE strongly measurable

theorem Frourio.withDensity_mul_indicator (σ : ℝ) : (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal x⁻¹).withDensity ((Set.Ioi 0).indicator (weightFunction σ)) = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal x⁻¹ * (Set.Ioi 0).indicator (weightFunction σ) x

Composition of density functions for weighted measures

theorem Frourio.lp_truncation_memLp_on_Ioc {σ : ℝ} (hσ_upper : σ ≤ 1) (s : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (R : ℝ) (p : ENNReal) (hp : p = 2) : MeasureTheory.MemLp (fun (x : ℝ) => if 0 < x ∧ x ≤ R then ↑↑s x else 0) p (MeasureTheory.volume.restrict (Set.Ioc 0 R))

Truncated Lp functions are in Lp with respect to volume measure on compact intervals NOTE: This requires σ ≤ 1 for the transfer from weighted to unweighted measure. For σ > 1, functions in L²(weightedMeasure σ) may not be in L²(volume). Example: σ = 6/5, s(x) = x^{-3/5} is in L²(weighted) but not L²(volume).

theorem Frourio.integrable_on_truncated_function {f : ℝ → ℂ} {R : ℝ} {p : ENNReal} (h_memLp : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (Set.Ioc 0 R))) (hp : 1 ≤ p) : MeasureTheory.IntegrableOn f (Set.Ioc 0 R) MeasureTheory.volume

Integrability on support for Lp functions on finite measure sets

theorem Frourio.lp_truncation_integrable {σ : ℝ} (hσ_upper : σ ≤ 1) (s : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (R : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => if 0 < x ∧ x ≤ R then ↑↑s x else 0) MeasureTheory.volume

Truncated Lp functions are integrable with respect to volume measure NOTE: This requires σ ≤ 1 for the proof to work through L² membership. For σ > 1, a different approach would be needed.

theorem Frourio.positive_truncation_memLp {σ : ℝ} (s : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (R : ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => if 0 < x ∧ x ≤ R then ↑↑s x else 0) 2 (weightedMeasure σ)

Positive truncation of Lp function is also in Lp for weighted measure

theorem Frourio.positive_truncation_error_bound {σ : ℝ} (s : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (R ε : ℝ) (hR_truncation : MeasureTheory.eLpNorm (fun (x : ℝ) => if |x| > R then ↑↑s x else 0) 2 (weightedMeasure σ) < ENNReal.ofReal ε) : let s_R := fun (x : ℝ) => if 0 < x ∧ x ≤ R then ↑↑s x else 0; MeasureTheory.eLpNorm (↑↑s - s_R) 2 (weightedMeasure σ) < ENNReal.ofReal ε

Error bound for positive truncation vs tail truncation

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

Convolution of integrable function with smooth compact support function is continuous

theorem Frourio.convolution_memLp_weighted {σ : ℝ} (hσ : 1 / 2 < σ) {f : ℝ → ℂ} {φ : ℝ → ℝ} (R δ : ℝ) (hR_pos : 0 < R) (hδ_pos : 0 < δ) (hf_support : Function.support f ⊆ Set.Icc (-R) R) (_hf_memLp : MeasureTheory.MemLp f 2 (weightedMeasure σ)) (hf_vol_integrable : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_support : Function.support φ ⊆ Set.Icc (-δ) δ) : MeasureTheory.MemLp (fun (x : ℝ) => ∫ (y : ℝ), f y * ↑(φ (x - y))) 2 (weightedMeasure σ)

Volume convolution with smooth compact kernel preserves L² membership in weighted spaces when f has bounded support

theorem Frourio.dist_lp_truncation_bound {σ : ℝ} (s : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (ε : ℝ) (hε : 0 < ε) (s_R : ℝ → ℂ) (hs_R_memLp : MeasureTheory.MemLp s_R 2 (weightedMeasure σ)) (h_truncation_error : MeasureTheory.eLpNorm (↑↑s - s_R) 2 (weightedMeasure σ) < ENNReal.ofReal ε) : dist s (MeasureTheory.MemLp.toLp s_R hs_R_memLp) < ε

Distance bound from truncation error for Lp elements

theorem Frourio.truncation_approximation {σ : ℝ} (hσ : 1 / 2 < σ) (f : ℝ → ℂ) (hf_memLp : MeasureTheory.MemLp f 2 (weightedMeasure σ)) (ε : ℝ) (hε_pos : 0 < ε) : ∃ (R : ℝ) (_ : 0 < R) (f_R : ℝ → ℂ) (_ : MeasureTheory.MemLp f_R 2 (weightedMeasure σ)), HasCompactSupport f_R ∧ MeasureTheory.eLpNorm (f - f_R) 2 (weightedMeasure σ) < ENNReal.ofReal (ε / 2)

Truncation approximation: Any L² function can be approximated by compactly supported functions

theorem Frourio.weightedMeasure_eq_withDensity (σ : ℝ) : weightedMeasure σ = mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))

The weighted measure is equivalent to withDensity measure