HeatDetailedBalance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Detailed balance from the self-adjoint Cheeger semigroup

theorem OAI.RegularPointCoordinates.indicatorConstLp_abs_le_one line 15

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_pair line 29

Source documentation

The constructed measure preserves the self-adjoint pairing on bounded square-integrable data.

theorem heatRadonMeasure_pair (t : ℝ) (ht : 0 < t)
    (f g : Lp ℝ 2 (hausdorff n X)) (Cf Cg : ℝ≥0)
    (hf : ∀ᵐ y ∂hausdorff n X, |f y| ≤ Cf)
    (hg : ∀ᵐ y ∂hausdorff n X, |g y| ≤ Cg) :
    (∫ x, f x * (∫ y, g y ∂hX.heatRadonMeasure hn p t ht x) ∂hausdorff n X) =
      ∫ y, g y * (∫ x, f x ∂hX.heatRadonMeasure hn p t ht y) ∂hausdorff n X := by
…

Mentions: OAI.RegularPointCoordinates.hausdorff

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_integral_indicator line 52

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_set_balance line 61

Source documentation

Transition mass between finite-volume sets is symmetric.

theorem heatRadonMeasure_set_balance (t : ℝ) (ht : 0 < t)
    {s u : Set X} (hs : MeasurableSet s) (hu : MeasurableSet u)
    (hfs : hausdorff n X s ≠ ∞) (hfu : hausdorff n X u ≠ ∞) :
    (∫ x in s, (hX.heatRadonMeasure hn p t ht x).real u ∂hausdorff n X) =
      ∫ y in u, (hX.heatRadonMeasure hn p t ht y).real s ∂hausdorff n X := by
…

Mentions: OAI.RegularPointCoordinates.hausdorff