ActualComparison.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Ford's comparison bound applied to finite families of actual tuple pairs.

def OAI.TotientAsymptotic.comparisonPairAt line 15
def OAI.TotientAsymptotic.comparisonEncoding line 23
lemma OAI.TotientAsymptotic.tuple_eq_of_head_tail line 29

theorem OAI.TotientAsymptotic.comparisonEncoding_injOn line 37

Source documentation

Once the canceled primes and the common prefix are fixed, the comparison data and the two residual tuples determine the ordered pair being counted.

theorem comparisonEncoding_injOn {x t : ℝ} {H k : ℕ} (I : Finset ℕ)
    (Q : Finset (TotientTuple (R x H) × TotientTuple (R x H)))
    (hL : L x H < m x) (hkL : k < L x H)
    (hQ : ∀ q ∈ Q, IsBasicTuple x H t q.1 ∧ IsBasicTuple x H t q.2)
    (fixed : ℕ → ℕ × ℕ)
    (hfixed : ∀ q ∈ Q, ∀ r ≤ 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.wholeWitnessPrime, OAI.TotientAsymptotic.chosenRemainder, OAI.TotientAsymptotic.comparisonEncoding

theorem OAI.TotientAsymptotic.actual_comparison_with_recovery line 86

Source documentation

This is the quantitative comparison for a single fixed canceled-index, grid, and residual-integer class. All counted objects are actual tuple pairs; the missing coordinates are restored by prime-occurrence allocation.

theorem actual_comparison_with_recovery (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 → k < 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) →
      ∀ fixed : ℕ → ℕ × ℕ,
      (∀ q ∈ Q, ∀ j ≤ k, j ∉ I →
        wholeWitnessPrime q.1.head (chosenRemainder x H q.1.tail) j=(fixed j).1 ∧
        wholeWitnessPrime q.2.head (chosenRemainder x H q.2.tail) j=(fixed j).2) →
      (∀ q ∈ Q, (suffixPreimage (chosenRemainder x H q.1.tail) k).totient=D) →
…

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.wholeWitnessPrime, OAI.TotientAsymptotic.chosenRemainder, OAI.TotientAsymptotic.suffixPreimage