UniformLipschitzL2Limit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform Lipschitz bounds turn L² convergence into pointwise convergence

theorem OAI.RegularPointCoordinates.tendsto_zero_of_uniform_lipschitz_l2 line 16

Source documentation

A fixed positive ball witnesses every persistent nonzero value.

theorem tendsto_zero_of_uniform_lipschitz_l2 (μ : Measure X) [ProperSpace X]
    [IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure]
    (u : ℕ → Lp ℝ 2 μ) (v : ℕ → X → ℝ) (L : ℝ≥0)
    (hrep : ∀ i, u i =ᵐ[μ] v i) (hLip : ∀ i, LipschitzWith L (v i))
    (hlim : Tendsto (fun i => ‖u i‖) atTop (𝓝 0)) (x : X) :
    Tendsto (fun i => v i x) atTop (𝓝 0) := by
…

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundedHeat_tendsto_zero line 54

Source documentation

Uniformly bounded L² data tending to zero have heat values tending to zero at every point. The proof uses no kernel estimate.

theorem boundedHeat_tendsto_zero (f : ℕ → Lp ℝ 2 (hausdorff n X)) (C : ℝ≥0)
    (hf : ∀ i, ∀ᵐ x ∂hausdorff n X, |f i x| ≤ C)
    (hlim : Tendsto f atTop (𝓝 0)) (t : ℝ) (ht : 0 < t) (x : X) :
    Tendsto (fun i => hX.boundedHeat hn p (f i) ⟨C, hf i⟩ t ht x) atTop (𝓝 0) := by
…

Mentions: OAI.RegularPointCoordinates.hausdorff