OAI/Geometry/RCD/Sobolev/RadialInteriorEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.radial_interior_energy_from_fit line 18

   Source documentation

   Weak radial cancellation and its actual Dirichlet correction upgrade an L2 fit to an interior gradient fit. The source is the same shifted Hessian budget already used for the radial value estimates.

   theorem radial_interior_energy_from_fit {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 →
         ∀ (f a : SobolevSpace (hausdorff n X) hX.quadratic)
           (G : LocalHessianPairing (hausdorff n X) hX.quadratic (ball p R) f a),
         ∀ {c P D : ℝ},
         IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p R) f c →
         IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p R) a →
         0 ≤ P → 0 ≤ D →
         (∀ φ : SobolevSpace.dirichlet (hausdorff n X) hX.quadratic (ball p R),
           ‖SobolevSpace.toLp (hausdorff n X) hX.quadratic φ.val‖ ^ 2 ≤
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp