LocalizedCutoffNorms.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Localization of cutoff L² and gradient terms

theorem OAI.RegularPointCoordinates.cutoffCLM_norm_sq_le_setIntegral line 19

Source documentation

A cutoff supported in a measurable set localizes its multiplier norm.

theorem cutoffCLM_norm_sq_le_setIntegral (u : SobolevSpace μ hQ)
    {v : X → ℝ} {L B : ℝ≥0} (hv : LipschitzWith L v)
    (hs : HasCompactSupport v) (hb : ∀ x, |v x| ≤ B) (hn : ∀ x, 0 ≤ v x)
    {Ω : Set X} (hΩ : MeasurableSet Ω) (hsΩ : tsupport v ⊆ Ω) :
    ‖SobolevSpace.toLp μ hQ (SobolevSpace.cutoffCLM μ hQ hv hs hb hn u)‖^2 ≤
      (B:ℝ)^2*∫ x in Ω, (SobolevSpace.toLp μ hQ u x)^2 ∂μ := by
…

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

theorem OAI.RegularPointCoordinates.cutoff_gradient_weight_le_setIntegral line 49

Source documentation

Locality makes the gradient-weighted L² error vanish outside the support of the cutoff.

theorem cutoff_gradient_weight_le_setIntegral (u η : SobolevSpace μ hQ)
    {v : X → ℝ} (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] v)
    {A : ℝ≥0} (hgrad : ∀ᵐ x ∂μ, |SobolevSpace.minimalSlope μ hQ η x| ≤ A)
    {Ω : Set X} (hΩ : MeasurableSet Ω) (hsΩ : tsupport v ⊆ Ω) :
    (∫ x, (SobolevSpace.toLp μ hQ u x)^2*(SobolevSpace.minimalSlope μ hQ η x)^2 ∂μ) ≤
      (A:ℝ)^2*∫ x in Ω, (SobolevSpace.toLp μ hQ u x)^2 ∂μ := by
…

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