WeakRadialCancellation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Weak radial cancellation and its harmonic correction

The local Hessian test formula is equation (3.1.10) in Gigli (2018). The cancellation itself is proved here: constant Laplacian and harmonicity make the two integration-by-parts terms vanish, and continuity extends the identity from the regular test core to the actual Dirichlet space.

theorem OAI.RegularPointCoordinates.integral_localGamma_dirichlet line 27
Source documentation
Integrating a local gradient pairing with a zero-boundary function gives the full Dirichlet pairing. Locality removes the complement.
```
theorem integral_localGamma_dirichlet (Ω : Set X) (hΩ : MeasurableSet Ω)
    (f : SobolevSpace μ hQ) (φ : SobolevSpace.dirichlet μ hQ Ω) :
    (∫ x in Ω, localGamma μ hQ f φ.val x ∂μ) = energyForm μ hQ f φ.val := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.energyForm
structure OAI.RegularPointCoordinates.LocalHessianPairing line 42
Source documentation
A local Hessian pairing with one fixed gradient. All functions in the Koszul formula are genuine Sobolev functions. The regular test core is dense in the zero-boundary Sobolev space.
```
structure LocalHessianPairing (Ω : Set X) (f a : SobolevSpace μ hQ) where
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.LocalHessianPairing.weak_cancellation line 61
Source documentation
The Hessian formula implies weak radial cancellation.
```
theorem weak_cancellation {Ω : Set X} (hΩ : MeasurableSet Ω)
    {f a : SobolevSpace μ hQ} (G : LocalHessianPairing μ hQ Ω f a)
    {c : ℝ} (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (ha : IsSobolevHarmonicOn μ hQ Ω a)
    (b : ℝ) (φ : SobolevSpace.dirichlet μ hQ Ω) :
    energyForm μ hQ G.mixed φ.val =
      2 * (G.hessian φ - b * energyForm μ hQ a φ.val) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.energyForm

theorem OAI.RegularPointCoordinates.LocalHessianPairing.energy_defect_le line 92

Source documentation

The shifted Hessian bound becomes a divergence defect bound with the exact factor four from weak cancellation.

theorem energy_defect_le {Ω : Set X} (hΩ : MeasurableSet Ω)
    {f a : SobolevSpace μ hQ} (G : LocalHessianPairing μ hQ Ω f a)
    {c : ℝ} (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (ha : IsSobolevHarmonicOn μ hQ Ω a) (b D : ℝ)
    (hbound : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (G.hessian φ - b * energyForm μ hQ a φ.val) ^ 2 ≤
        D * energyForm μ hQ φ.val φ.val)
    (φ : SobolevSpace.dirichlet μ hQ Ω) :
    (energyForm μ hQ G.mixed φ.val) ^ 2 ≤ (4 * D) * energyForm μ hQ φ.val φ.val := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.energyForm

theorem OAI.RegularPointCoordinates.LocalHessianPairing.exists_harmonic_correction line 106

Source documentation

Lax--Milgram now constructs the harmonic approximation to the radial derivative, with energy and L² error linear in the shifted Bochner mass.

theorem exists_harmonic_correction {Ω : Set X} (hΩ : MeasurableSet Ω)
    {f a : SobolevSpace μ hQ} (G : LocalHessianPairing μ hQ Ω f a)
    {c P D : ℝ} (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (ha : IsSobolevHarmonicOn μ hQ Ω a) (b : ℝ) (hP : 0 ≤ P) (hD : 0 ≤ D)
    (hpoincare : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ φ.val‖ ^ 2 ≤ P * energyForm μ hQ φ.val φ.val)
    (hbound : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (G.hessian φ - b * energyForm μ hQ a φ.val) ^ 2 ≤
        D * energyForm μ hQ φ.val φ.val) :
    ∃ h : SobolevSpace μ hQ, G.mixed - h ∈ SobolevSpace.dirichlet μ hQ Ω ∧
      IsSobolevHarmonicOn μ hQ Ω h ∧
      energyForm μ hQ (G.mixed - h) (G.mixed - h) ≤ 4 * D ∧
…