OAI/NumberTheory/TotientAsymptotic/GoodTuples.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.normalityScale line 16
2. def OAI.TotientAsymptotic.collisionLastIndex line 19
3. def OAI.TotientAsymptotic.collisionSmoothCutoff line 21
4. def OAI.TotientAsymptotic.collisionResidual line 24
5. def OAI.TotientAsymptotic.GoodWitnessConditions line 29

   Source documentation

   The four conditions in extraction.tex, equation good-conditions. The coordinates and scales are those of the common original endpoint x.

   def GoodWitnessConditions {x : ℝ} {H : ℕ} (p : ℕ)
       (η : RemainderDatum (L x H)) : Prop :=
   …

   Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L

6. def OAI.TotientAsymptotic.IsGoodTuple line 43

   Source documentation

   Witnesses are universally quantified; no arbitrary choice can turn a bad tuple into a good one.

   def IsGoodTuple (x : ℝ) (H : ℕ) (t : ℝ) (τ : TotientTuple (R x H)) : Prop :=
   …

   Mentions: OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.R

7. def OAI.TotientAsymptotic.goodTupleFinset line 48
8. def OAI.TotientAsymptotic.badTupleFinset line 51
9. lemma OAI.TotientAsymptotic.mem_goodTupleFinset line 54
10. lemma OAI.TotientAsymptotic.bad_tuple_failing_witness line 59
11. def OAI.TotientAsymptotic.failingWitnessFinset line 77

    Source documentation

    The finite witness space used to bound discarded tuples.

    def failingWitnessFinset (x : ℝ) (H : ℕ) (t : ℝ) :
        Finset (ℕ × RemainderDatum (L x H)) :=
    …

    Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L

12. theorem OAI.TotientAsymptotic.bad_tuple_card_le_failing_witnesses line 84

    Source documentation

    Multiple basic witnesses cause no loss: counting all failing witnesses is an upper bound for the number of bad tuples.

    theorem bad_tuple_card_le_failing_witnesses {x t : ℝ} {H : ℕ} (hPH : P H ≤ H) :
        (badTupleFinset x H t).card ≤ (failingWitnessFinset x H t).card := by
    …

    Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.badTupleFinset, OAI.TotientAsymptotic.failingWitnessFinset