OAI/Geometry/PinnedDistances/Pins.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPinned.lightTargets line 11
  2. def OAI.WeakPinned.richTargets line 14
  3. lemma OAI.WeakPinned.light_card_le line 17
  4. lemma OAI.WeakPinned.row_card_split line 46
  5. lemma OAI.WeakPinned.rich_card_sum line 53
  6. lemma OAI.WeakPinned.bad_fraction_bound line 62
  7. lemma OAI.WeakPinned.badPinFraction_nonneg line 118
  8. lemma OAI.WeakPinned.badPinFraction_le_one line 122
  9. lemma OAI.WeakPinned.bad_values_nonempty line 130
  10. lemma OAI.WeakPinned.bad_values_bddAbove line 135
  11. lemma OAI.WeakPinned.badPinFraction_le_B line 141
  12. lemma OAI.WeakPinned.B_nonneg line 146
  13. lemma OAI.WeakPinned.B_bound line 153
  14. theorem OAI.WeakPinned.pins line 166

    Source documentation

    All but a uniformly vanishing fraction of pins determine at least n^(1-ε) distinct nonzero distances.

    theorem pins (ε : ℝ) (hε : 0<ε) : Tendsto (fun n : ℕ => B n ε) atTop (𝓝 0) := by
…

    Mentions: OAI.WeakPinned.B

  15. theorem OAI.WeakPinned.pinsStatement line 180
  16. lemma OAI.WeakPinned.distances_pos line 192
  17. theorem OAI.WeakPinned.exists_pin_eventually line 199

    Source documentation

    Every sufficiently large configuration has a pin with at least the prescribed power of its cardinality many distinct nonzero distances.

    theorem exists_pin_eventually (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n : ℕ in atTop, ∀ P : Finset Plane, P.card = n →
      ∃ x ∈ P, (P.card : ℝ) ^ (1-ε) ≤ ((distances P x).card : ℝ) := by
…

    Mentions: OAI.WeakPinned.Plane, OAI.WeakPinned.distances