theorem Frourio.weightedMeasure_finite_on_compact {σ : ℝ} (hσ : 1 / 2 < σ) {K : Set ℝ} (hK_compact : IsCompact K) : (weightedMeasure σ) K < ⊤

The weighted measure is finite on compact sets for σ > 1/2

theorem Frourio.memLp_of_hasFiniteIntegral_and_aestronglyMeasurable {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℂ} (hf_meas : MeasureTheory.AEStronglyMeasurable f μ) (hf_finite : MeasureTheory.HasFiniteIntegral (fun (x : ℝ) => ‖f x‖ ^ 2) μ) : MeasureTheory.MemLp f 2 μ

Convert HasFiniteIntegral and AEStronglyMeasurable to MemLp for p = 2

theorem Frourio.hasFiniteIntegral_of_dominated_on_compactSupport {μ : MeasureTheory.Measure ℝ} {g : ℝ → ℂ} {M : ℝ} (h_dominated : ∀ᵐ (x : ℝ) ∂μ, ‖g x‖ ^ 2 ≤ M ^ 2) (h_finite_on_support : μ (tsupport g) < ⊤) : MeasureTheory.HasFiniteIntegral (fun (x : ℝ) => ‖g x‖ ^ 2) μ

For a function with compact support that is dominated a.e. by a constant on its support, if the weighted measure of the support is finite, then the function has finite integral

theorem Frourio.memLp_convolution_simpleFunc_truncation {σ : ℝ} (hσ : 1 / 2 < σ) (f_simple : MeasureTheory.SimpleFunc ℝ ℂ) (φ : ℝ → ℝ) (R δ : ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => if |x| ≤ R then f_simple x else 0) 2 (weightedMeasure σ) → ∀ (hφ_smooth : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_support : Function.support φ ⊆ Set.Icc (-δ) δ) (hR_pos : 0 < R) (hδ_pos : 0 < δ), MeasureTheory.MemLp (fun (x : ℝ) => ∫ (y : ℝ), (if |y| ≤ R then f_simple y else 0) * ↑(φ (x - y))) 2 (weightedMeasure σ)

Convolution of simple function truncation with smooth compact support function is in L²

theorem Frourio.eLpNorm_lp_function_diff_eq {σ : ℝ} (s : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (f : ℝ → ℂ) (hf_memLp : MeasureTheory.MemLp f 2 (weightedMeasure σ)) : MeasureTheory.eLpNorm (↑↑s - ↑↑(MeasureTheory.MemLp.toLp f hf_memLp)) 2 (weightedMeasure σ) = MeasureTheory.eLpNorm (↑↑s - f) 2 (weightedMeasure σ)

eLpNorm equality for Lp element and function difference

theorem Frourio.weightedMeasure_finite_on_interval {σ : ℝ} (hσ : 1 / 2 < σ) (R : ℝ) : (weightedMeasure σ) (Set.Icc (-R) R) < ⊤

Compact intervals have finite weighted measure for σ > 1/2

theorem Frourio.simpleFunc_unbounded_levelSet_finite_measure_L2 {σ : ℝ} (_hσ : 1 / 2 < σ) (f : MeasureTheory.SimpleFunc ℝ ℂ) (hf_memL2 : MeasureTheory.MemLp (⇑f) 2 (weightedMeasure σ)) (v : ℂ) (hv_nonzero : v ≠ 0) (_hv_range : v ∈ Set.range ⇑f) (_h_unbounded : ¬∃ R > 0, {x : ℝ | f x = v} ⊆ Set.Icc (-R) R) : (weightedMeasure σ) {x : ℝ | f x = v} ≠ ⊤

Unbounded level sets of L² simple functions have finite weighted measure for σ > 1/2

theorem Frourio.simpleFunc_levelSet_tail_measure_vanishing {σ : ℝ} (hσ : 1 / 2 < σ) (f : MeasureTheory.SimpleFunc ℝ ℂ) (hf_memL2 : MeasureTheory.MemLp (⇑f) 2 (weightedMeasure σ)) (v : ℂ) (hv_nonzero : v ≠ 0) (hv_range : v ∈ Set.range ⇑f) : Filter.Tendsto (fun (R : ℝ) => (weightedMeasure σ) {x : ℝ | f x = v ∧ R < |x|}) Filter.atTop (nhds 0)

theorem Frourio.simpleFunc_tail_l2_convergence {σ : ℝ} (_hσ : 1 / 2 < σ) (f : MeasureTheory.SimpleFunc ℝ ℂ) (_hf_memLp : MeasureTheory.MemLp (⇑f) 2 (weightedMeasure σ)) (_h_pointwise : ∀ (x : ℝ), Filter.Tendsto (fun (R : ℝ) => if |x| ≤ R then 0 else f x) Filter.atTop (nhds 0)) (_h_domination : ∀ (R x : ℝ), ‖if |x| ≤ R then 0 else f x‖ ≤ ‖f x‖) (h_tail_measure_vanishing : ∀ (v : ℂ), v ≠ 0 → v ∈ Set.range ⇑f → Filter.Tendsto (fun (R : ℝ) => (weightedMeasure σ) {x : ℝ | f x = v ∧ R < |x|}) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (R : ℝ) => MeasureTheory.eLpNorm (fun (x : ℝ) => if |x| ≤ R then 0 else f x) 2 (weightedMeasure σ)) Filter.atTop (nhds 0)

L² convergence of tail functions for simple functions

theorem Frourio.simpleFunc_tail_pointwise_limit (f : MeasureTheory.SimpleFunc ℝ ℂ) (x : ℝ) : Filter.Tendsto (fun (R : ℝ) => if |x| ≤ R then 0 else f x) Filter.atTop (nhds 0)

For simple functions, the tail truncation converges pointwise to zero

theorem Frourio.simpleFunc_tail_L2_convergence {σ : ℝ} (hσ : 1 / 2 < σ) (f : MeasureTheory.SimpleFunc ℝ ℂ) (hf_memLp : MeasureTheory.MemLp (⇑f) 2 (weightedMeasure σ)) : Filter.Tendsto (fun (R : ℝ) => MeasureTheory.eLpNorm (fun (x : ℝ) => if |x| ≤ R then 0 else f x) 2 (weightedMeasure σ)) Filter.atTop (nhds 0)

Tail functions of L² simple functions converge to 0 in L² norm by dominated convergence

theorem Frourio.l2_tail_vanishing {σ : ℝ} (hσ : 1 / 2 < σ) (f : MeasureTheory.SimpleFunc ℝ ℂ) (hf_memLp : MeasureTheory.MemLp (⇑f) 2 (weightedMeasure σ)) (ε : ℝ) (hε : 0 < ε) : ∃ (R : ℝ), 0 < R ∧ MeasureTheory.eLpNorm (fun (x : ℝ) => if |x| ≤ R then 0 else f x) 2 (weightedMeasure σ) < ENNReal.ofReal ε

L² functions have vanishing tails: for any ε > 0, there exists R > 0 such that the L² norm of the function outside [-R, R] is less than ε

theorem Frourio.truncation_memLp {σ : ℝ} (hσ : 1 / 2 < σ) (f : MeasureTheory.SimpleFunc ℝ ℂ) (_hf_memLp : MeasureTheory.MemLp (⇑f) 2 (weightedMeasure σ)) (R : ℝ) (_hR_pos : 0 < R) : MeasureTheory.MemLp (fun (x : ℝ) => if |x| ≤ R then f x else 0) 2 (weightedMeasure σ)

Truncation of an L² function to a bounded interval remains in L²

theorem Frourio.lp_tail_vanishing {σ : ℝ} (hσ : 1 / 2 < σ) (s : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (ε : ℝ) (hε : 0 < ε) : ∃ (R : ℝ), 0 < R ∧ MeasureTheory.eLpNorm (fun (x : ℝ) => if |x| > R then ↑↑s x else 0) 2 (weightedMeasure σ) < ENNReal.ofReal ε

Tail vanishing property for Lp functions in weighted measure

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

Truncation of Lp functions preserves Lp membership

theorem Frourio.mollification_delta_small (ε : ℝ) (hε_pos : 0 < ε) (s_R : ℝ → ℂ) (R : ℝ) (_hR_pos : 0 < R) (σ : ℝ) : let M := (MeasureTheory.eLpNorm s_R 2 (weightedMeasure σ)).toReal + 1; let δ := min (ε / (8 * M)) (1 / (2 * (R + 1))); δ < ε / (4 * M)

Mollification parameter δ is small when defined as minimum

theorem Frourio.schwartzToHσ_continuous {σ : ℝ} (hσ : 1 / 2 < σ) : ∃ (k₁ : ℕ) (C₀ : ℝ) (C₁ : ℝ), 0 < C₀ ∧ 0 < C₁ ∧ ∀ (f : SchwartzMap ℝ ℂ), ‖schwartzToHσ hσ f‖ ≤ C₀ * (SchwartzMap.seminorm ℝ 0 0) f + C₁ * (SchwartzMap.seminorm ℝ k₁ 0) f

The embedding is continuous with respect to a finite family of Schwartz seminorms for σ > 1/2