MollifierCkRoute

formal source

 244kernels with shrinking support. This is *infrastructure only* — the
 245analytic blocker is uniform compact-set derivative bounds on
 246`mollified G (φ n)`, not the existence of the bump family. -/
 247def MollifierCkRoute : Prop :=
 248  ∃ (φ : ℕ → ContDiffBump (0 : ℝ)),
 249    Filter.Tendsto (fun n => (φ n).rOut) Filter.atTop (nhds 0)
 250
 251set_option maxHeartbeats 400000 in
 252/-- Existence of a shrinking-support bump family on `ℝ`. -/
 253theorem mollifierCkRoute_exists : MollifierCkRoute := by
 254  classical
 255  refine ⟨fun n => ?_, ?_⟩
 256  · refine
 257      { rIn := (1 : ℝ) / (2 * ((n : ℝ) + 1))
 258        rOut := (1 : ℝ) / ((n : ℝ) + 1)
 259        rIn_pos := by positivity
 260        rIn_lt_rOut := by
 261          have hn : (0 : ℝ) < ((n : ℝ) + 1) := by
 262            have : (0 : ℝ) ≤ (n : ℝ) := by exact_mod_cast Nat.zero_le n
 263            linarith
 264          have hlt : ((n : ℝ) + 1) < 2 * ((n : ℝ) + 1) := by linarith
 265          exact one_div_lt_one_div_of_lt hn hlt }
 266  · -- (1 : ℝ) / ((n : ℝ) + 1) → 0
 267    have h : Filter.Tendsto (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1)) Filter.atTop (nhds 0) :=
 268      tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ)
 269    simpa using h
 270
 271/-! ## 3. Promoting polynomial to continuous
 272
 273The polynomial case is a special case of the continuous case. Concretely,
 274any polynomial of total degree at most two on `ℝ × ℝ` is continuous, so
 275`SatisfiesLawsOfLogic ⊆ SatisfiesLawsOfLogicContinuous`. -/
 276
 277private theorem polynomial_continuous