PartitionedBandMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual prime-band parts satisfy the independent mass estimate used in Ford 4.1.

theorem OAI.TotientAsymptotic.partitioned_squarefree_mass line 12

theorem OAI.TotientAsymptotic.partitioned_band_value_count line 42

Source documentation

A concrete count of the values themselves. The hypotheses concern only their interval parts, squarefreeness, and factor-count lower bounds.

theorem partitioned_band_value_count : ∃ C D : ℝ,0 < C ∧ 0 < D ∧
    ∀ (S X z k : ℕ) (Y : ℕ → ℝ) (c R : Fin k → ℝ),
    2 ≤ S → S ≤ z → Y 0=z → Y k=S →
    (∀ j < k,Y (j+1) ≤ Y j) → (∀ j < k,2 ≤ Y (j+1)) →
    (∀ j,1 ≤ c j) → ∀ Q : Finset ℕ,
    (∀ n ∈ Q,0 < n ∧ n ≤ X ∧ z*partBetween n S z ≤ X ∧
      Squarefree (partBetween n S z) ∧
      ∀ j : Fin k,R j ≤ (omegaIn (partBetween n S z) (Y (j.val+1)) (Y j.val):ℝ)) →
    (Q.card:ℝ) ≤ C*X*Real.log S/Real.log z * Real.exp
      (∑ j : Fin k,(c j*(B (Y j.val)-B (Y (j.val+1))+D)-R j*Real.log (c j))) := by
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.partBetween, OAI.TotientAsymptotic.omegaIn, OAI.TotientAsymptotic.B