HeatTransitionPointwise.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Pointwise bounds for actual heat transition probabilities

Spatial strong Feller smoothing converts the separated-set Davies estimate to a bound at each starting point. The localization radius remains free, so it can be optimized later using the established volume comparison.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_set_lipschitz line 23

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_pointwise_separated line 35

Source documentation

A pointwise transition bound derived without a pointwise kernel estimate.

theorem heatRadonMeasure_pointwise_separated (t : ℝ) (ht : 0 < t)
    {A : Set X} (hA : MeasurableSet A) (hAf : hausdorff n X A ≠ ∞)
    (q x : X) {r δ : ℝ} (hδ : 0 < δ) (hsep : r + δ ≤ dist q x)
    (hnear : ∀ y ∈ A, dist q y ≤ r) :
    (hX.heatRadonMeasure hn p t ht x).real A ≤
      Real.sqrt (1 / (2*t*Real.exp (-2*|K| * t))) * δ +
        Real.exp (-((dist q x-δ)-r)^2 / (4*t)) * Real.sqrt ((hausdorff n X).real A) /
          Real.sqrt ((hausdorff n X).real (ball x δ)) := by
…

Mentions: OAI.RegularPointCoordinates.hausdorff