Mollifier existence, rescale technicalities, and Bridge Lemma 1

Smooth compactly supported infrastructure on ℝⁿ:

Main contents

• mollifier_exists — there exists ψ ∈ C^∞_c(ℝⁿ; ℝ) with ψ ≥ 0, ∫ ψ = 1, and supp(ψ) ⊂ (-π, π)ⁿ.
• rescale_hasCompactSupport, rescale_contDiff, rescale_support_in_cube — rescale n φ ε preserves compact support, smoothness, and the cube-support condition.
• ftRn_at_zero — ftRn n φ 0 = ∫ φ.
• cinfty_rapidDecay (Bridge Lemma 1) — for φ ∈ C^∞_c(ℝⁿ; ℂ), FTRapidDecay n φ holds.
• convDistrib_memSobolevDistrib — convDistrib n φ u ∈ H^s_* whenever φ is integrable and u ∈ H^s_*.

Mollifier existence

theorem NashEmbedding.Sobolev.mollifier_exists {n : ℕ} : ∃ (ψ : (Fin n → ℝ) → ℝ), ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ MeasureTheory.Integrable ψ MeasureTheory.volume ∧ (∀ (x : Fin n → ℝ), 0 ≤ ψ x) ∧ (∀ (x : Fin n → ℝ), ψ x ≠ 0 → ∀ (j : Fin n), |x j| < Real.pi) ∧ ∫ (x : Fin n → ℝ), ψ x = 1

Rescale technicalities

theorem NashEmbedding.Sobolev.rescale_hasCompactSupport {n : ℕ} {φ : (Fin n → ℝ) → ℂ} (hsupp : HasCompactSupport φ) {ε : ℝ} (hε : 0 < ε) : HasCompactSupport (rescale n φ ε)

theorem NashEmbedding.Sobolev.rescale_contDiff {n : ℕ} {φ : (Fin n → ℝ) → ℂ} (hsmooth : ContDiff ℝ (↑⊤) φ) (ε : ℝ) : ContDiff ℝ (↑⊤) (rescale n φ ε)

theorem NashEmbedding.Sobolev.rescale_support_in_cube {n : ℕ} {φ : (Fin n → ℝ) → ℂ} (hsupp : ∀ (x : Fin n → ℝ), φ x ≠ 0 → ∀ (j : Fin n), |x j| < Real.pi) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (x : Fin n → ℝ) : rescale n φ ε x ≠ 0 → ∀ (j : Fin n), |x j| < Real.pi

theorem NashEmbedding.Sobolev.ftRn_at_zero {n : ℕ} (φ : (Fin n → ℝ) → ℂ) : ftRn n φ 0 = ∫ (y : Fin n → ℝ), φ y

Bridge Lemma 1: C^∞_c ⟹ FTRapidDecay

The statement and proof now live in NashEmbedding/Sobolev/IntegrationByParts.lean alongside the ftRn-side IBP infrastructure it depends on. Downstream callers still see NashEmbedding.Sobolev.cinfty_rapidDecay through this file's transitive re-export.

MemSobolevDistrib closure for convDistrib

theorem NashEmbedding.Sobolev.convDistrib_memSobolevDistrib {n : ℕ} {φ : (Fin n → ℝ) → ℂ} (hφ : MeasureTheory.Integrable φ MeasureTheory.volume) {s : ℝ} {u : TrigPolyDual n} (hu : MemSobolevDistrib n s u) : MemSobolevDistrib n s (convDistrib n φ u)