OAI/Geometry/DoublingHilbert/Model.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DoublingHilbert.RealL2 line 7

   Also declared: ComparatorChallenges/DoublingHilbert.lean:7 (same declaration text).

2. def OAI.DoublingHilbert.DoublingAtMost line 10

   Source documentation

   Intrinsic open-ball doubling with a specified integer bound and centers in the subset.

   Also declared: ComparatorChallenges/DoublingHilbert.lean:10 (same declaration text).

   def DoublingAtMost (S : Set RealL2) (bound : ℕ) : Prop :=
   …

   Mentions: OAI.DoublingHilbert.RealL2

3. def OAI.DoublingHilbert.AdmitsBiLipschitzEmbedding line 16

   Source documentation

   Finite distortion includes an arbitrary positive change of scale.

   Also declared: ComparatorChallenges/DoublingHilbert.lean:16 (same declaration text).

   def AdmitsBiLipschitzEmbedding (S : Set RealL2) (k : ℕ) : Prop :=
   …

   Mentions: OAI.DoublingHilbert.RealL2