CompactCutoffSource.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compact support of the full cutoff source

theorem OAI.RegularPointCoordinates.signedDensity_variation_compl line 20

Source documentation

An integrable density vanishing off a measurable set has its whole signed variation supported there.

theorem signedDensity_variation_compl {f : X → ℝ} (hf : Integrable f μ)
    {K : Set X} (hK : MeasurableSet K) (hs : ∀ᵐ x ∂μ, x ∉ K → f x = 0) :
    (μ.withDensityᵥ f).variation Kᶜ = 0 := by
…

theorem OAI.RegularPointCoordinates.cutoffSourceDensity_zero_off line 30

theorem OAI.RegularPointCoordinates.cutoffMeasureSource_variation_compl line 42

Source documentation

Both the cutoff function and its full measure Laplacian have the same support bound as the cutoff and its weak Laplacian.

theorem cutoffMeasureSource_variation_compl (g c : SobolevSpace μ hQ) (q : Lp ℝ 2 μ)
    (ν : SignedMeasure X) (χ : X →ᵇ ℝ)
    (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    {K : Set X} (hK : MeasurableSet K) (hχ : ∀ x ∉ K, χ x = 0)
    (hq : ∀ᵐ x ∂μ, x ∉ K → q x = 0) :
    (cutoffMeasureSource μ hQ g c q ν χ).variation Kᶜ = 0 := by
…

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

theorem OAI.RegularPointCoordinates.cutoffProduct_zero_off line 58