EuclideanDimensionGap.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional obstruction to an extra Euclidean factor

A map from R^(n+1) to R^n cannot have an almost identity Gram operator. This supplies the algebraic part of the quantitative non-(n+1)-splitting condition in the published harmonic transformation theorem.

theorem OAI.RegularPointCoordinates.extra_dimension_gram_gap line 21
Source documentation
Injectivity forced by a Gram error strictly below one contradicts dimension.
```
theorem extra_dimension_gram_gap (n : ℕ)
    (F : Euclidean (n + 1) →L[ℝ] Euclidean n) :
    1 ≤ ‖F.adjoint.comp F - ContinuousLinearMap.id ℝ (Euclidean (n + 1))‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
def OAI.RegularPointCoordinates.euclideanColumnMap line 45
Source documentation
The continuous linear map with the specified Euclidean columns.
```
def euclideanColumnMap {k n : ℕ} (v : Fin k → Euclidean n) :
    Euclidean k →L[ℝ] Euclidean n := ∑ i, (EuclideanSpace.proj i).smulRight (v i)
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.euclideanColumnMap_single line 48

theorem OAI.RegularPointCoordinates.extra_dimension_inner_error line 55

Source documentation

An explicit upper bound on entrywise almost-orthonormality is impossible for n+1 vectors in R^n.

theorem extra_dimension_inner_error (n : ℕ) (v : Fin (n + 1) → Euclidean n)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hgram : ∀ i j, |⟪v i, v j⟫_ℝ - (if i = j then 1 else 0)| ≤ ε) :
    1 ≤ ((n + 1 : ℕ) : ℝ) ^ 2 * ε := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.extra_dimension_squared_distance_error line 74

Source documentation

Squared distances of the vertices of an orthogonal simplex cannot all be too accurate in one dimension less.

theorem extra_dimension_squared_distance_error (n : ℕ) (p : Euclidean n)
    (x : Fin (n + 1) → Euclidean n) {ε : ℝ} (hε : 0 ≤ ε)
    (hbase : ∀ i, |dist (x i) p ^ 2 - 1| ≤ ε)
    (hpair : ∀ i j, i ≠ j → |dist (x i) (x j) ^ 2 - 2| ≤ ε) :
    1 ≤ 2 * ((n + 1 : ℕ) : ℝ) ^ 2 * ε := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.sq_error_le_five line 101

theorem OAI.RegularPointCoordinates.extra_dimension_distance_error line 113

Source documentation

A metric formulation suited to composing Gromov--Hausdorff approximations.

theorem extra_dimension_distance_error (n : ℕ) (p : Euclidean n)
    (x : Fin (n + 1) → Euclidean n) {η : ℝ} (hη : 0 ≤ η) (hη1 : η ≤ 1)
    (hbase : ∀ i, |dist (x i) p - 1| ≤ η)
    (hpair : ∀ i j, i ≠ j → |dist (x i) (x j) - Real.sqrt 2| ≤ η) :
    1 ≤ 10 * ((n + 1 : ℕ) : ℝ) ^ 2 * η := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.extra_dimension_scaled_distance_error line 131

Source documentation

The same obstruction at an arbitrary positive length scale.

theorem extra_dimension_scaled_distance_error (n : ℕ) (p : Euclidean n)
    (x : Fin (n + 1) → Euclidean n) {a ε : ℝ} (ha : 0 < a) (hε : 0 ≤ ε)
    (hbase : ∀ i, |dist (x i) p - a| ≤ ε)
    (hpair : ∀ i j, i ≠ j → |dist (x i) (x j) - Real.sqrt 2 * a| ≤ ε) :
    a ≤ 10 * ((n + 1 : ℕ) : ℝ) ^ 2 * ε := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean