OAI/NumberTheory/JointDickman/Counting/HistogramOverlapEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.local_mass_sum line 12
2. theorem OAI.JointDickman.manuscript_histogram_overlap_energy line 32

   Source documentation

   The number of dyadic boxes does not multiply the global channel energy. Only the fixed overlap constant remains.

   theorem manuscript_histogram_overlap_energy
       (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
       (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (hMP : PublishedInputs.PrimeProductMertensInput) :
       ∃ C : ℝ, 0 < C ∧ ∀ m : ℕ, 0 < m → ∀ᶠ B : ℕ in atTop,
         ∀ q : ℕ, [NeZero q] → q ≤ B →
         ∀ (t L U : ℝ), 0 < t → L ≤ U → ∀ S : Finset ℤ,
         ∀ g : (auxiliaryPrimes B → Bool) → ℝ,
         (∑ k ∈ S, ∑ i ∈ histogramWindowCells (channelFineCount m B)
             (((k : ℝ)*t+L)/B) (((k : ℝ)*t+U)/B),
           ∑ r : (ZMod q)ˣ,
   …

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