OAI/Geometry/RCD/Harmonic/UpperLevelCaccioppoli.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.upper_level_cutoff_energy_eq line 18

   Source documentation

   Testing above a level sees the same energy pairing before and after positive-part truncation. This is locality on the zero set of the test.

   theorem upper_level_cutoff_energy_eq
       (u : SobolevSpace μ hQ) {k : ℝ} (hk : 0 ≤ k)
       {χ : X → ℝ} {L B : ℝ≥0} (hχ : LipschitzWith L χ)
       (hs : HasCompactSupport χ) (hb : ∀ x, |χ x| ≤ B) (hn : ∀ x, 0 ≤ χ x) :
       let v := u.upperPositivePart μ hQ hk
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace

2. theorem OAI.RegularPointCoordinates.IsSobolevHarmonicOn.upper_level_caccioppoli line 49

   Source documentation

   The actual unbounded upper-level part of a harmonic function satisfies the weighted energy estimate. Compact cutoff multiplication supplies the test.

   theorem IsSobolevHarmonicOn.upper_level_caccioppoli
       {Ω : Set X} (u η : SobolevSpace μ hQ) {k : ℝ} (hk : 0 ≤ k)
       (hharm : IsSobolevHarmonicOn μ hQ Ω u)
       {χ : X → ℝ} {L B A : ℝ≥0} (hχ : LipschitzWith L χ)
       (hs : HasCompactSupport χ) (hb : ∀ x, |χ x| ≤ B) (hn : ∀ x, 0 ≤ χ x)
       (hΩ : tsupport χ ⊆ Ω) (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] χ)
       (hgrad : ∀ᵐ x ∂μ, |SobolevSpace.minimalSlope μ hQ η x| ≤ A) :
       let v := u.upperPositivePart μ hQ hk
   …

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