OAI/Geometry/RCD/Metric/DyadicMassComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.dyadic_bochner_mass_small_of_comparison line 18

   Source documentation

   The local smallness argument only uses positivity and conjugated comparison of the heat form. Its cutoff may be centered at another point.

   theorem dyadic_bochner_mass_small_of_comparison {K : ℝ} (m : ℕ)
       (hX : NoncollapsedRCD K (m + 1) X) [(hausdorff (m + 1) X).Regular]
       {a : ℝ} (ha : 0 ≤ a)
       (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
       (u : Fin (m + 1) → SobolevSpace (hausdorff (m + 1) X) hX.quadratic)
       (M : PositiveBilinearMeasure X (Euclidean (m + 1)))
       (S : ℕ → Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
       (Q : ℕ → Euclidean (m + 1) →L[ℝ] Euclidean (m + 1))
       (hQpos : ∀ i, (Q i).IsPositive)
       {p : X} {R e V C : ℝ} {L : ℝ≥0}
       (G : ∀ v, LocalHarmonicEnergy (hausdorff (m + 1) X) hX.quadratic
         (sobolevColumnMap (hausdorff (m + 1) X) hX.quadratic u) M |K| p (2 * R) L v)
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap