TransportLevelBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local level-set bound from the actual RCD transport plan

Transport from a superlevel set to a sublevel set controls the squared distance to their common level. Only energy in the enlarged ball occurs.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.level_integral_bound line 20

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.balanced_level_integral_bound line 105

Source documentation

When the opposite level set has at least as much mass, normalization of the transport plan cancels exactly from the estimate.

theorem NoncollapsedRCD.balanced_level_integral_bound
    {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    (p : X) {R : ℝ} (hR : 0 < R) {A B : Set X}
    (hA : MeasurableSet A) (hB : MeasurableSet B)
    (hsA : A ⊆ closedBall p R) (hsB : B ⊆ closedBall p R)
    (hAB : hausdorff n X A ≤ hausdorff n X B)
    {u G : Lp ℝ 2 (hausdorff n X)} (hG : IsRelaxedSlope (hausdorff n X) u G)
    (k : ℝ) (hlevel : ∀ x ∈ A, ∀ y ∈ B, (u x - k) ^ 2 ≤ (u y - u x) ^ 2) :
    (∫ x in A, (u x - k) ^ 2 ∂hausdorff n X) ≤
      (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