OAI/NumberTheory/TotientAsymptotic/PairedComparisonGrid.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.pairedGridUpper line 13
2. def OAI.TotientAsymptotic.pairedGridLower line 16
3. theorem OAI.TotientAsymptotic.paired_grid_intervals line 21

   Source documentation

   All comparisons are made with the same finite grid label. The endpoint ζ is the smooth residual cutoff and the top endpoint is exactly one.

   theorem paired_grid_intervals {b : ℕ} {δ ζ : ℝ} (hb : 1 ≤ b) (hδ : 0 < δ)
       (u v : Fin b → ℝ) (hu : ∀ j, 0 ≤ u j) (hv : ∀ j, 0 ≤ v j)
       (halign : ∀ j, |u j-v j| ≤ (2*(j.val : ℝ)+1)*δ)
       (htop : max (u ⟨0,hb⟩) (v ⟨0,hb⟩) ≤ 1)
       (hhead : (4/5 : ℝ)≤ min (u ⟨0,hb⟩) (v ⟨0,hb⟩))
       (hfirst : pairedGridUpper δ ζ (fun j => collisionGridIndex δ (u j) (v j)) 1 < 4/5)
       (hnext : ∀ j : Fin b, ∀ hj : j.val+1<b,
         max (u ⟨j.val+1,hj⟩) (v ⟨j.val+1,hj⟩)+(2*(j.val+1 : ℕ)+4 : ℝ)*δ <
           min (u j) (v j))
       (hbottom : ζ+δ < min (u ⟨b-1,by omega⟩) (v ⟨b-1,by omega⟩)) :
       let n := fun j => collisionGridIndex δ (u j) (v j)
   …

   Mentions: OAI.TotientAsymptotic.pairedGridUpper, OAI.TotientAsymptotic.collisionGridIndex

4. lemma OAI.TotientAsymptotic.paired_grid_width line 86
5. lemma OAI.TotientAsymptotic.paired_grid_approximation line 95
6. lemma OAI.TotientAsymptotic.paired_grid_gaps line 112
7. lemma OAI.TotientAsymptotic.paired_grid_first line 148