OAI/NumberTheory/TotientAsymptotic/FiniteMap.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The finite-map counting lemma in collisions.tex, Lemma finite-map. The collision count records ordered distinct pairs of good tuples with the same image. Both the exceptional values and all tuples above them are bounded.

  1. def OAI.TotientAsymptotic.FiniteMap.fiber line 17
  2. def OAI.TotientAsymptotic.FiniteMap.collisionCount line 20
  3. def OAI.TotientAsymptotic.FiniteMap.multipleValues line 23
  4. def OAI.TotientAsymptotic.FiniteMap.badValues line 26
  5. def OAI.TotientAsymptotic.FiniteMap.badPreimages line 29
  6. lemma OAI.TotientAsymptotic.FiniteMap.collisionCount_eq_ordered_pairs line 32
  7. lemma OAI.TotientAsymptotic.FiniteMap.twice_le_two_add_pairs line 66
  8. lemma OAI.TotientAsymptotic.FiniteMap.two_le_pairs line 74
  9. lemma OAI.TotientAsymptotic.FiniteMap.good_preimage_bound line 78
  10. lemma OAI.TotientAsymptotic.FiniteMap.multiple_values_bound line 94
  11. lemma OAI.TotientAsymptotic.FiniteMap.bad_values_subset line 108
  12. lemma OAI.TotientAsymptotic.FiniteMap.bad_values_bound line 118
  13. theorem OAI.TotientAsymptotic.FiniteMap.counting line 130

    Source documentation

    The manuscript's finite-map lemma, with all half-collision bounds expressed over the reals and the bijection expressed as Set.BijOn.

    theorem counting [DecidableEq α] (T G D : Finset α) (W E : Finset β) (F : α → β)
    (hpartition : T = G ∪ D) (hdisjoint : Disjoint G D)
    (hmap : ∀ t ∈ T, F t ∈ W) (hE : E ⊆ W)
    (hcoverage : W \ E ⊆ T.image F) :
    (-(E.card : ℝ) ≤ (T.card : ℝ) - W.card) ∧
    ((T.card : ℝ) - W.card ≤ D.card + (collisionCount G W F : ℝ)/2) ∧
    ((badValues G D W E F).card : ℝ) ≤
      E.card + D.card + (collisionCount G W F : ℝ)/2 ∧
    ((badPreimages T G D W E F).card : ℝ) ≤
      E.card + 2*D.card + collisionCount G W F ∧
    Set.BijOn F (↑(T \ badPreimages T G D W E F))
      (↑(W \ badValues G D W E F)) := by
…

    Mentions: OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.FiniteMap.collisionCount, OAI.TotientAsymptotic.FiniteMap.badValues, OAI.TotientAsymptotic.FiniteMap.badPreimages