OAI/Geometry/RCD/Heat/BochnerHeatSmallness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.bochner_mass_small_relative_to_heat line 22

   Source documentation

   The normalized Bochner estimate on a sixteen-times larger ball gives smallness in a heat metric at the inner scale. Both comparison factors are two, so they cancel the factor four from the Bochner cutoff radius.

   theorem bochner_mass_small_relative_to_heat {n : ℕ}
       (u : Fin n → SobolevSpace μ hQ) (M : PositiveBilinearMeasure X (Euclidean n))
       {p : X} {s R e C κ V : ℝ} {L : ℝ≥0}
       (G : ∀ v, LocalHarmonicEnergy μ hQ (sobolevColumnMap μ hQ u) M κ p (2 * s) L v)
       (A : Euclidean n ≃L[ℝ] Euclidean n) {w : X → Euclidean n}
       (hfirst : FirstOrderSplittingOn μ hQ p (16 * s) e (transformedColumn μ hQ u A) w)
       (hexact : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u)
         (ball p (16 * s)) measurableSet_ball A)
       (hs : 0 < s) (hsR : s ≤ R) (he : 0 ≤ e) (he1 : e ≤ 1)
       (hC : 0 ≤ C) (hκ : 0 ≤ κ) (hcurv : κ * R ^ 2 ≤ e) (hV : 0 ≤ V)
       (hvolpos : 0 < μ.real (ball p (16 * s)))
       (hvol : μ.real (ball p (16 * s)) ≤ V * (16 * s) ^ n)
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsExactMeanNormalization