SuffixComparison.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The comparison count for distinct suffixes after removing a varying prefix.

lemma OAI.TotientAsymptotic.tupleSuffix_zero_injective line 14
lemma OAI.TotientAsymptotic.pairSuffix_zero_injective line 27

theorem OAI.TotientAsymptotic.comparisonEncoding_injOn_of_suffix line 34

Source documentation

Comparison data need determine only the suffix, because representatives of distinct suffix pairs are selected before applying this estimate.

theorem comparisonEncoding_injOn_of_suffix {x t : ℝ} {H i k : ℕ}
    (I : Finset ℕ) (Q : Finset (TotientTuple (R x H) × TotientTuple (R x H)))
    (hL : L x H < m x) (hk : k < L x H) (hi : i ≤ R x H)
    (hQ : ∀ q ∈ Q, IsBasicTuple x H t q.1 ∧ IsBasicTuple x H t q.2)
    (hdet : Set.InjOn (fun q : TotientTuple (R x H) × TotientTuple (R x H) => pairSuffix q i) (↑Q : Set _))
    (fixed : ℕ → ℕ × ℕ)
    (hfixed : ∀ q ∈ Q, ∀ r ∈ Finset.Icc i k, r ∉ I →
      wholeWitnessPrime q.1.head (chosenRemainder x H q.1.tail) r=(fixed r).1 ∧
      wholeWitnessPrime q.2.head (chosenRemainder x H q.2.tail) r=(fixed r).2) :
    Set.InjOn (comparisonEncoding x H k I) (↑Q : Set _) := by
…

Mentions: OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.IsBasicTuple, OAI.TotientAsymptotic.pairSuffix, OAI.TotientAsymptotic.wholeWitnessPrime, OAI.TotientAsymptotic.chosenRemainder, OAI.TotientAsymptotic.comparisonEncoding

lemma OAI.TotientAsymptotic.fixed_canceled_coordinates line 68

theorem OAI.TotientAsymptotic.actual_comparison_injective line 93

Source documentation

The raw published bound is unchanged when the finite actual family is known injective in its recovered comparison data.

theorem actual_comparison_injective (hford : FordLemma51Input) :
    ∃ C y₀ : ℝ, 0 < C ∧ 1 < y₀ ∧
    ∀ {x t : ℝ} {H k K D r : ℕ} (I : Finset ℕ) (y S : ℝ) (Y U : ℕ → ℝ),
      y₀ ≤ y → FordComparisonParameters I.card y S D r Y U →
      L x H < m x → R x H < L x H →
      ∀ Q : Finset (TotientTuple (R x H) × TotientTuple (R x H)),
      (∀ q ∈ Q, IsBasicTuple x H t q.1 ∧ IsBasicTuple x H t q.2) →
      Set.InjOn (comparisonEncoding x H k I) (↑Q : Set _) →
      (∀ q ∈ Q, (suffixPreimage (chosenRemainder x H q.1.tail) k).totient=D) →
      (∀ q ∈ Q, (comparisonPairAt x H k I q).remainder.primeFactorsList.length ≤ K) →
      (∀ q ∈ Q, FordComparisonConditions I.card y S D r Y U (comparisonPairAt x H k I q)) →
      (Q.card : ℝ) ≤ (((R x H-k : ℕ) : ℝ)+1)^(D.primeFactorsList.length+K)*
…

Mentions: OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.FordComparisonParameters, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.IsBasicTuple, OAI.TotientAsymptotic.comparisonEncoding, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.chosenRemainder, OAI.TotientAsymptotic.comparisonPairAt, OAI.TotientAsymptotic.FordComparisonConditions