TupleCounting.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite set of distinct arithmetic tuples used in the collision count.

lemma OAI.TotientAsymptotic.basic_tuple_head_bound line 14
def OAI.TotientAsymptotic.tupleFinset line 29
lemma OAI.TotientAsymptotic.mem_tupleFinset line 34
lemma OAI.TotientAsymptotic.tuple_fiber_card line 48
Source documentation
The tuple fiber over a fixed tail is exactly the allowed largest-prime interval. The prime number theorem is applied to this finite set later.
```
lemma tuple_fiber_card (x : ℝ) (H : ℕ) (t : ℝ) (ζ : PrefixDatum (R x H)) :
    ((tupleFinset x H t).filter (fun τ : TotientTuple (R x H) => τ.tail = ζ)).card =
      if IsPrefixDatum x H ζ then
        ((Finset.range (⌊t⌋₊+2)).filter (fun p : ℕ => p.Prime ∧ x^(9/10 : ℝ) ≤ p ∧
          (tupleValue (TotientTuple.mk p ζ) : ℝ) ≤ t)).card
      else 0 := by
…
```
Mentions: OAI.TotientAsymptotic.PrefixDatum, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.tupleFinset, OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.IsPrefixDatum, OAI.TotientAsymptotic.tupleValue