Main.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding.

theorem OAI.DoublingHilbert.no_normalized_embedding line 20
Source documentation
A normalized finite-dimensional bi-Lipschitz embedding of the fixed set cannot exist.
```
theorem no_normalized_embedding {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (hlower : ∀ p q, dist p q ≤ dist (f p) (f q)) : False := by
…
```
Mentions: OAI.DoublingHilbert.constructedSet

theorem OAI.DoublingHilbert.no_scaled_embedding line 29

Source documentation

Arbitrary positive embedding scales reduce to the normalized obstruction.

theorem no_scaled_embedding (f : constructedSet → E) {a D : ℝ}
    (ha : 0 < a) (hD : 1 ≤ D)
    (hf : ∀ x y, a * dist x y ≤ dist (f x) (f y) ∧
      dist (f x) (f y) ≤ D * a * dist x y) : False := by
…

Mentions: OAI.DoublingHilbert.constructedSet

theorem OAI.DoublingHilbert.main line 57
Source documentation
A single fixed subset, independent of dimension and distortion.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Set, Subtype, PreLp, Nat, Real, Membership.mem, AddSubgroup, OAI.DoublingHilbert.RealL2, And, OAI.DoublingHilbert.DoublingAtMost, OfNat.ofNat, LT.lt, Not, OAI.DoublingHilbert.AdmitsBiLipschitzEmbedding
Proof uses: Exists.intro, OAI.DoublingHilbert.constructedSet, And.intro, OAI.DoublingHilbert.constructedSet_cover, EuclideanSpace, Fin, LE.le, HMul.hMul, Dist.dist, ENNReal, False, OAI.DoublingHilbert.no_scaled_embedding
68 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/DoublingHilbert.lean:23 (same statement text; different proof or body). Qualify references as OAI.DoublingHilbert.main@path.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem main : ∃ S : Set RealL2,
    DoublingAtMost S 76800 ∧
      ∀ k : ℕ, 0 < k → ¬ AdmitsBiLipschitzEmbedding S k := by
…
```
Mentions: OAI.DoublingHilbert.RealL2, OAI.DoublingHilbert.DoublingAtMost, OAI.DoublingHilbert.AdmitsBiLipschitzEmbedding