WeakBochnerSquare.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The Bochner square identity without differentiating the L² sources

All derivatives of the two source functions cancel after the weak Laplacians are tested against bounded Sobolev products.

def OAI.RegularPointCoordinates.mixedBochnerTest line 23
Source documentation
The scalar mixed Bochner test expression, before finite-span assembly.
```
def mixedBochnerTest (K : ℝ) (f g : SobolevSpace μ hQ) (d e : Lp ℝ 2 μ)
    (F : SobolevSpace μ hQ) (q : X →ᵇ ℝ) (ψ : SobolevSpace μ hQ) : ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.weighted_localHessianAction line 30
Source documentation
The three-term Hessian action under a bounded test.
```
theorem weighted_localHessianAction (q : X →ᵇ ℝ) (f v u fv fu vu : SobolevSpace μ hQ) :
    (∫ x, q x*localHessianAction μ hQ f v u fv fu vu x ∂μ) =
      (weightedGamma μ hQ q v fu+weightedGamma μ hQ q u fv-weightedGamma μ hQ q f vu)/2 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localHessianAction, OAI.RegularPointCoordinates.weightedGamma

theorem OAI.RegularPointCoordinates.mixedBochnerTest_square line 50

Source documentation

The exact square-product identity for bounded regular functions with merely L² weak Laplacians. No Sobolev representative of either source is required.

theorem mixedBochnerTest_square
    (K : ℝ) (f g F G ψ : SobolevSpace μ hQ) (d e ez : Lp ℝ 2 μ)
    (hd : IsWeakLaplacian μ hQ f d) (he : IsWeakLaplacian μ hQ g e)
    (A B C L M : ℝ≥0)
    (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x|≤A)
    (hF : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ F x|≤B)
    (hG : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ G x|≤C)
    (hfL : ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ f x≤L)
    (hgM : ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ g x≤M)
    (hFr : SobolevSpace.toLp μ hQ F =ᵐ[μ] localGamma μ hQ f g)
    (hGr : SobolevSpace.toLp μ hQ G =ᵐ[μ] localGamma μ hQ g g)
    (gb q : X →ᵇ ℝ) (hgb : SobolevSpace.toLp μ hQ g =ᵐ[μ] gb)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.localGamma