OAI/Geometry/RCD/Heat/HeatOverlapFinite.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finiteness of every heat overlap from actual L² smoothing

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_product_integrable line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatOverlapKernel_finite line 27

    Source documentation

    The extended overlap is finite at every pair, with no Gaussian premise.

    theorem heatOverlapKernel_finite (t : ℝ) (ht : 0 < t) (x y : X) :
    hX.heatOverlapKernel hn p t ht x y ≠ ∞ := by
…
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_eq_density_product line 41
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_memLp_two_unconditional line 52