RegularEllipsoids.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual frozen ellipsoids inside the working coordinate image

def OAI.RegularPointCoordinates.regularEllipsoidRadius line 14

theorem OAI.RegularPointCoordinates.regular_frozen_ellipsoid_preimages line 21

Source documentation

The constructive quarter-scale corrections fill a small ellipsoid in the actual fine heat metric. Every preimage lies in the patch region.

theorem regular_frozen_ellipsoid_preimages {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)
    (i : ℕ) {q : X} (hq : q ∈ e.heat.patchRegion)
    (hball : ball q (4 * regularEllipsoidRadius e.heat.radius e.heat.shift i) ⊆ e.heat.patchRegion) :
    ∀ P : Euclidean n,
      ‖e.heat.frozenAt q i (P - e.heat.values q)‖ <
…

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

theorem OAI.RegularPointCoordinates.regular_ellipsoid_room line 63
Source documentation
The inner original-space ball has room for every ellipsoid used by the iteration, uniformly over the scale.
```
theorem regular_ellipsoid_room {R : ℝ} (hR : 0 < R) (shift i : ℕ)
    {base q : X} (hq : q ∈ ball base (R / 2 ^ (shift + 12))) :
    ball q (4 * regularEllipsoidRadius R shift i) ⊆ regularPatchRegion base R shift := by
…
```
Mentions: OAI.RegularPointCoordinates.regularEllipsoidRadius, OAI.RegularPointCoordinates.regularPatchRegion