OAI/NumberTheory/TotientAsymptotic/NormalityAlignment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.primeFactor_le_largest line 12
2. lemma OAI.TotientAsymptotic.omegaIn_mul line 19
3. lemma OAI.TotientAsymptotic.omegaIn_prod line 26
4. lemma OAI.TotientAsymptotic.omegaIn_eq_zero_of_largest_le line 38
5. lemma OAI.TotientAsymptotic.normality_interval_bounds line 52
6. theorem OAI.TotientAsymptotic.normality_alignment line 63

   Source documentation

   Equal products force close largest-factor locations. The left side has j+1 normal shifts reaching the interval, while only j right shifts can reach it. Smooth residual factors contribute nothing.

   theorem normality_alignment {k D D' : ℕ} (p q : Fin k → ℕ) (j : Fin k)
       {S U T ε : ℝ} (hD : D ≠ 0) (hD' : D' ≠ 0)
       (hp : ∀ i, IsNormalPrime S (p i)) (hq : ∀ i, IsNormalPrime S (q i))
       (hprod : D * shiftedProduct p = D' * shiftedProduct q)
       (hDs : (largestPrimeFactor D : ℝ) ≤ U)
       (hD's : (largestPrimeFactor D' : ℝ) ≤ U)
       (hSU : S ≤ U) (hUT : U < T) (hε : Real.sqrt (B S * B T) ≤ ε)
       (hpT : ∀ i ≤ j, T ≤ (p i-1 : ℕ))
       (hqT : ∀ i < j, T ≤ (q i-1 : ℕ))
       (hqsmall : ∀ i, j ≤ i → (largestPrimeFactor (q i-1) : ℝ) ≤ U) :
       B T-B U ≤ (2*(j.val : ℝ)+1)*ε := by
   …

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