PrimeCommonCell.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The conditional common-product cell bound

theorem OAI.JointDickman.primeProductLogCell_eq line 14

theorem OAI.JointDickman.primeCommonLogCell_upper line 36

Source documentation

A low exclusive product shifts each cell inside a fixed positive logarithmic range, where the common-product density is uniformly bounded.

theorem primeCommonLogCell_upper
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput) :
    ∃ M C : ℝ, 0 ≤ M ∧ 0 < C ∧ ∀ᶠ B : ℕ in atTop,
      ∀ (D : Type*) [DecidableEq D], ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (B : ℝ) ^ (100 : ℝ) →
      ∀ lower upper : D → ℝ,
      (∀ d e s, s ∈ Set.Ioc (lower d) (upper d) → s ∈ Set.Ioc (lower e) (upper e) → d = e) →
      (∀ d, 1 / 2 ≤ lower d) → (∀ d, lower d ≤ upper d) → (∀ d, upper d ≤ 16 / 5) →
      ∀ e : auxiliaryPrimes B → Bool,
      lowPrimeLog (auxiliaryPrimes B) B (1 / 4) e → ∀ d : D, ∀ r : (ZMod q)ˣ,
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.lowPrimeLog