AnnularHeatLipschitz.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Interior Lipschitz control for heat flow of an annular source

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.annular_heat_difference line 19

Source documentation

A source supported away from an interior ball has a uniformly Lipschitz heat evolution there, all the way down to arbitrarily small positive time.

theorem NoncollapsedRCD.annular_heat_difference {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2 ≤ n)
    {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker)
    (hg : HasCoordinateHeatBounds (hausdorff n X) ker) :
    ∃ J : ℝ, 0 < J ∧ ∀ (p : X) (R t : ℝ), 0 < R → -1 ≤ K*R^2 →
      0 < t → t ≤ 1 → t ≤ R^2 →
      ∀ q : Lp ℝ 2 (hausdorff n X), Integrable q (hausdorff n X) →
      (∀ᵐ z ∂hausdorff n X, q z ≠ 0 → R ≤ dist z p ∧ dist z p ≤ 2*R) →
      ∀ x y : X, dist x p ≤ R/8 → dist y p ≤ R/8 →
      |kernelHeat (hausdorff n X) hX.quadratic hk t q x-
        kernelHeat (hausdorff n X) hX.quadratic hk t q y| ≤
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.kernelHeat