OAI/Geometry/RCD/Sobolev/PoissonProjectionGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.poisson_projection_gradient line 19

   Source documentation

   A sharp L² bound for the actual two-center projection yields a harmonic Sobolev residual with the corresponding physical gradient bound.

   theorem poisson_projection_gradient {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
       (hgradient : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
       {P : ℝ} (hP : 0 < P) :
       ∃ Q : ℝ, 0 < Q ∧ ∀ {κ root B J C : ℝ} {first center : X}
         (S1 : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ first root)
         (S2 : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ center root)
         (T1 : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S1 B J C)
         (T2 : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S2 B J C) (i : ℕ),
         let s := distanceSourceRadius root i
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius