OAI/Geometry/RCD/Transport/ActualRadialTransportDefect.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.positiveSquaredDistance_inward_smaller line 21

   Source documentation

   The compact squared-distance datum has the exact inward pairing on every smaller ball.

   theorem positiveSquaredDistance_inward_smaller {p : X} {R r C : ℝ}
       (hR : 0 ≤ R) (hrR : r ≤ R) (χ : GoodLaplacianCutoff μ hQ p R C)
       (heik : ∀ᵐ x ∂μ.restrict (ball p R),
         localGamma μ hQ (inwardSobolev μ hQ p R) (inwardSobolev μ hQ p R) x = 1) :
       localGamma μ hQ (positiveSquaredDistance μ hQ hR χ) (inwardSobolev μ hQ p r) =ᵐ[
         μ.restrict (ball p r)] fun x => -dist p x := by
   …

   Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.inwardSobolev, OAI.RegularPointCoordinates.positiveSquaredDistance

2. theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.radial_transport_defect line 39

   Source documentation

   The error is an actual square-integrable gradient pairing. Its full L2 mass is bounded by the same source energy, even across the transport cutoff. The radial identity is asserted only inside that cutoff.

   theorem DyadicDistanceReplacements.radial_transport_defect
       {n : ℕ} {κ r0 B J C : ℝ} {p : X}
       {S : DyadicDistanceSources μ hQ n κ p r0}
       (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
       {R : ℝ} (_hR : 0 < R) (hroom : 3 * R ≤ 4 * distanceSourceRadius r0 i) :
       ∃ g : X → ℝ, MemLp g 2 μ ∧
         (localGamma μ hQ (T.replacement i) (inwardSobolev μ hQ p (3 * R)) =ᵐ[
           μ.restrict (ball p (3 * R))] fun x => g x - dist p x) ∧
         (∫ x in ball p (4 * R), (g x) ^ 2 ∂μ) ≤
           (S.source i).real (ball p (distanceSourceRadius r0 i)) *
             (B * (distanceSourceRadius r0 i) ^ 2) := by
   …

   Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.inwardSobolev