NoExtraFactor.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The quantitative no-extra-factor hypothesis

An approximation by R^n excludes a product with an R^(n+1) factor, at a fixed positive dimensional tolerance, giving the non-extra-factor hypothesis in the Huang--Huang transformation theorem.

def OAI.RegularPointCoordinates.NoExtraEuclideanFactor line 22
Source documentation
The ball-map form of the no-(n+1)-Euclidean condition.
```
def NoExtraEuclideanFactor {X : Type u} [MetricSpace X]
    (n : ℕ) (p : X) (r η : ℝ) : Prop :=
…
```

theorem OAI.RegularPointCoordinates.noExtraEuclideanFactor_of_approximation line 29

Source documentation

A single explicit tolerance works at every center and scale.

theorem noExtraEuclideanFactor_of_approximation {X : Type u} [MetricSpace X]
    (n : ℕ) {p : X} {r δ : ℝ} (_hr : 0 < r) (hδ : 0 ≤ δ)
    (hsmall : δ ≤ 1 / (100 * ((n + 1 : ℕ) : ℝ) ^ 2))
    (f : X → Euclidean n) (hf : IsPointedApproximation p 0 r 1 δ f) :
    NoExtraEuclideanFactor n p r (1 / (100 * ((n + 1 : ℕ) : ℝ) ^ 2)) := by
…

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