PublishedResidueChannel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual residue-channel estimate from published analytic inputs

No marginal, conditional-cell, or high-exclusive approximation is assumed here: all three are derived from the cited input estimates.

def OAI.JointDickman.residueChannelError line 16

theorem OAI.JointDickman.primeResidueChannel_from_published line 25

Source documentation

The bound is uniform in the number of cells, their endpoints, the modulus and the real input. It uses only structural conditions on the cells.

theorem primeResidueChannel_from_published
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput) :
    ∃ M C T : ℝ, 0 ≤ M ∧ 0 < C ∧ 0 < T ∧ ∀ᶠ B : ℕ in atTop,
      ∀ (D : Type*) [Fintype D] [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) →
      ∀ δ : ℝ, 0 < δ → (∀ d, upper d - lower d = δ) →
…

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