WeakLaplacianMixedSourceL2.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Mixed integration by parts with an arbitrary L2 source

Bounded Sobolev recovery converges strongly. With one bounded-gradient factor, both remaining products are L² pairings, so the product identity passes to an unbounded Sobolev Laplacian.

theorem OAI.RegularPointCoordinates.mixed_bounded_source_test line 22
theorem OAI.RegularPointCoordinates.weakLaplacian_mixed_source_L2 line 59

theorem OAI.RegularPointCoordinates.weakLaplacian_local_mixed_source_L2 line 110

Source documentation

An L² source can be replaced by a Sobolev representative only near the test support. No amplitude bound on that representative is needed.

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

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