WeakLaplacianSquare.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

This is the product identity needed to differentiate heat variance. The asserted right-hand side is an actual L² function.

theorem OAI.RegularPointCoordinates.weakLaplacian_square line 21
Source documentation
The exact weak square rule, proved using bounded tests and density.
```
theorem weakLaplacian_square (f : SobolevSpace μ hQ) (d q : Lp ℝ 2 μ)
    (C : ℝ≥0) (hf : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ C)
    (hd : IsWeakLaplacian μ hQ f d)
    (hq : q =ᵐ[μ] fun x => 2*(SobolevSpace.toLp μ hQ f x*d x+localGamma μ hQ f f x)) :
    IsWeakLaplacian μ hQ (SobolevSpace.square μ hQ f C) q := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.square