LocalCaccioppoli.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local harmonic cutoff tests in the canonical Dirichlet space

theorem OAI.RegularPointCoordinates.square_cutoff_product_mem_dirichlet line 20

Source documentation

A compactly supported Lipschitz cutoff supplies an admissible squared cutoff test against any bounded Sobolev function.

theorem square_cutoff_product_mem_dirichlet
    (Ω : Set X) (u η : SobolevSpace μ hQ) (C D L : ℝ≥0)
    (hu : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ u x| ≤ C)
    (v : X → ℝ) (hv : LipschitzWith L v) (hs : HasCompactSupport v)
    (hb : ∀ x, |v x| ≤ D) (hΩ : tsupport v ⊆ Ω)
    (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] v) :
    SobolevSpace.product μ hQ (SobolevSpace.square μ hQ η D) u (D * D) C ∈
      SobolevSpace.dirichlet μ hQ Ω := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.product, OAI.RegularPointCoordinates.SobolevSpace.square, OAI.RegularPointCoordinates.SobolevSpace.dirichlet

theorem OAI.RegularPointCoordinates.IsSobolevHarmonicOn.caccioppoli line 65

Source documentation

Local harmonicity, rather than a global weak Laplacian, suffices for the weighted Caccioppoli inequality when the cutoff is supported inside the harmonicity domain.

theorem IsSobolevHarmonicOn.caccioppoli
    (Ω : Set X) (u η : SobolevSpace μ hQ) (C D L : ℝ≥0)
    (hharm : IsSobolevHarmonicOn μ hQ Ω u)
    (hu : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ u x| ≤ C)
    (v : X → ℝ) (hv : LipschitzWith L v) (hs : HasCompactSupport v)
    (hb : ∀ x, |v x| ≤ D) (hΩ : tsupport v ⊆ Ω)
    (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] v) :
    (∫ x, (SobolevSpace.toLp μ hQ η x) ^ 2 *
      (SobolevSpace.minimalSlope μ hQ u x) ^ 2 ∂μ) ≤
      4 * ∫ x, (SobolevSpace.toLp μ hQ u x) ^ 2 *
        (SobolevSpace.minimalSlope μ hQ η x) ^ 2 ∂μ := by
…

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