ExtraFactorObstruction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

An extra Euclidean factor contradicts a sufficiently flat n-dimensional ball

This uses the actual pointed approximation predicate: lift n+1 orthogonal unit vectors through its density clause, then apply the finite-dimensional distance obstruction. No topological dimension theorem is assumed.

def OAI.RegularPointCoordinates.IsBallApproximation line 21
Source documentation
Distortion and density for a ball approximation, without requiring the center to be preserved. This also covers ordinary, unpointed GH maps.
```
def IsBallApproximation {X Y : Type*} [MetricSpace X] [MetricSpace Y]
    (p : X) (q : Y) (r R ε : ℝ) (f : X → Y) : Prop :=
…
```
theorem OAI.RegularPointCoordinates.approximation_distance_error line 28
theorem OAI.RegularPointCoordinates.orthogonal_units_distance line 46

theorem OAI.RegularPointCoordinates.unpointed_simplex_approximation_obstruction line 58

Source documentation

The obstruction does not require either approximation to preserve centers: lift the target center as well as the simplex vertices.

theorem unpointed_simplex_approximation_obstruction {X Y : Type*}
    [MetricSpace X] [MetricSpace Y] (n : ℕ) {p : X} {q : Y} {r R δ η a : ℝ}
    (hδ : 0 ≤ δ) (hη : 0 ≤ η) (ha : 0 < a) (hinside : a ≤ R - η)
    (f : X → Euclidean n) (g : X → Y) (v : Fin (n + 1) → Y)
    (hv : ∀ i, dist (v i) q = a)
    (hvv : ∀ i j, i ≠ j → dist (v i) (v j) = Real.sqrt 2 * a)
    (hf : IsBallApproximation p 0 r R δ f)
    (hg : IsBallApproximation p q r R η g) :
    a ≤ 10 * ((n + 1 : ℕ) : ℝ) ^ 2 * (δ + 3 * η) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsBallApproximation

theorem OAI.RegularPointCoordinates.simplex_approximation_obstruction_radius line 83

Source documentation

A finite orthogonal simplex already detects an extra direction.

theorem simplex_approximation_obstruction_radius {X Y : Type*} [MetricSpace X] [MetricSpace Y]
    (n : ℕ) {p : X} {q : Y} {r R δ η a : ℝ} (hr : 0 < r) (hR : 0 ≤ R) (hδ : 0 ≤ δ) (hη : 0 ≤ η)
    (ha : 0 < a) (hinside : a ≤ R - η)
    (f : X → Euclidean n) (g : X → Y) (v : Fin (n + 1) → Y)
    (hv : ∀ i, dist (v i) q = a)
    (hvv : ∀ i j, i ≠ j → dist (v i) (v j) = Real.sqrt 2 * a)
    (hf : IsPointedApproximation p 0 r R δ f)
    (hg : IsPointedApproximation p q r R η g) :
    a ≤ 10 * ((n + 1 : ℕ) : ℝ) ^ 2 * (δ + 3 * η) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.simplex_approximation_obstruction line 108

Source documentation

A finite orthogonal simplex already detects an extra direction.

theorem simplex_approximation_obstruction {X Y : Type*} [MetricSpace X] [MetricSpace Y]
    (n : ℕ) {p : X} {q : Y} {r δ η a : ℝ} (hr : 0 < r) (hδ : 0 ≤ δ) (hη : 0 ≤ η)
    (ha : 0 < a) (hinside : a ≤ 2 - η)
    (f : X → Euclidean n) (g : X → Y) (v : Fin (n + 1) → Y)
    (hv : ∀ i, dist (v i) q = a)
    (hvv : ∀ i j, i ≠ j → dist (v i) (v j) = Real.sqrt 2 * a)
    (hf : IsPointedApproximation p 0 r 2 δ f)
    (hg : IsPointedApproximation p q r 2 η g) :
    a ≤ 10 * ((n + 1 : ℕ) : ℝ) ^ 2 * (δ + 3 * η) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.extra_factor_approximation_obstruction line 123

Source documentation

A ball close to R^n cannot also be close to a space containing an isometric R^(n+1) through its base point. This is the finite-point obstruction needed for the non-extra-factor hypothesis of Huang--Huang Theorem4.1.

theorem extra_factor_approximation_obstruction {X Y : Type*} [MetricSpace X] [MetricSpace Y]
    (n : ℕ) {p : X} {r δ η : ℝ} (hr : 0 < r) (hδ : 0 ≤ δ) (hη : 0 ≤ η)
    (hsmall : δ + 3 * η ≤ 1)
    (f : X → Euclidean n) (g : X → Y) (e : Euclidean (n + 1) → Y) (he : Isometry e)
    (hf : IsPointedApproximation p 0 r 2 δ f)
    (hg : IsPointedApproximation p (e 0) r 2 η g) :
    1 ≤ 10 * ((n + 1 : ℕ) : ℝ) ^ 2 * (δ + 3 * η) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation