TransportPoincare.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The local L² Poincare estimate from RCD transport

The two median level sets are transported to their larger opposite sets. The normalization cancels from the compression bound and only energy in the eightfold ball remains.

theorem OAI.RegularPointCoordinates.measure_sdiff_le_inter_of_half line 21
theorem OAI.RegularPointCoordinates.split_level_integral line 31

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_mean_poincare_transport line 75

Source documentation

The direct transport estimate before replacing its curvature factor by a constant depending only on the rescaled lower curvature bound.

theorem NoncollapsedRCD.local_mean_poincare_transport
    {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    (p : X) {R : ℝ} (hR : 0 < R)
    {u G : Lp ℝ 2 (hausdorff n X)} (hG : IsRelaxedSlope (hausdorff n X) u G) :
    ∃ k : ℝ, (∫ x in ball p R, (u x - k) ^ 2 ∂hausdorff n X) ≤
      2 * ((2 * R) ^ 2 * Real.exp ((n : ℝ) * (4 * R) * Real.sqrt (|K| / (n - 1))) *
        (∫ x in ball p (8 * R), (G x) ^ 2 ∂hausdorff n X)) := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsRelaxedSlope

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.localMeanPoincareInput line 113
Source documentation
The local Poincare bound obtained from bounded-compression RCD transport.
```
theorem NoncollapsedRCD.localMeanPoincareInput {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [ProperSpace X] (hn : 2 ≤ n) :
    LocalMeanPoincareInput hX := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalMeanPoincareInput