OAI/NumberTheory/JointDickman/Amplification/CandidateMultiplicity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.candidatePairRepresentations line 11
2. theorem OAI.JointDickman.latentCandidateKernel_representation_sum line 16
3. theorem OAI.JointDickman.latentCandidateKernel_square_multiplicity line 27

   Source documentation

   The multiplicity factor must be averaged with a first representation; replacing it by one would incorrectly discard collisions on an edge.

   theorem latentCandidateKernel_square_multiplicity
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {L : ℕ} (hL : 1 ≤ L) {τ : ℝ} (hτ : 0 ≤ τ) (hτsmall : τ ≤ samplingTau) :
       ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (T H M : ℕ) (S : Fin M → Finset ℕ)
         (χ : BlockCandidateIndex M → ℝ), (∀ e, 0 ≤ χ e ∧ χ e ≤ 1) →
         ∀ i k : Fin M, i < k →
         (latentCandidateKernel B L T H M τ C S χ i k)^2 ≤
           (B : ℝ)^(-(22/100 : ℝ))*
             (candidatePairRepresentations B L T H τ C i k (S i) (S k)).card*
             latentCandidateKernel B L T H M τ C S χ i k := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.samplingTau, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.latentCandidateKernel, OAI.JointDickman.candidatePairRepresentations