BochnerDriftProduct.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The drift cancellation in the Bochner product rule

def OAI.RegularPointCoordinates.bochnerDrift line 19
Source documentation
The absolutely continuous part of the Gram Laplacian after removing its full Bochner measure.
```
def bochnerDrift (K : ℝ) (f g df dg : SobolevSpace μ hQ) : X → ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.bochnerDrift_integrable line 23

theorem OAI.RegularPointCoordinates.bochnerDrift_product line 30

Source documentation

The source terms of the product Gram equation differ from the Bochner drift by precisely four times the Hessian action.

theorem bochnerDrift_product {Ω : Set X} (K : ℝ)
    (f g h df dg dh Fg Fh Gh : SobolevSpace μ hQ)
    (C D E F : ℝ≥0)
    (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x|≤C)
    (hh : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ h x|≤D)
    (hdg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ dg x|≤E)
    (hdh : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ dh x|≤F)
    (hFg : SobolevSpace.toLp μ hQ Fg =ᵐ[μ.restrict Ω] localGamma μ hQ f g)
    (hFh : SobolevSpace.toLp μ hQ Fh =ᵐ[μ.restrict Ω] localGamma μ hQ f h) :
    let gh := SobolevSpace.product μ hQ g h C D
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.product