GramProductMeasure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The full measure equation for a product Gram entry

theorem OAI.RegularPointCoordinates.gram_product_measure line 21

Source documentation

The Gram entry of a product is represented by genuine Sobolev products. Its local Laplacian keeps both weighted full measures and the ordinary cross terms.

theorem gram_product_measure {Ω : Set X}
    (f g h Fg Fh : SobolevSpace μ hQ)
    (G H : X →ᵇ ℝ)
    (hG : SobolevSpace.toLp μ hQ g =ᵐ[μ] G)
    (hH : SobolevSpace.toLp μ hQ h =ᵐ[μ] H)
    (dg dh : Lp ℝ 2 μ) (hdg : IsWeakLaplacian μ hQ g dg)
    (hdh : IsWeakLaplacian μ hQ h dh)
    (νg νh : SignedMeasure X)
    (hνg : IsMeasureLaplacianOn μ hQ Ω Fg νg)
    (hνh : IsMeasureLaplacianOn μ hQ Ω Fh νh)
    (hFg : SobolevSpace.toLp μ hQ Fg =ᵐ[μ.restrict Ω] localGamma μ hQ f g)
    (hFh : SobolevSpace.toLp μ hQ Fh =ᵐ[μ.restrict Ω] localGamma μ hQ f h)
…

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