OAI/Geometry/RCD/Heat/HeatBoundedMeasurableTest.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_integral_measurable_lipschitz line 20

   Source documentation

   Compact exhaustion extends the quantitative smoothing bound to every bounded measurable test, including tests outside L².

   theorem heatRadonMeasure_integral_measurable_lipschitz (t : ℝ) (ht : 0 < t)
       (f : X → ℝ) (hf : Measurable f) (C : ℝ≥0) (hb : ∀ y, |f y| ≤ C) :
       LipschitzWith ⟨Real.sqrt ((C : ℝ) ^ 2 / (2 * t * Real.exp (-2 * |K| * t))),
         Real.sqrt_nonneg _⟩
         (fun x => ∫ y, f y ∂hX.heatRadonMeasure hn p t ht x) := by
   …