OAI/Geometry/RCD/Coordinates/RegularUniformDirection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_pair_direction_uniform line 18

   Source documentation

   One constant and tolerance work at every center and scale of the constructed family. Only the original scalar source envelope must be small.

   theorem regular_pair_direction_uniform {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       (haction : LocalPoissonHessianActionInput hX)
       (hgradient : LocalHarmonicL2GradientInput hX)
       (hmean : LocalHarmonicL2MeanValueInput hX) (hn : 2 ≤ n)
       {κ A B J Cχ Cg D Ca : ℝ} (hκ : 0 ≤ κ) (hK : -κ ≤ K)
       (hA : 0 ≤ A) (hB : 0 ≤ B) (hJ : 0 ≤ J) (hCχ : 0 ≤ Cχ) :
       ∃ L tau : ℝ, 0 < L ∧ 0 < tau ∧
       ∀ {base first center : X} {a C enlargement zeta eta : ℝ}
         {ker : ℝ → X → X → ℝ}
         {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
         (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.tau, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment