PPTUnequalAlignment.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The unequal-length factor-count argument needed before matching the two lists in the PPT construction. A prefix of j+1 left shifts reaching an interval cannot be balanced by only j right shifts unless that interval has small double-logarithmic length. Consequently the required right index exists before any equal-length ShiftedPair is formed.

theorem OAI.TotientAsymptotic.ppt_unequal_normality_gap line 21

Source documentation

The right list may have arbitrary length, and its first j shifts need not reach the top of the interval. Normality's upper bound handles these truncated intervals.

theorem ppt_unequal_normality_gap {k l D E : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ) (j : Fin k)
    {S U T ε : ℝ} (hS : 1 < S) (hBS : 0 ≤ B S)
    (hD : D ≠ 0) (hE : E ≠ 0)
    (hp : ∀ i, IsNormalPrime S (p i)) (hq : ∀ i, IsNormalPrime S (q i))
    (heq : D*shiftedProduct p = E*shiftedProduct q)
    (hDU : (largestPrimeFactor D : ℝ) ≤ U)
    (hEU : (largestPrimeFactor E : ℝ) ≤ U)
    (hSU : S ≤ U) (hUT : U < T)
    (hε : Real.sqrt (B S*B T) ≤ ε)
    (hpT : ∀ i ≤ j, T ≤ (p i-1 : ℕ))
    (hqsmall : ∀ i : Fin l, j.val ≤ i.val → (largestPrimeFactor (q i-1) : ℝ) ≤ U) :
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.largestPrimeFactor

theorem OAI.TotientAsymptotic.ppt_right_index_exists line 93

Source documentation

A wide enough interval forces a right prime at rank at least j. This proves the existence of that index; it does not assume the two lists have the same length.

theorem ppt_right_index_exists {k l D E : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ) (j : Fin k)
    {S U T ε : ℝ} (hS : 1 < S) (hBS : 0 ≤ B S)
    (hD : D ≠ 0) (hE : E ≠ 0)
    (hp : ∀ i, IsNormalPrime S (p i)) (hq : ∀ i, IsNormalPrime S (q i))
    (heq : D*shiftedProduct p = E*shiftedProduct q)
    (hDU : (largestPrimeFactor D : ℝ) ≤ U)
    (hEU : (largestPrimeFactor E : ℝ) ≤ U)
    (hSU : S ≤ U) (hUT : U < T)
    (hε : Real.sqrt (B S*B T) ≤ ε)
    (hpT : ∀ i ≤ j, T ≤ (p i-1 : ℕ))
    (hgap : (2*(j.val : ℝ)+1)*ε < B T-B U) :
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.largestPrimeFactor