OAI/NumberTheory/TotientAsymptotic/SurvivingGridGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.collision_last_band_le_half line 12
2. theorem OAI.TotientAsymptotic.ordered_surviving_band_margins line 29

   Source documentation

   This statement concerns the actual band heights only; the finite grid rounding is added afterwards. The first height uses the large head-prime bound, and every other height uses its own Ford band.

   theorem ordered_surviving_band_margins {x Y : ℝ} {i k b : ℕ}
       (hb : 0<b) (hB : 1<B x) (hi : i < m x) (hk : k < m x)
       (j : Fin b ↪o ℕ) (hj0 : j ⟨0,hb⟩=i) (hjk : ∀ r, j r≤k)
       (_hY : 0<Y) (hYl : (87/100 : ℝ)*fordBandScale x i≤Y)
       (hlast : fordBandScale x k ≤ fordBandScale x i/2)
       (u v : Fin b → ℝ)
       (hhead : (9/10 : ℝ)*Y≤ min (u ⟨0,hb⟩) (v ⟨0,hb⟩))
       (hlo : ∀ r, 0<r.val → (22/25 : ℝ)*fordBandScale x (j r)≤ min (u r) (v r))
       (hhi : ∀ r, 0<r.val → max (u r) (v r)≤(28/25 : ℝ)*fordBandScale x (j r)) :
       (∀ r, 0<r.val → max (u r) (v r)≤(18/25 : ℝ)*Y) ∧
       (∀ r, (4/5 : ℝ)*fordBandScale x k≤ min (u r) (v r)) ∧
       (∀ r s, r<s → (1/10 : ℝ)*fordBandScale x k≤ min (u r) (v r)-max (u s) (v s)) := by
   …

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