HeatReversePoincare.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The pointwise reverse Poincaré inequality for bounded L² data

theorem OAI.RegularPointCoordinates.integral_indicatorConstLp_mul line 17

Source documentation

Finite-measure indicators test a weighted integral without introducing an abstract duality hypothesis.

theorem integral_indicatorConstLp_mul (s : Set X) (hs : MeasurableSet s)
    (hfin : μ s ≠ ∞) (g : X → ℝ) :
    (∫ x, indicatorConstLp 2 hs hfin (1:ℝ) x*g x ∂μ) = ∫ x in s, g x ∂μ := by
…

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_reverse_poincare line 30
Source documentation
The actual heat flow satisfies reverse Poincaré almost everywhere. The right side is the heat flow of the actual L² square.
```
theorem NoncollapsedRCD.heat_reverse_poincare
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X) (p : X) :
    letI : ProperSpace X := hX.proper K n hn
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD