PairedFactorizationMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted counts of actual ordered left and right interval factorizations.

lemma OAI.TotientAsymptotic.paired_factorization_mass_le line 11

theorem OAI.TotientAsymptotic.paired_interval_allocation_bound line 40

Source documentation

After fixing the extracted large prime(s), the remaining two allocations have the bound used at each step of Ford's iteration.

theorem paired_interval_allocation_bound : ∃ U₀ : ℝ,2 ≤ U₀ ∧
    ∀ (k : ℕ) (U V I : ℝ),1 ≤ k → U₀ ≤ U → 4*(k:ℝ)^2 ≤ U → U ≤ V →
    (k:ℝ)*(B V-B U+1) ≤ I →
    ∀ Q : Finset ((Fin k → ℕ) × (Fin k → ℕ)),
    (∀ f ∈ Q,0 < (∏ j,f.1 j) ∧ (∏ j,f.1 j)=(∏ j,f.2 j) ∧
      (((∏ j,f.1 j).primeFactorsList.length):ℝ) ≤ I ∧
      ∀ p ∈ (∏ j,f.1 j).primeFactorsList,U < (p:ℝ) ∧ (p:ℝ) ≤ V) →
    (∑ f ∈ Q,((∏ j,f.1 j):ℝ)⁻¹) ≤ Real.exp (I*(Real.log k+1)+1) := by
…

Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B