RegularTangents.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Regularity and convergence of rescalings

The compactness input is kept separate from regularity. In particular, regularity is never used as an assertion that a tangent already exists. Once subsequential pointed compactness is available, all rescaling sequences at a regular point converge to Euclidean space.

theorem OAI.RegularPointCoordinates.IsPointedApproximation.postcomp_isometry line 25

Source documentation

Pointed metric approximations are preserved by a target isometry.

theorem IsPointedApproximation.postcomp_isometry
    {p : X} {q : Y} {r R epsilon : ℝ} {f : X → Y}
    (hf : IsPointedApproximation p q r R epsilon f) (e : Y ≃ᵢ Z) :
    IsPointedApproximation p (e q) r R epsilon (fun x => e (f x)) := by
…

Mentions: OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.RescalingsConverge.postcomp_isometry line 39
def OAI.RegularPointCoordinates.PointedRescalingPrecompactness line 49
Source documentation
Rescalings at a point admit a pointed-convergent subsequence with a proper metric-space limit.
```
def PointedRescalingPrecompactness (p : X) : Prop :=
…
```
theorem OAI.RegularPointCoordinates.regular_rescalings_converge line 58
Source documentation
The all-tangents definition of regularity and pointed compactness imply convergence along every prescribed sequence of scales.
```
theorem regular_rescalings_converge {n : ℕ} {p : X}
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular n p)
    (r : ℕ → ℝ) (hr : ∀ i, 0 < r i) (hrzero : Tendsto r atTop (𝓝 0)) :
    RescalingsConverge p (0 : Euclidean n) r := by
…
```
Mentions: OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.RescalingsConverge, OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.regular_has_euclidean_tangent line 83
Source documentation
Compactness also proves existence of a Euclidean tangent; this is not silently built into the universal definition of regularity.
```
theorem regular_has_euclidean_tangent {n : ℕ} {p : X}
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular n p) :
    IsTangent p (0 : Euclidean n) := by
…
```
Mentions: OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.IsTangent, OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.regular_small_scale_approximation line 93
Source documentation
The sequential statement gives a uniform approximation threshold for every fixed radius and tolerance, not merely a chosen blow-up sequence.
```
theorem regular_small_scale_approximation {n : ℕ} {p : X}
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular n p)
    {R epsilon : ℝ} (hR : 0 < R) (hepsilon : 0 < epsilon) :
    ∃ delta : ℝ, 0 < delta ∧ ∀ r : ℝ, 0 < r → r < delta →
      ∃ f : X → Euclidean n, IsPointedApproximation p 0 r R epsilon f := by
…
```
Mentions: OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation