BochnerMeasureProduct.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The exact local Leibniz identity for the full Bochner measure

theorem OAI.RegularPointCoordinates.bochner_measure_product_test line 21

Source documentation

The full weak product calculation, tested against an arbitrary continuous compact Sobolev function. The extra term is twice the Hessian action; all singular Bochner terms remain in the weighted measures.

theorem bochner_measure_product_test {Ω : Set X} (hΩ : MeasurableSet Ω) (K : ℝ)
    (f g h df dg dh Fg Fh Gh Fz : SobolevSpace μ hQ)
    (dg₀ dh₀ : Lp ℝ 2 μ) (hdg : IsWeakLaplacian μ hQ g dg₀)
    (hdh : IsWeakLaplacian μ hQ h dh₀)
    (hdg₀ : dg₀ =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ dg)
    (hdh₀ : dh₀ =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ dh)
    (G H : X →ᵇ ℝ) (hG : SobolevSpace.toLp μ hQ g =ᵐ[μ] G)
    (hH : SobolevSpace.toLp μ hQ h =ᵐ[μ] H)
    (A B E F : ℝ≥0)
    (hA : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ Fg x|≤A)
    (hB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ Fh x|≤B)
    (hE : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ dg x|≤E)
…

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