MeasureLaplacianProduct.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Cutting off a local measure Laplacian

The source is the full weighted signed measure plus the two ordinary product-rule terms. This is an algebraic consequence of the actual Sobolev product rule, rather than an additional analytic assumption.

def OAI.RegularPointCoordinates.IsMeasureLaplacianOn line 26
Source documentation
Local distributional measure Laplacian, using continuous compactly supported Sobolev tests inside the indicated region.
```
def IsMeasureLaplacianOn (Ω : Set X) (g : SobolevSpace μ hQ)
    (ν : SignedMeasure X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
def OAI.RegularPointCoordinates.cutoffSourceDensity line 34
Source documentation
The absolutely continuous part introduced by the cutoff product.
```
def cutoffSourceDensity (g c : SobolevSpace μ hQ) (q : Lp ℝ 2 μ) : X → ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.cutoffSourceDensity_integrable line 38
def OAI.RegularPointCoordinates.cutoffMeasureSource line 44
Source documentation
The full signed source of the cutoff function.
```
def cutoffMeasureSource (g c : SobolevSpace μ hQ) (q : Lp ℝ 2 μ)
    (ν : SignedMeasure X) (χ : X →ᵇ ℝ) : SignedMeasure X :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace

theorem OAI.RegularPointCoordinates.IsMeasureLaplacianOn.cutoff line 51

Source documentation

The local measure equation and the weak cutoff Laplacian imply the full global product equation, with no assumption of absolute continuity for the local source.

theorem IsMeasureLaplacianOn.cutoff {Ω : Set X} {g : SobolevSpace μ hQ}
    {ν : SignedMeasure X} (hν : IsMeasureLaplacianOn μ hQ Ω g ν)
    (χ : X →ᵇ ℝ) (hχs : HasCompactSupport (χ : X → ℝ)) (hχΩ : tsupport (χ : 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) :
    IsMeasureLaplacian μ 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.IsMeasureLaplacian, OAI.RegularPointCoordinates.SobolevSpace.product, OAI.RegularPointCoordinates.cutoffMeasureSource