BoundedPoissonLipschitz.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded weak Laplacians give Lipschitz representatives

The proof pairs the actual heat flow with normalized ball indicators. Its derivative is the heat flow of the weak Laplacian. Integrating the inverse-square-root smoothing estimate and taking small-ball averages produces the representative; no pointwise time derivative is assumed.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_average_difference_le line 22

Source documentation

Spatial differences of heat averages, with the outer time held fixed.

theorem NoncollapsedRCD.heat_average_difference_le
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    (f : Lp ℝ 2 (hausdorff n X)) (C : ℝ≥0)
    (hf : ∀ᵐ x ∂hausdorff n X, |f x| ≤ C)
    (t T : ℝ) (ht : 0 < t) (htT : t ≤ T) (x y : X) (r : ℝ) (hr : 0 < r) :
    |(⨍ z in closedBall x r, heatAt (hausdorff n X) hX.quadratic t f z ∂hausdorff n X)-
      (⨍ z in closedBall y r, heatAt (hausdorff n X) hX.quadratic t f z ∂hausdorff n X)| ≤
      (C*Real.exp (|K| *T)/Real.sqrt t)*(dist x y+2*r) := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.heatAt

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_weakLaplacian_lipschitz line 42

Source documentation

A global bounded Poisson solution has a quantitative Lipschitz representative at every chosen positive time scale.

theorem NoncollapsedRCD.bounded_weakLaplacian_lipschitz
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X)
    (u : SobolevSpace (hausdorff n X) hX.quadratic) (d : Lp ℝ 2 (hausdorff n X))
    (hd : IsWeakLaplacian (hausdorff n X) hX.quadratic u d)
    (C D : ℝ≥0) (hu : ∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp _ _ u x| ≤ C)
    (hdB : ∀ᵐ x ∂hausdorff n X, |d x| ≤ D) (T : ℝ) (hT : 0 < T) :
    ∃ v : X → ℝ,
      LipschitzWith ⟨Real.exp (|K| *T)*(C/Real.sqrt T+2*D*Real.sqrt T),by positivity⟩ v ∧
      SobolevSpace.toLp (hausdorff n X) hX.quadratic u =ᵐ[hausdorff n X] v := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp