HeatTransitionDecay.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Gaussian decay of the actual transition mass between separated sets

The estimate is a consequence of the weighted Cheeger semigroup bound.

theorem OAI.RegularPointCoordinates.indicatorConstLp_norm_eq_sqrt line 19
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_set_pair line 32

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_separated_sets line 57

Source documentation

The sharp Davies exponent for transition mass between a source set inside a ball and an observation set outside a larger concentric ball.

theorem heatRadonMeasure_separated_sets (t : ℝ) (ht : 0 < t)
    {A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B)
    (hAf : hausdorff n X A ≠ ∞) (hBf : hausdorff n X B ≠ ∞)
    (q : X) {r R : ℝ} (hnear : ∀ x ∈ A, dist q x ≤ r)
    (hfar : ∀ x ∈ B, R ≤ dist q x) (hrR : r ≤ R) :
    (∫ x in B, (hX.heatRadonMeasure hn p t ht x).real A ∂hausdorff n X) ≤
      Real.exp (-(R-r)^2 / (4*t)) *
        Real.sqrt ((hausdorff n X).real A) * Real.sqrt ((hausdorff n X).real B) := by
…

Mentions: OAI.RegularPointCoordinates.hausdorff