NormalFactorBands.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Separated largest-factor bands for the actual normal remainder primes.

lemma OAI.TotientAsymptotic.basic_remainder_prime_ge_three line 14
lemma OAI.TotientAsymptotic.normal_remainder_largest_band line 32

theorem OAI.TotientAsymptotic.collision_normal_factor_bands line 57

Source documentation

Uniformly over the whole collision block, the normality error is absorbed by one percent of each actual prime band.

theorem collision_normal_factor_bands : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i ≤ R x H, ∀ j ∈ Finset.Icc 1 (collisionLastIndex x i), j ≤ L x H →
    ∀ η : RemainderDatum (L x H), IsBasicRemainder x H η → ∀ y : ℝ,
    1 < normalityScale x i → 0 ≤ B (normalityScale x i) → normalityScale x i ≤ y →
    0 < B y → B y ≤ 2*fordBandScale x i →
    IsNormalPrime (normalityScale x i) (remainderPrime η j) →
    (remainderPrime η j-1 : ℕ) ≤ y →
    (89/100 : ℝ)*bandScale x j ≤ B (largestPrimeFactor (remainderPrime η j-1)) ∧
    B (largestPrimeFactor (remainderPrime η j-1)) ≤ (11/10 : ℝ)*bandScale x j := by
…

Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.collisionLastIndex, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.normalityScale, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.remainderPrime, OAI.TotientAsymptotic.bandScale, OAI.TotientAsymptotic.largestPrimeFactor

lemma OAI.TotientAsymptotic.separated_normal_factor_bands line 77