OAI/Geometry/PinnedDistances/Model.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakPinned.Plane line 10

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

2. def OAI.WeakPinned.distanceFiber line 12

   Also declared: ComparatorChallenges/PinnedDistances.lean:12 (same declaration text).

3. def OAI.WeakPinned.k line 15

   Also declared: ComparatorChallenges/PinnedDistances.lean:15 (same declaration text).

4. def OAI.WeakPinned.richPairs line 18

   Also declared: ComparatorChallenges/PinnedDistances.lean:18 (same declaration text).

5. def OAI.WeakPinned.pairFraction line 22

   Also declared: ComparatorChallenges/PinnedDistances.lean:22 (same declaration text).

6. def OAI.WeakPinned.F line 25

   Also declared: ComparatorChallenges/PinnedDistances.lean:25 (same declaration text).

7. def OAI.WeakPinned.distances line 29
8. def OAI.WeakPinned.badPins line 32
9. def OAI.WeakPinned.badPinFraction line 35
10. def OAI.WeakPinned.B line 38
11. def OAI.WeakPinned.MainStatement line 43

    Source comment

    Uniform multiplicity and pinned-distance convergence statements.

    def MainStatement : Prop :=
    …

12. def OAI.WeakPinned.PinsStatement line 46