OAI/Geometry/RCD/Coordinates/RegularPatchIteration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.iterationRadius_distanceSourceRadius line 15
2. theorem OAI.RegularPointCoordinates.exists_regular_patch_iteration line 26

   Source documentation

   All analytic patch fields are made from the original harmonic map, its heat frames, its full Bochner measure and its fixed energy centers. Only the displayed scalar smallness conditions remain to be selected.

   theorem exists_regular_patch_iteration {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       {base : X} {a κ B J C A Cχ enlargement zeta eta Cpin budget : ℝ}
       {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)
       (hzeta : 0 ≤ zeta) (hzeta1 : zeta ≤ 1 / 64) (hCχ : 0 ≤ Cχ)
       (henlargement : 1 ≤ enlargement)
       (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 8 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 2)
       (hnear : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 2 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 4)
       (hwide : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 64 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 4)
       (psi : EuclideanGevreyCutoff n) (f : RegularPinchingField e.heat Cpin budget)
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.EuclideanGevreyCutoff, OAI.RegularPointCoordinates.RegularPinchingField