OAI/Geometry/RCD/Coordinates/RegularIterationPairs.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_iteration_pair_geometry line 21

   Source documentation

   The inverse of the working chart transports the actual heat frames. Endpoint separation and the segment estimates follow from approximation and the ellipsoid preimages, rather than being extra geometric inputs.

   theorem regular_iteration_pair_geometry {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       {base : X} {a κ B J C 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)
       (hzeta : 0 ≤ zeta) (hzetaSmall : zeta ≤ 1 / 2048)
       (hgramSmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 4 : ℝ) ^ n)⁻¹) * zeta) ≤ 3 / 4)
       (hnear : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 2 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 4)
       {Ω : Set (Euclidean n)} (u : e.heat.patchRegion ≃ₜ Ω)
       (hu : ∀ q, (u q).val = e.heat.values q.val)
       (inverse : Euclidean n → {q : X // q ∈ ball base (e.heat.radius / 32)})
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.Euclidean