OAI/NumberTheory/TotientAsymptotic/CollisionFactorHeights.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.ford_band_step line 15
2. lemma OAI.TotientAsymptotic.ford_band_antitone line 25
3. theorem OAI.TotientAsymptotic.collision_factor_ford_bands line 34

   Source documentation

   Normality changes either endpoint of an actual coarse band by less than one further percent when expressed in Ford's centers.

   theorem collision_factor_ford_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 →
       (22/25 : ℝ)*fordBandScale x j ≤ B (largestPrimeFactor (remainderPrime η j-1)) ∧
       B (largestPrimeFactor (remainderPrime η j-1)) ≤ (28/25 : ℝ)*fordBandScale 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.largestPrimeFactor

4. lemma OAI.TotientAsymptotic.normal_factor_band_gap line 58
5. lemma OAI.TotientAsymptotic.collision_rounding_margin line 70
6. lemma OAI.TotientAsymptotic.normalized_factor_margin line 94

   Source documentation

   The smallest factor-band margin dominates the full grid rounding cost.

   lemma normalized_factor_margin {x y : ℝ} {i : ℕ} {h : ℕ}
       (hh : 4≤h) (hB : 1<B x) (him : i< m x)
       (hcut : 2*collisionCutoff (m x-i)< m x-i) (hhdef : h=m x-i)
       (hBy : 0<B y) (hByu : B y≤2*fordBandScale x i) :
       1/(100*(h : ℝ)^20)<(1/10 : ℝ)*fordBandScale x (collisionLastIndex x i)/B y := by
   …

   Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.collisionCutoff, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.collisionLastIndex