DyadicBochnerSmallness.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual dyadic mass smallness from splitting and the cutoff

theorem OAI.RegularPointCoordinates.dyadic_bochner_mass_small line 20
Source documentation
The same full Bochner measure is small relative to the actual heat metric at every sufficiently fine scale. The coefficient depends on the fixed volume and cutoff constants, and is linear in the splitting error.
```
theorem dyadic_bochner_mass_small {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))
    {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff (m + 1) X) hX.quadratic ker)
    (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))
    {p : X} {R e V lambda 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.IsContinuousHeatKernel, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap