BochnerMeasureProductLocal.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The full local measure identity for the Bochner product rule

theorem OAI.RegularPointCoordinates.bochner_measure_product line 18

Source documentation

Multiplying a gradient direction by a regular function produces the Hessian term in the full local Bochner measure, including singular mass.

theorem bochner_measure_product [SecondCountableTopology X] [IsFiniteMeasureOnCompacts μ]
    {Ω S : 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)
…

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