OAI/NumberTheory/JointDickman/Probability/ResidueChannelRate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.auxiliary_inv_ratio_eventually_le line 12
2. theorem OAI.JointDickman.residueDecayEnvelope_power_bound line 33
3. theorem OAI.JointDickman.manuscriptChannel_residue_rate line 77

   Source documentation

   The squared residue norm has the stronger rate B^(-1/40), so taking square roots also gives the manuscript's weaker B^(-1/200) norm rate.

   theorem manuscriptChannel_residue_rate
       (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
       (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (hMP : PublishedInputs.PrimeProductMertensInput) :
       ∃ K : ℝ, 0 < K ∧ ∀ 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 -
               finiteResidueAverage (fun r => manuscriptChannel m₁ B q f (a.1, r))) ^ 2) ≤
   …

   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, OAI.JointDickman.finiteResidueAverage