WeakLaplacianProduct.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

L² Laplacians of products of bounded Sobolev functions

theorem OAI.RegularPointCoordinates.IsWeakLaplacian.product line 18

Source documentation

The product rule retains the mixed gradient term. A bounded gradient of one factor suffices to make the resulting weak Laplacian belong to L².

theorem IsWeakLaplacian.product
    (f g : SobolevSpace μ hQ) (df dg : Lp ℝ 2 μ)
    (hdf : IsWeakLaplacian μ hQ f df) (hdg : IsWeakLaplacian μ hQ g dg)
    (A B L : ℝ≥0)
    (hA : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ A)
    (hB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x| ≤ B)
    (hL : ∀ᵐ x ∂μ, localGamma μ hQ g g x ≤ (L:ℝ)^2) :
    ∃ q : Lp ℝ 2 μ,
      IsWeakLaplacian μ hQ (SobolevSpace.product μ hQ f g A B) q ∧
      q =ᵐ[μ] fun x => SobolevSpace.toLp μ hQ g x*df x+
        SobolevSpace.toLp μ hQ f x*dg x+2*localGamma μ hQ f g x := by
…

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