OAI/Geometry/RCD/Sobolev/HarmonicInteriorEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput.interior_energy line 18

   Source documentation

   Normalizing the outer L² norm gives a uniform scaled energy bound on every fixed inner fraction. The function need not be bounded pointwise.

   theorem LocalHarmonicL2GradientInput.interior_energy {K : ℝ} {n : ℕ}
       {hX : NoncollapsedRCD K n X} (hinput : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
       {a τ : ℝ} (ha : 0 ≤ a) (hτ : 0 < τ) (hτ1 : τ < 1) :
       ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (R : ℝ), ∀ _hR : 0 < R, -a ≤ K * R ^ 2 →
         ∀ w : SobolevSpace (hausdorff n X) hX.quadratic,
           IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p R) w →
           ‖normalizeLocalL2 (hausdorff n X) (ball p R)
             (ne_of_lt (hX.finiteOnBounded _ isBounded_ball))
             (SobolevSpace.restrictLp (hausdorff n X) hX.quadratic (ball p R) w)‖ ≤ 1 →
           R ^ 2 * ((hausdorff n X).real (ball p R))⁻¹ *
             (∫ x in ball p (τ * R), localGamma (hausdorff n X) hX.quadratic w w x
               ∂hausdorff n X) ≤ C ^ 2 := by
   …

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