OAI/Geometry/RCD/Sobolev/CorrectionInteriorEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.localGamma_add_self_le line 16
2. theorem OAI.RegularPointCoordinates.sobolev_restrict_norm_sq line 29
3. theorem OAI.RegularPointCoordinates.correction_interior_energy line 41

   Source documentation

   The harmonic part is controlled by the interior gradient estimate; the zero-boundary correction retains its full energy budget. This supplies the radial W12 step without assuming bounded harmonic data.

   theorem correction_interior_energy {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) (hgradient : LocalHarmonicL2GradientInput hX)
       (hn : 2 ≤ n) {κ : ℝ} (hκ : 0 ≤ κ) :
       ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (R : ℝ), 0 < R → -κ ≤ K * R ^ 2 →
         ∀ (g h F : SobolevSpace (hausdorff n X) hX.quadratic),
         IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p R) h →
         IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p R) F →
         ∀ {D I J : ℝ},
         energyForm (hausdorff n X) hX.quadratic (g - h) (g - h) ≤ D →
         ‖SobolevSpace.restrictLp (hausdorff n X) hX.quadratic (ball p R) (g - F)‖ ^ 2 ≤ I →
         ‖SobolevSpace.toLp (hausdorff n X) hX.quadratic (g - h)‖ ^ 2 ≤ J →
         (∫ x in ball p (R / 2), localGamma (hausdorff n X) hX.quadratic (g - F) (g - F) x
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma