theorem Frourio.lp_to_continuous_approx {σ : ℝ} (hσ_lower : 1 / 2 < σ) (f : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (ε : ℝ) (hε : 0 < ε) : ∃ (g_cont : ℝ → ℂ) (hg_cont_memLp : MeasureTheory.MemLp g_cont 2 (weightedMeasure σ)), HasCompactSupport g_cont ∧ Continuous g_cont ∧ dist f (MeasureTheory.MemLp.toLp g_cont hg_cont_memLp) < ε

L² functions can be approximated by continuous compactly supported functions in weighted L² spaces

theorem Frourio.HasCompactSupport.exists_radius_closedBall {f : ℝ → ℂ} (hf : HasCompactSupport f) : ∃ (R : ℝ), 0 < R ∧ tsupport f ⊆ Metric.closedBall 0 R

Given a function with compact support on ℝ, there exists a radius R > 0 such that the topological support is contained in the closed ball of radius R.

theorem Frourio.Continuous.uniformContinuous_of_hasCompactSupport {f : ℝ → ℂ} (hf : Continuous f) (hf_support : HasCompactSupport f) : UniformContinuous f

A continuous function with compact support on ℝ is uniformly continuous.

theorem Frourio.exists_smooth_cutoff_closedBall (R : ℝ) (hR : 0 < R) : ∃ (χ : ℝ → ℝ), HasCompactSupport χ ∧ ContDiff ℝ (↑⊤) χ ∧ (∀ x ∈ Metric.closedBall 0 R, χ x = 1) ∧ tsupport χ = Metric.closedBall 0 (R + 1)

A smooth cut-off function that equals 1 on the closed ball of radius R and whose support is contained in the closed ball of radius R + 1.

theorem Frourio.lp_dist_le_of_uniform_bound_on_set {μ : MeasureTheory.Measure ℝ} {f g : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) {K : Set ℝ} (hK_meas : MeasurableSet K) (hK_fin : μ K < ⊤) (h_eq : ∀ x ∉ K, f x = g x) {C : ℝ} (hC_nonneg : 0 ≤ C) (h_bound : ∀ x ∈ K, ‖f x - g x‖ ≤ C) : dist (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp g hg) ≤ C * √(μ K).toReal

If two functions coincide outside a measurable set of finite measure and are uniformly close on that set, then their L²-distance with respect to the weighted measure is controlled by the uniform bound and the measure of the set.

theorem Frourio.continuous_to_smooth_approx {σ : ℝ} (hσ_lower : 1 / 2 < σ) (g_cont : ℝ → ℂ) (hg_cont_memLp : MeasureTheory.MemLp g_cont 2 (weightedMeasure σ)) (hg_cont_compact : HasCompactSupport g_cont) (hg_cont_continuous : Continuous g_cont) (ε : ℝ) (hε : 0 < ε) : ∃ (g : ℝ → ℂ) (hg_memLp : MeasureTheory.MemLp g 2 (weightedMeasure σ)), HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ dist (MeasureTheory.MemLp.toLp g_cont hg_cont_memLp) (MeasureTheory.MemLp.toLp g hg_memLp) < ε

Continuous compactly supported functions can be approximated by smooth compactly supported functions

theorem Frourio.lp_norm_eq_under_measure_change {σ : ℝ} (f g : ℝ → ℂ) (hf_weightedMeasure : MeasureTheory.MemLp f 2 (weightedMeasure σ)) (hg_memLp : MeasureTheory.MemLp g 2 (weightedMeasure σ)) (μ : MeasureTheory.Measure ℝ) (h_measure_eq : weightedMeasure σ = μ) (hf_memLp_μ : MeasureTheory.MemLp f 2 μ) (hg_memLp_μ : MeasureTheory.MemLp g 2 μ) : ‖MeasureTheory.MemLp.toLp f hf_weightedMeasure - MeasureTheory.MemLp.toLp g hg_memLp‖ = ‖MeasureTheory.MemLp.toLp f hf_memLp_μ - MeasureTheory.MemLp.toLp g hg_memLp_μ‖

Norm equality for Lp elements under measure change

theorem Frourio.lp_dist_measure_equiv {σ : ℝ} (f : ↥(Hσ σ)) (g : ℝ → ℂ) (f_Lp : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (hf_weightedMeasure : MeasureTheory.MemLp (Hσ.toFun f) 2 (weightedMeasure σ)) (hf_Lp_eq : f_Lp = MeasureTheory.MemLp.toLp (Hσ.toFun f) hf_weightedMeasure) (hg_memLp : MeasureTheory.MemLp g 2 (weightedMeasure σ)) (h_measure_eq : weightedMeasure σ = mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) : dist f (MeasureTheory.MemLp.toLp g ⋯) = dist f_Lp (MeasureTheory.MemLp.toLp g hg_memLp)

Distance equivalence under measure equality for Lp spaces

theorem Frourio.lp_approximation_triangle_chain {σ : ℝ} (f_Lp : ↥(MeasureTheory.Lp ℂ 2 (weightedMeasure σ))) (s : ↥(MeasureTheory.Lp.simpleFunc ℂ 2 (weightedMeasure σ))) (g_cont : ℝ → ℂ) (hg_cont_memLp : MeasureTheory.MemLp g_cont 2 (weightedMeasure σ)) (g : ℝ → ℂ) (hg_memLp : MeasureTheory.MemLp g 2 (weightedMeasure σ)) (ε : ℝ) (hs_close : dist f_Lp ↑s < ε / 2) (hg_cont_close : dist (↑s) (MeasureTheory.MemLp.toLp g_cont hg_cont_memLp) < ε / 4) (hg_mollify_close : dist (MeasureTheory.MemLp.toLp g_cont hg_cont_memLp) (MeasureTheory.MemLp.toLp g hg_memLp) < ε / 4) : dist f_Lp (MeasureTheory.MemLp.toLp g hg_memLp) < ε

Triangle inequality chain for Lp approximation sequence

theorem Frourio.smooth_compactSupport_dense_in_weightedL2 {σ : ℝ} (hσ_lower : 1 / 2 < σ) (_hσ_upper : σ < 3 / 2) (f : ↥(Hσ σ)) (ε : ℝ) (hε : 0 < ε) : ∃ (g : ℝ → ℂ) (hg_mem : MeasureTheory.MemLp g 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1)))), HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ dist f (MeasureTheory.MemLp.toLp g hg_mem) < ε

Smooth compactly supported functions are dense in weighted L² spaces for σ > 1/2

theorem Frourio.schwartz_dense_in_Hσ {σ : ℝ} (hσ_lower : 1 / 2 < σ) (hσ_upper : σ < 3 / 2) : DenseRange (schwartzToHσ hσ_lower)

Schwartz functions are dense in Hσ for σ > 1/2

theorem Frourio.exists_schwartz_approximation {σ : ℝ} (hσ_lower : 1 / 2 < σ) (hσ_upper : σ < 3 / 2) (f : ↥(Hσ σ)) (ε : ℝ) (hε : 0 < ε) : ∃ (φ : SchwartzMap ℝ ℂ), ‖schwartzToHσ hσ_lower φ - f‖ < ε

For any f ∈ Hσ and ε > 0, there exists a Schwartz function approximating f for σ > 1/2

theorem Frourio.schwartz_ae_dense {σ : ℝ} (hσ_lower : 1 / 2 < σ) (hσ_upper : σ < 3 / 2) (f : ↥(Hσ σ)) (ε : ℝ) (hε : 0 < ε) : ∃ (φ : SchwartzMap ℝ ℂ), ‖schwartzToHσ hσ_lower φ - f‖ < ε ∧ ↑↑(schwartzToHσ hσ_lower φ) =ᵐ[mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))] fun (x : ℝ) => if x > 0 then φ x else 0

Schwartz approximation with a.e. convergence for σ > 1/2