LocalMixedSourceIdentity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Integration by parts with a local Sobolev source

theorem OAI.RegularPointCoordinates.weakLaplacian_local_mixed_identity line 20

Source documentation

Only the source representative near the test support matters. In particular, derivatives of a compact extension outside that region vanish from the mixed Bochner formula.

theorem weakLaplacian_local_mixed_identity {Ω : Set X} (hΩ : MeasurableSet Ω)
    (f b ψ : SobolevSpace μ hQ) (d e : Lp ℝ 2 μ)
    (hd : IsWeakLaplacian μ hQ f d)
    (he : e =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ b)
    (A C : ℝ≥0)
    (hb : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ b x|≤A)
    (hψb : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ ψ x|≤C)
    (q : X → ℝ) (hψ : SobolevSpace.toLp μ hQ ψ =ᵐ[μ] q)
    (hq : tsupport q ⊆ Ω) :
    (∫ x, q x*d x*e x ∂μ)+weightedGamma μ hQ e f ψ =
      -(∫ x, q x*localGamma μ hQ f b x ∂μ) := by
…

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