OAI/Geometry/RCD/Heat/HeatBoundedContinuousTest.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Spatial Lipschitz continuity of bounded continuous heat tests

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compactHeatEval_lipschitz line 18
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_integral_lipschitz line 31

    Source documentation

    The same quantitative smoothing applies to bounded continuous data that need not be globally square integrable.

    theorem heatRadonMeasure_integral_lipschitz (t : ℝ) (ht : 0 < t) (f : X →ᵇ ℝ) :
    LipschitzWith ⟨Real.sqrt (‖f‖ ^ 2 / (2 * t * Real.exp (-2 * |K| * t))), Real.sqrt_nonneg _⟩
      (fun x => ∫ y, f y ∂hX.heatRadonMeasure hn p t ht x) := by
…