RegularSquareLaplacian.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual local Laplacians of squared regular functions

theorem OAI.RegularPointCoordinates.IsWeakLaplacian.square_local line 18

Source documentation

A local Sobolev representative of the source suffices. The global weak Laplacian remains the actual L² source of the compact extension.

theorem IsWeakLaplacian.square_local {Ω : Set X}
    (g G dg : SobolevSpace μ hQ) (d : Lp ℝ 2 μ)
    (hd : IsWeakLaplacian μ hQ g d) (A B L : ℝ≥0)
    (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x|≤A)
    (hdg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ dg x|≤B)
    (hL : ∀ᵐ x ∂μ, localGamma μ hQ g g x≤(L:ℝ)^2)
    (hGr : SobolevSpace.toLp μ hQ G =ᵐ[μ.restrict Ω] localGamma μ hQ g g)
    (hdr : d =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ dg) :
    ∃ q : Lp ℝ 2 μ,
      IsWeakLaplacian μ hQ (SobolevSpace.product μ hQ g g A A) q ∧
      q =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ
        (SobolevSpace.product μ hQ g dg A B+
…

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

theorem OAI.RegularPointCoordinates.squareLaplacianSource_bound line 48