theorem Newton.exists_smooth_cutoff {n : ℕ} (r R : ℝ) (hr : 0 < r) (hR : r < R) : ∃ (χ : (Fin n → ℝ) → ℝ), ContDiff ℝ (↑⊤) χ ∧ (∀ (x : Fin n → ℝ), ‖x‖ ≤ r → χ x = 1) ∧ (∀ (x : Fin n → ℝ), 0 ≤ χ x ∧ χ x ≤ 1) ∧ HasCompactSupport χ ∧ tsupport χ ⊆ Metric.closedBall 0 R

theorem Newton.triangle_inequality_aux {n : ℕ} (f g h : (Fin n → ℝ) → ℂ) (ε ε₁ ε₂ ε₃ : ℝ) (hf_meas : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hg_meas : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hh_meas : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) (hf : MeasureTheory.eLpNorm f 1 MeasureTheory.volume < ENNReal.ofReal ε₁) (hg : MeasureTheory.eLpNorm g 1 MeasureTheory.volume < ENNReal.ofReal ε₂) (hh : MeasureTheory.eLpNorm h 1 MeasureTheory.volume < ENNReal.ofReal ε₃) (h_sum : ε₁ + ε₂ + ε₃ ≤ ε) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x + g x + h x) 1 MeasureTheory.volume < ENNReal.ofReal ε

theorem Newton.exists_mollifier_scale {n : ℕ} (f₀ : (Fin n → ℝ) → ℂ) (hf₀_L1 : MeasureTheory.MemLp f₀ 1 MeasureTheory.volume) (hf₀_L2 : MeasureTheory.MemLp f₀ 2 MeasureTheory.volume) (ε₁ ε₂ : ℝ) (hε₁ : 0 < ε₁) (hε₂ : 0 < ε₂) : ∃ (η : ℝ) (_ : 0 < η) (_ : η ≤ 1) (ψ : (Fin n → ℝ) → ℝ), ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ ∫ (x : Fin n → ℝ), ψ x = 1 ∧ (∀ (x : Fin n → ℝ), 0 ≤ ψ x) ∧ tsupport ψ ⊆ Metric.closedBall 0 1 ∧ have ψ_η := fun (x : Fin n → ℝ) => η ^ (-↑n) * ψ fun (i : Fin n) => x i / η; have φ := fun (x : Fin n → ℝ) => ∫ (y : Fin n → ℝ), f₀ (x - y) * ↑(ψ_η y); MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f₀ x - φ x) 1 MeasureTheory.volume < ENNReal.ofReal ε₁ ∧ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f₀ x - φ x) 2 MeasureTheory.volume < ENNReal.ofReal ε₂

theorem Newton.cutoff_L1_bound {n : ℕ} (f f_cut : (Fin n → ℝ) → ℂ) (hf_L1 : MeasureTheory.MemLp f 1 MeasureTheory.volume) (χ : (Fin n → ℝ) → ℝ) (R ε_tail₁ : ℝ) (hχ_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ χ x) (hχ_le_one : ∀ (x : Fin n → ℝ), χ x ≤ 1) (hf_cut_def : f_cut = fun (x : Fin n → ℝ) => ↑(χ x) * f x) (h_diff_zero_inside : ∀ {x : Fin n → ℝ}, ‖x‖ ≤ R → f x - f_cut x = 0) (hf_tail_L1 : ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | R ≤ ‖x‖}, ‖f x‖ < ε_tail₁) (htail₁ : 0 < ε_tail₁) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - f_cut x) 1 MeasureTheory.volume ≤ ENNReal.ofReal ε_tail₁

theorem Newton.cutoff_L2_bound {n : ℕ} (f f_cut : (Fin n → ℝ) → ℂ) (χ : (Fin n → ℝ) → ℝ) (R ε_tail₂ : ℝ) (hχ_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ χ x) (hχ_le_one : ∀ (x : Fin n → ℝ), χ x ≤ 1) (hf_cut_def : f_cut = fun (x : Fin n → ℝ) => ↑(χ x) * f x) (h_diff_zero_inside : ∀ {x : Fin n → ℝ}, ‖x‖ ≤ R → f x - f_cut x = 0) (hf_tail_L2 : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x) 2 (MeasureTheory.volume.restrict {x : Fin n → ℝ | R ≤ ‖x‖}) < ENNReal.ofReal ε_tail₂) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - f_cut x) 2 MeasureTheory.volume ≤ ENNReal.ofReal ε_tail₂

theorem Newton.cutoff_then_convolve_Lp {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_L1 : MeasureTheory.MemLp f 1 MeasureTheory.volume) (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (R : ℝ) (hR : 0 < R) {ε ε_cut₁ ε_cut₂ ε_tail₁ ε_tail₂ : ℝ} (hε : 0 < ε) (hcut₁ : 0 < ε_cut₁) (hcut₂ : 0 < ε_cut₂) (htail₁ : 0 < ε_tail₁) (htail₂ : 0 < ε_tail₂) (h_budget_L1 : ε_cut₁ + ε_tail₁ < ε) (h_budget_L2 : ε_cut₂ + ε_tail₂ < ε) (hf_tail_L1 : ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | R ≤ ‖x‖}, ‖f x‖ < ε_tail₁) (hf_tail_L2 : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x) 2 (MeasureTheory.volume.restrict {x : Fin n → ℝ | R ≤ ‖x‖}) < ENNReal.ofReal ε_tail₂) : ∃ (φ : SchwartzMap (Fin n → ℝ) ℂ), tsupport ⇑φ ⊆ Metric.closedBall 0 (R + 3) ∧ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - φ x) 1 MeasureTheory.volume < ENNReal.ofReal ε ∧ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - φ x) 2 MeasureTheory.volume < ENNReal.ofReal ε

theorem Newton.schwartz_dense_L1_L2_simultaneous {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_L1 : MeasureTheory.MemLp f 1 MeasureTheory.volume) (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) {ε : ℝ} (hε : 0 < ε) : ∃ (φ : SchwartzMap (Fin n → ℝ) ℂ), MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - φ x) 1 MeasureTheory.volume < ENNReal.ofReal ε ∧ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - φ x) 2 MeasureTheory.volume < ENNReal.ofReal ε

theorem Newton.smooth_cutoff_compactSupport_Lp_real (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (hφ_memLp : MeasureTheory.MemLp φ 2 MeasureTheory.volume) {R : ℝ} (hR_pos : 0 < R) {ε : ℝ} (hε : 0 < ε) : ∃ (g : ℝ → ℂ), ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ MeasureTheory.MemLp g 2 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (t : ℝ) => φ t - g t) 2 MeasureTheory.volume < ENNReal.ofReal ε

Variant for ℝ (n=1 case) with simultaneous L¹ and L² control.

This is the specific instance needed for the Plancherel theorem on ℝ.

theorem Newton.smooth_cutoff_compactSupport_L1_L2_real (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (hφ_memLp₁ : MeasureTheory.MemLp φ 1 MeasureTheory.volume) (hφ_memLp₂ : MeasureTheory.MemLp φ 2 MeasureTheory.volume) {R : ℝ} (hR_pos : 0 < R) {ε : ℝ} (hε : 0 < ε) : ∃ (g : ℝ → ℂ), ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ MeasureTheory.MemLp g 2 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (t : ℝ) => φ t - g t) 1 MeasureTheory.volume < ENNReal.ofReal ε ∧ MeasureTheory.eLpNorm (fun (t : ℝ) => φ t - g t) 2 MeasureTheory.volume < ENNReal.ofReal ε

theorem Newton.smooth_compactSupport_dense_L1_L2_real (f : ℝ → ℂ) (hf_L1 : MeasureTheory.Integrable f MeasureTheory.volume) (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) {ε : ℝ} (hε : 0 < ε) : ∃ (g : ℝ → ℂ), ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ MeasureTheory.eLpNorm (f - g) 1 MeasureTheory.volume < ENNReal.ofReal ε ∧ MeasureTheory.eLpNorm (f - g) 2 MeasureTheory.volume < ENNReal.ofReal ε