LocalMeasureProduct.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The local product rule for full measure Laplacians

Multiplication by a regular function preserves the exact measure source, including singular mass. Tests stay in the original open region.

theorem OAI.RegularPointCoordinates.IsMeasureLaplacianOn.mul line 22

Source documentation

Multiply a local measure Laplacian by a bounded continuous Sobolev function with an L² weak Laplacian.

theorem IsMeasureLaplacianOn.mul {Ω : Set X} {g : SobolevSpace μ hQ}
    {ν : SignedMeasure X} (hν : IsMeasureLaplacianOn μ hQ Ω g ν)
    (χ : X →ᵇ ℝ)
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
    (D : ℝ≥0) (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x| ≤ D) :
    IsMeasureLaplacianOn μ hQ Ω
      (SobolevSpace.product μ hQ g c D ‖χ‖₊)
      (cutoffMeasureSource μ hQ g c q ν χ) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsMeasureLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.product, OAI.RegularPointCoordinates.cutoffMeasureSource