PoissonHessianIdentity.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cancellation of both constant-source terms in the integrated Hessian

theorem OAI.RegularPointCoordinates.LocalHessianPairing.constant_source_identity line 17
Source documentation
Constant Laplacians cancel each other in the integrated Koszul formula, so the mixed-gradient energy pairing equals twice the Hessian action.
```
theorem LocalHessianPairing.constant_source_identity {Ω : Set X} (hΩ : MeasurableSet Ω)
    {f a : SobolevSpace μ hQ} (G : LocalHessianPairing μ hQ Ω f a)
    {c d : ℝ} (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (ha : IsConstantLaplacianOn μ hQ Ω a d)
    (φ : SobolevSpace.dirichlet μ hQ Ω) :
    energyForm μ hQ G.mixed φ.val = 2*G.hessian φ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.energyForm
theorem OAI.RegularPointCoordinates.LocalHessianPairing.hessian_unique_of_constant_sources line 49
Source documentation
The action is independent of all choices of compact extensions and regular cores. This allows estimates proved for any local construction to use the same Hessian action.
```
theorem LocalHessianPairing.hessian_unique_of_constant_sources {Ω : Set X}
    (hΩ : MeasurableSet Ω) {f a : SobolevSpace μ hQ}
    (G H : LocalHessianPairing μ hQ Ω f a) {c d : ℝ}
    (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (ha : IsConstantLaplacianOn μ hQ Ω a d) : G.hessian = H.hessian := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.IsConstantLaplacianOn
theorem OAI.RegularPointCoordinates.LocalHessianPairing.shifted_source_identity line 64
Source documentation
The exact factor two in the shifted divergence identity applies to both Poisson functions, including a nonzero constant source.
```
theorem LocalHessianPairing.shifted_source_identity {Ω : Set X}
    (hΩ : MeasurableSet Ω) {f a : SobolevSpace μ hQ}
    (G : LocalHessianPairing μ hQ Ω f a) {c d : ℝ}
    (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (ha : IsConstantLaplacianOn μ hQ Ω a d)
    (b : ℝ) (φ : SobolevSpace.dirichlet μ hQ Ω) :
    energyForm μ hQ G.mixed φ.val - 2*b*energyForm μ hQ a φ.val =
      2*(G.hessian φ-b*energyForm μ hQ a φ.val) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.energyForm