OAI/Geometry/RCD/Coordinates/RegularPairBochner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_pair_bochner line 24

   Source documentation

   The actual pair has a single full Bochner measure. Its difference mass is bounded by the source defects, and its coordinate block controls the original heat measure on the smaller ball. All objects come from the cited local calculus and cutoff inputs.

   theorem regular_pair_bochner {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       (hhessian : LocalPoissonHessianInput hX) (hcutoff : LocalGoodCutoffInput hX)
       (hn : 2 ≤ n) :
       ∃ C₀ : ℝ, 1 ≤ C₀ ∧
       ∀ {base first center : X} {a B J C A Cχ enlargement zeta eta Cg D Ca : ℝ}
         {ker : ℝ → X → X → ℝ}
         {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker},
       0 ≤ A → 0 ≤ Cχ →
       ∀ (e : RegularProjectionEnvironment hX base hk a |K| B J C A Cχ enlargement zeta eta),
       center ∈ ball base (e.heat.radius / 32) →
       ∀ (d1 : RegularCenterRadialData hX e.heat |K| B J C A Cχ eta Cg D Ca first)
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalGoodCutoffInput, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.RegularCenterRadialData