OAI/Geometry/RCD/Harmonic/HarmonicCorrection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.exists_harmonic_correction line 20

   Source documentation

   A bound for the energy-dual defect gives a harmonic correction with that energy bound and the corresponding Poincare L² bound. This is the functional step in the manuscript's radial harmonic correction.

   theorem exists_harmonic_correction (Ω : Set X) {P D : ℝ}
       (hP : 0 ≤ P) (hD : 0 ≤ D)
       (hbound : ∀ f : SobolevSpace.dirichlet μ hQ Ω,
         ‖SobolevSpace.toLp μ hQ f.val‖ ^ 2 ≤ P * energyForm μ hQ f.val f.val)
       (g : SobolevSpace μ hQ)
       (hdefect : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
         (energyForm μ hQ g φ.val) ^ 2 ≤ D * energyForm μ hQ φ.val φ.val) :
       ∃ h : SobolevSpace μ hQ, g - h ∈ SobolevSpace.dirichlet μ hQ Ω ∧
         IsSobolevHarmonicOn μ hQ Ω h ∧
         energyForm μ hQ (g - h) (g - h) ≤ D ∧
         ‖SobolevSpace.toLp μ hQ (g - h)‖ ^ 2 ≤ P * D := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn