WeakLaplacianWeightedProduct.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Product tests against an L² weak Laplacian

Both product factors are bounded Sobolev functions. In particular no Sobolev derivative of the Laplacian is needed for these identities.

theorem OAI.RegularPointCoordinates.energyForm_product_test line 22

Source documentation

The energy product rule with the two bounded coefficients exposed.

theorem energyForm_product_test (f g w : SobolevSpace μ hQ) (A B : ℝ≥0)
    (hf : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x|≤A)
    (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x|≤B) :
    energyForm μ hQ (SobolevSpace.product μ hQ f g A B) w =
      weightedGamma μ hQ (SobolevSpace.toLp μ hQ f) g w+
        weightedGamma μ hQ (SobolevSpace.toLp μ hQ g) f w := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace.product, OAI.RegularPointCoordinates.weightedGamma

theorem OAI.RegularPointCoordinates.IsWeakLaplacian.weighted_product line 41

Source documentation

Integration by parts against a bounded Sobolev product. This is the cancellation used in the Bochner square rule for merely L² sources.

theorem IsWeakLaplacian.weighted_product (f g w : SobolevSpace μ hQ)
    (d : Lp ℝ 2 μ) (hd : IsWeakLaplacian μ hQ f d) (A B : ℝ≥0)
    (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x|≤A)
    (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ w x|≤B) :
    weightedGamma μ hQ (SobolevSpace.toLp μ hQ w) f g+
      weightedGamma μ hQ (SobolevSpace.toLp μ hQ g) f w =
        -(∫ x, SobolevSpace.toLp μ hQ w x*SobolevSpace.toLp μ hQ g x*d x ∂μ) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.weightedGamma