UniformResidueChannel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform residue attenuation on the actual refining grid

def OAI.JointDickman.manuscriptChannel line 12

theorem OAI.JointDickman.manuscriptChannel_residue_envelope line 25

Source documentation

Residue dependence tends to zero uniformly on the unit ball, including inputs varying with B and the modulus. All arithmetic hypotheses are the precise previously published inputs.

theorem manuscriptChannel_residue_envelope
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput) :
    ∃ M C T : ℝ, 0 ≤ M ∧ 0 < C ∧ 0 < T ∧
      ∀ m₁ : ℕ, 0 < m₁ → ∀ᶠ B : ℕ in atTop,
      ∀ q : ℕ, [NeZero q] → q ≤ B →
      ∀ f : (auxiliaryPrimes B → Bool) → ℝ,
      (∑ a : Fin (channelFineCount m₁ B) × (ZMod q)ˣ,
        (channelMesh (channelFineCount m₁ B) / (q.totient : ℝ)) *
          (manuscriptChannel m₁ B q f a -
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.channelFineCount, OAI.JointDickman.channelMesh, OAI.JointDickman.manuscriptChannel

theorem OAI.JointDickman.manuscriptChannel_residue_attenuation line 72