OAI/NumberTheory/JointDickman/Probability/CoarseKernelComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.coarseGroupAverage line 11
2. theorem OAI.JointDickman.finiteResidueAverage_square_le line 14
3. theorem OAI.JointDickman.coarseGroupAverage_energy line 27
4. theorem OAI.JointDickman.fullPrimeMass_unit_energy line 36
5. theorem OAI.JointDickman.groupedManuscriptChannel_bilinear_coarse line 50

   Source documentation

   A fixed coarse partition works for all bounded endpoint tests and every kernel with a prescribed weighted absolute row and column bound.

   theorem groupedManuscriptChannel_bilinear_coarse
       (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
       (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (hMP : PublishedInputs.PrimeProductMertensInput)
       {ε : ℝ} (hε : 0 < ε) :
       ∃ m : ℕ, 0 < m ∧ ∀ᶠ B : ℕ in atTop,
         ∀ g h : (auxiliaryPrimes B → Bool) → ℝ,
         (∀ x, |g x| ≤ 1) → (∀ x, |h x| ≤ 1) →
         ∀ K : (Fin m × Fin (channelBlockCount m B)) →
           (Fin m × Fin (channelBlockCount m B)) → ℝ,
         ∀ A : ℝ, 0 ≤ A →
   …

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