OAI/NumberTheory/TotientAsymptotic/PPTComparisonGrid.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.pptGridLower line 18
2. theorem OAI.TotientAsymptotic.ppt_grid_intervals line 23

   Source documentation

   Every adaptive interval contains both actual coordinates. The top lower edge is chosen inside the true head-to-tail gap.

   theorem ppt_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 : θ ≤ min (u ⟨0,hb⟩) (v ⟨0,hb⟩)) (hθ : θ < 1)
       (hfirst : pairedGridUpper δ ζ (fun j => collisionGridIndex δ (u j) (v j)) 1 < θ)
       (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

3. lemma OAI.TotientAsymptotic.ppt_grid_width line 82
4. theorem OAI.TotientAsymptotic.ppt_ford_parameters_from_grid line 91

   Source documentation

   The constructed finite intervals satisfy the literal published parameter restrictions once their actual first-cutoff loss and scalar size bounds are known.

   theorem ppt_ford_parameters_from_grid {b : ℕ} {z S δ ζ θ : ℝ}
       (hb : 1 ≤ b) (hz : 1 < z) (hB : 0 < B z) (D r : ℕ)
       (n : Fin b → ℕ) (hS : Real.exp (Real.exp 1) ≤ S)
       (hSb : S ≤ comparisonCutoffs z (pairedGridUpper δ ζ n) b)
       (horder : ∀ j ∈ Finset.range b,
         pairedGridUpper δ ζ n (j+1) < pptGridLower δ θ n j ∧
           pptGridLower δ θ n j < pairedGridUpper δ ζ n j)
       (hfirst : Real.log (10*B z) ≤ B z*(1-pairedGridUpper δ ζ n 1))
       (hgap : ∀ j ∈ Finset.Icc 2 b,
         2*Real.sqrt (B S/B z) < pairedGridUpper δ ζ n (j-1)-pairedGridUpper δ ζ n j)
       (hD : 1 ≤ D) (hDz : (D : ℝ) ≤ z^(1/100 : ℝ))
       (hDs : (largestPrimeFactor D : ℝ) ≤ comparisonCutoffs z (pairedGridUpper δ ζ n) b)
   …

   Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.comparisonCutoffs, OAI.TotientAsymptotic.pairedGridUpper, OAI.TotientAsymptotic.pptGridLower, OAI.TotientAsymptotic.largestPrimeFactor