OAI/NumberTheory/TotientAsymptotic/TupleTotients.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.wholePreimage line 16
2. lemma OAI.TotientAsymptotic.basic_head_coprime line 19
3. lemma OAI.TotientAsymptotic.wholePreimage_totient line 34
4. lemma OAI.TotientAsymptotic.basic_tuple_isTotient line 44
5. def OAI.TotientAsymptotic.totientValues line 59
6. def OAI.TotientAsymptotic.uncoveredValues line 61
7. lemma OAI.TotientAsymptotic.card_totientValues line 64
8. lemma OAI.TotientAsymptotic.basic_tuple_mem_values line 66
9. lemma OAI.TotientAsymptotic.good_collision_count_eq line 72
10. theorem OAI.TotientAsymptotic.tuple_value_comparison line 85

    Source documentation

    Both errors are for concrete finite sets: actual bad tuples and actual uncovered totient values. The coverage error will be bounded by extraction.

    theorem tuple_value_comparison : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop, ∀ t : ℝ,
        -((uncoveredValues x H t).card : ℝ) ≤ ((tupleFinset x H t).card : ℝ)-V t ∧
        ((tupleFinset x H t).card : ℝ)-V t ≤
          (badTupleFinset x H t).card+((goodCollisionPairs x H t).card : ℝ)/2 := by
    …

    Mentions: OAI.TotientAsymptotic.uncoveredValues, OAI.TotientAsymptotic.tupleFinset, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.badTupleFinset, OAI.TotientAsymptotic.goodCollisionPairs