theorem Newton.continuous_compactSupport_dense_Lp {n : ℕ} (p : ENNReal) (hp_ne_top : p ≠ ⊤) (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) {ε : ℝ} (hε : 0 < ε) : ∃ (g : (Fin n → ℝ) → ℂ), Continuous g ∧ HasCompactSupport g ∧ MeasureTheory.MemLp g p MeasureTheory.volume ∧ MeasureTheory.eLpNorm (f - g) p MeasureTheory.volume < ENNReal.ofReal ε

Continuous compactly supported functions are dense in Lp.

For any f ∈ Lp(ℝⁿ) with 1 ≤ p < ∞ and any ε > 0, there exists a continuous function g with compact support such that ‖f - g‖_p < ε.

theorem Newton.tsupport_subset_closedBall {n : ℕ} (g : (Fin n → ℝ) → ℂ) (hg_compact : HasCompactSupport g) : ∃ (R : ℝ), tsupport g ⊆ Metric.closedBall 0 R ∧ 1 ≤ R

Any compactly supported function has its topological support contained in some closed ball of radius at least 1.

theorem Newton.eLpNorm_triangle_ineq_lt {n : ℕ} {g φ₀ ψ : (Fin n → ℝ) → ℂ} (p : ENNReal) (hp_one : 1 ≤ p) (hg_cont : Continuous g) (hφ₀_smooth : ContDiff ℝ (↑⊤) φ₀) (hψ_cont : Continuous ψ) {ε : ℝ} (h_term_support : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => g x - φ₀ x) p MeasureTheory.volume < ENNReal.ofReal (ε / 2)) (h_term_cutoff : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => φ₀ x - ψ x) p MeasureTheory.volume < ENNReal.ofReal (ε / 2)) (hε_half : 0 < ε / 2) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => g x - ψ x) p MeasureTheory.volume < ENNReal.ofReal ε

theorem Newton.phi0_eq_zero_outside_enlarged_ball {n : ℕ} (φ₀ : (Fin n → ℝ) → ℂ) (R : ℝ) (h_support : tsupport φ₀ ⊆ Metric.closedBall 0 (R + 1)) ⦃x : Fin n → ℝ⦄ : R + 1 < ‖x‖ → φ₀ x = 0

theorem Newton.mollifier_compactSupport_Lp_approx {n : ℕ} (p : ENNReal) (hp_one : 1 ≤ p) (g : (Fin n → ℝ) → ℂ) (hg_cont : Continuous g) (hg_compact : HasCompactSupport g) {ε : ℝ} (hε : 0 < ε) : ∃ (φ : (Fin n → ℝ) → ℂ), ContDiff ℝ (↑⊤) φ ∧ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => g x - φ x) p MeasureTheory.volume < ENNReal.ofReal ε ∧ MeasureTheory.MemLp φ p MeasureTheory.volume

Approximating a continuous compactly supported function by a smooth function in Lᵖ.

theorem Newton.smooth_cutoff_compactSupport_Lp_aux {n : ℕ} (p : ENNReal) (hp_one : 1 ≤ p) (g : (Fin n → ℝ) → ℂ) (hg_cont : Continuous g) (hg_compact : HasCompactSupport g) {ε : ℝ} (hε : 0 < ε) : ∃ (ψ : (Fin n → ℝ) → ℂ), ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ MeasureTheory.MemLp ψ p MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => g x - ψ x) p MeasureTheory.volume < ENNReal.ofReal ε

Auxiliary lemma: smoothly cut off a continuous compactly supported function while keeping control of the Lᵖ error.

theorem Newton.smooth_cutoff_compactSupport_Lp {n : ℕ} (p : ENNReal) (hp_one : 1 ≤ p) (hp_ne_top : p ≠ ⊤) (φ : (Fin n → ℝ) → ℂ) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (hφ_memLp : MeasureTheory.MemLp φ p MeasureTheory.volume) {R : ℝ} (hR_pos : 0 < R) {ε : ℝ} (hε : 0 < ε) : ∃ (ψ : (Fin n → ℝ) → ℂ), ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ MeasureTheory.MemLp ψ p MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => φ x - ψ x) p MeasureTheory.volume < ENNReal.ofReal ε

Cutting off a smooth function so that it has compact support while keeping control of the Lᵖ error.

theorem Newton.smooth_compactSupport_to_schwartz {n : ℕ} (g : (Fin n → ℝ) → ℂ) (hg_smooth : ContDiff ℝ (↑⊤) g) (hg_support : HasCompactSupport g) : ∃ (φ : SchwartzMap (Fin n → ℝ) ℂ), ⇑φ = g

Smooth compactly supported functions are Schwartz.

theorem Newton.integrable_tail_small {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.MemLp f 1 MeasureTheory.volume) {ε : ℝ} (hε : 0 < ε) : ∃ R > 0, ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | R ≤ ‖x‖}, ‖f x‖ < ε

Tail estimate for integrable functions on ℝⁿ (placeholder).

theorem Newton.tail_bound_mono {n : ℕ} (F : (Fin n → ℝ) → ℝ) {R₁ R₂ ε : ℝ} (hR : R₁ ≤ R₂) (h_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ F x) (h_int : MeasureTheory.Integrable F (MeasureTheory.volume.restrict {x : Fin n → ℝ | R₁ ≤ ‖x‖})) (h_bound : ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | R₁ ≤ ‖x‖}, F x < ε) : ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | R₂ ≤ ‖x‖}, F x < ε

Monotonicity of tail integrals with respect to the radius (placeholder).