HessianActionCoreIntegral.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From regular-core Hessian actions to all Dirichlet tests

theorem OAI.RegularPointCoordinates.LocalHessianPairing.integral_action_core_on line 19
Source documentation
The action integral on the local domain is the actual continuous Hessian functional, because all three test factors vanish off the domain.
```
theorem LocalHessianPairing.integral_action_core_on {Ω : Set X} (hΩ : MeasurableSet Ω)
    {f a : SobolevSpace μ hQ} (G : LocalHessianPairing μ hQ Ω f a) (φ : G.core) :
    (∫ x in Ω, localHessianAction μ hQ f a φ.val.val G.mixed
      (G.gammaF φ).val (G.gammaA φ).val x ∂μ) = G.hessian φ.val := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.localHessianAction

theorem OAI.RegularPointCoordinates.LocalHessianPairing.bound_of_core line 43

Source documentation

An estimate on the genuine dense regular core extends to every Dirichlet test by continuity of the Hessian and Dirichlet forms.

theorem LocalHessianPairing.bound_of_core {Ω : Set X}
    {f a : SobolevSpace μ hQ} (G : LocalHessianPairing μ hQ Ω f a) (b D : ℝ)
    (hbound : ∀ φ : G.core,
      (G.hessian φ.val-b*energyForm μ hQ a φ.val.val)^2≤D*energyForm μ hQ φ.val.val φ.val.val) :
    ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (G.hessian φ-b*energyForm μ hQ a φ.val)^2≤D*energyForm μ hQ φ.val φ.val := by
…

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

theorem OAI.RegularPointCoordinates.LocalHessianPairing.bound_of_core_action line 68

Source documentation

The shifted pointwise action bound gives the sharp integrated bound with one direction cap and the full shifted Bochner mass.

theorem LocalHessianPairing.bound_of_core_action {Ω : Set X} (hΩ : MeasurableSet Ω)
    [IsFiniteMeasure (μ.restrict Ω)] {f a : SobolevSpace μ hQ}
    (G : LocalHessianPairing μ hQ Ω f a) (σ : Measure X) [IsFiniteMeasure σ]
    (b c C : ℝ) (hC : 0≤C)
    (hden : ∀ᵐ x ∂μ.restrict Ω, c≤(σ.rnDeriv μ x).toReal)
    (hbound : ∀ φ : G.core, ∀ᵐ x ∂μ.restrict Ω,
      (localHessianAction μ hQ f a φ.val.val G.mixed (G.gammaF φ).val (G.gammaA φ).val x-
        b*localGamma μ hQ a φ.val.val x)^2 ≤
      (C*((σ.rnDeriv μ x).toReal-c))*localGamma μ hQ φ.val.val φ.val.val x) :
    ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (G.hessian φ-b*energyForm μ hQ a φ.val)^2 ≤
        (C*(σ.real Ω-c*μ.real Ω))*energyForm μ hQ φ.val φ.val := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.localHessianAction, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.energyForm