OAI/Geometry/RCD/Sobolev/PositiveDefectCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.positive_defect_cutoff_identity line 20

   Source documentation

   The compact Lipschitz source identity is sufficient for the cutoff calculation; no extension to arbitrary continuous tests is assumed.

   theorem positive_defect_cutoff_identity {S : Set X} (Q : SobolevSpace μ hQ)
       (σ : Measure X) (a : ℝ)
       (hsource : ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (L : ℝ≥0),
         LipschitzWith L v → HasCompactSupport v → tsupport v ⊆ S →
         SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v →
         energyForm μ hQ Q ψ + a * (∫ x in S, v x ∂μ) = ∫ x, v x ∂σ)
       (χ : X →ᵇ ℝ) {L : ℝ≥0} (hχlip : LipschitzWith L (χ : X → ℝ))
       (hχs : HasCompactSupport (χ : X → ℝ)) (hχS : tsupport (χ : X → ℝ) ⊆ S)
       (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
       (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
       (hqs : ∀ᵐ x ∂μ, x ∉ S → q x = 0) :
       (∫ x in S, SobolevSpace.toLp μ hQ Q x * q x ∂μ) =
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.IsWeakLaplacian

2. theorem OAI.RegularPointCoordinates.shifted_poisson_mass_of_positive_defect line 55

   Source documentation

   The full shifted Bochner mass bound uses only the actual compact Lipschitz source identity proved for the squared-distance datum.

   theorem shifted_poisson_mass_of_positive_defect
       {U : E →L[ℝ] SobolevSpace μ hQ} {M : PositiveBilinearMeasure X E}
       {κ : ℝ} {p : X} {r : ℝ} {L : ℝ≥0} {v : E}
       [IsFiniteMeasure (μ.restrict (ball p (2 * r)))]
       (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
       (ell : E →ₗ[ℝ] ℝ) (n : ℝ)
       (hshift : ShiftedBochnerLowerBound M (μ.restrict (ball p (2 * r))) ell n)
       (Q : SobolevSpace μ hQ) (σ : Measure X) [IsFiniteMeasure σ]
       (hsource : ∀ (ψ : SobolevSpace μ hQ) (w : X → ℝ) (C : ℝ≥0),
         LipschitzWith C w → HasCompactSupport w → tsupport w ⊆ ball p (2 * r) →
         SobolevSpace.toLp μ hQ ψ =ᵐ[μ] w →
         energyForm μ hQ Q ψ + ell v * (∫ x in ball p (2 * r), w x ∂μ) = ∫ x, w x ∂σ)
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.ShiftedBochnerLowerBound, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm