OAI/Geometry/RCD/Sobolev/BochnerMassFromEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.bochner_mass_le_of_energy line 19

   Source documentation

   A cutoff bounds the full positive mass, including its singular part, by the local energy. This version does not subtract a constant Gram field.

   theorem bochner_mass_le_of_energy
       (U : E →L[ℝ] SobolevSpace μ hQ) (M : PositiveBilinearMeasure X E)
       (χ : X →ᵇ ℝ) (hχ : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
       (S s : Set X) (hs : MeasurableSet s) (hχone : ∀ x ∈ s, χ x = 1)
       (q : X → ℝ) {D κ A : ℝ} (hD : 0 ≤ D) (hκ : 0 ≤ κ)
       (hqmeas : AEStronglyMeasurable q (μ.restrict S))
       (hq : ∀ᵐ x ∂μ.restrict S, |q x| ≤ D) (v : E)
       (henergy : (∫ x in S, localGamma μ hQ (U v) (U v) x ∂μ) ≤ A)
       (hsource : ⟪v, M.weightedOperator χ v⟫_ℝ =
         (1 / 2 : ℝ) * (∫ x in S, localGamma μ hQ (U v) (U v) x * q x ∂μ) +
           κ * ∫ x in S, χ x * localGamma μ hQ (U v) (U v) x ∂μ) :
       ⟪v, M.massOperator s v⟫_ℝ ≤ (D / 2 + κ) * A := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.localGamma

2. theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.mass_le_of_energy line 70

   Source documentation

   The exact local harmonic Bochner equation supplies the source identity in the energy estimate; no mass bound is included as an input.

   theorem LocalHarmonicEnergy.mass_le_of_energy
       {U : E →L[ℝ] SobolevSpace μ hQ} {M : PositiveBilinearMeasure X E}
       {κ : ℝ} {p : X} {r : ℝ} {L : ℝ≥0} {v : E}
       (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
       (χ : X →ᵇ ℝ) (hχ : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
       (hχs : HasCompactSupport (χ : X → ℝ))
       (hχΩ : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
       (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
       (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
       (hqs : ∀ᵐ x ∂μ, x ∉ ball p (2 * r) → q x = 0)
       (S s : Set X) (hs : MeasurableSet s) (hχone : ∀ x ∈ s, χ x = 1)
       (hχS : ∀ x ∉ S, χ x = 0) (hqS : ∀ᵐ x ∂μ, x ∉ S → q x = 0)
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian