OAI/NumberTheory/JointDickman/Amplification/LogMassBilinear.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.channelIndexEquiv line 11
2. def OAI.JointDickman.cellMassBilinear line 14
3. def OAI.JointDickman.coarseLogMass line 19
4. theorem OAI.JointDickman.cellMassBilinear_reindex line 24
5. theorem OAI.JointDickman.logMassBilinear_reindex line 43
6. theorem OAI.JointDickman.coarseLogMassBilinear_reindex line 54
7. theorem OAI.JointDickman.logMassBilinear_coarse_band line 70

   Source documentation

   The actual logarithmic signed measures admit a fixed coarse approximation uniformly over every kernel of height O(B) and width O(1/B).

   theorem logMassBilinear_coarse_band
       (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 (channelFineCount m B) → Fin (channelFineCount m B) → ℝ,
         ∀ C M : ℝ, 0 ≤ C → 0 ≤ M →
         (∀ i k, |K i k| ≤ M*B) →
   …

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