OAI/NumberTheory/JointDickman/Arithmetic/PrimeChannelMarginal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.primeLogCell_eq line 14
2. theorem OAI.JointDickman.primeChannelMarginal_upper line 30

   Source documentation

   The independent common/exclusive marginal is bounded by the half-prime local law plus the proved finite two-split comparison error.

   theorem primeChannelMarginal_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 / 4 ≤ lower d) → (∀ d, lower d ≤ upper d) → (∀ d, upper d ≤ 16 / 5) →
         ∀ d : D, ∀ r : (ZMod q)ˣ,
         independentCellMarginal (quarterPrimeMass (auxiliaryPrimes B))
   …

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