OAI/Geometry/RCD/Coordinates/RegularInitialChart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.normalized_pair_error line 14

   Source documentation

   The metric error in normalized coordinates, returned to physical units.

   theorem normalized_pair_error {X E : Type*} [MetricSpace X]
       [NormedAddCommGroup E] [NormedSpace ℝ E]
       (f : X → E) (N : E ≃L[ℝ] E) {x z : X} {r epsilon : ℝ} (hr : 0 < r)
       (hg : IsPointedApproximation x 0 r 4 epsilon
         (fun y => r⁻¹ • N (f y - f x))) (hz : dist z x ≤ 4 * r) :
       |‖N (f z - f x)‖ - dist x z| ≤ epsilon * r := by
   …

   Mentions: OAI.RegularPointCoordinates.IsPointedApproximation

2. theorem OAI.RegularPointCoordinates.regular_initial_chart line 34

   Source documentation

   The existing harmonic map is a homeomorphism onto an open image on a fixed smaller neighborhood. Exact preimages come from the quarter-scale correction construction.

   theorem regular_initial_chart {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) :
       let Ω := ball base (e.heat.radius / 1024)
   …

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