CollisionKernelDomain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform numerical data for applying the recovered Ford kernel.

lemma OAI.TotientAsymptotic.good_residual_omega_floor line 14
lemma OAI.TotientAsymptotic.normalized_grid_bottom line 26
lemma OAI.TotientAsymptotic.comparison_cutoff_one_lt line 33

theorem OAI.TotientAsymptotic.collision_kernel_domain line 38

Source documentation

All scalar hypotheses of the single-class kernel follow uniformly from the Ford bands. The only tuple-dependent bound is its number of survivors.

theorem collision_kernel_domain : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i : ℕ, i ≤ R x H → L x H < m x → R x H < L x H → ∀ y : ℝ,
    1 < y → 0 < B y → (87/100 : ℝ)*fordBandScale x i ≤ B y →
    B y ≤ 2*fordBandScale x i →
    5 ≤ ((m x-i : ℕ) : ℝ) ∧ 1 ≤ Real.log y ∧
    ((R x H-collisionLastIndex x i : ℕ) : ℝ) ≤ ((m x-i : ℕ) : ℝ) ∧
    Real.log (B y) ≤ 26*((m x-i : ℕ) : ℝ) ∧
    (⌊fordBandScale x i/((m x-i : ℕ) : ℝ)^8⌋₊ : ℝ) ≤
      2*B y/((m x-i : ℕ) : ℝ)^8 ∧
    0 < fordBandScale x (collisionLastIndex x i) ∧
    (7/10 : ℝ)*fordBandScale x (collisionLastIndex x i) ≤
      2*B y/((m x-i : ℕ) : ℝ)^18 ∧
…

Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.collisionLastIndex