OAI/NumberTheory/JointDickman/Amplification/CandidateExpectedDegree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.candidateSiteKernel_expected_degree line 13

   Source documentation

   Every fixed endpoint type has bounded expected degree, including types with no regular splitting. No division by a typical-event probability occurs.

   theorem candidateSiteKernel_expected_degree
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (L T H M : ℕ) (τ C : ℝ),
         0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) →
         ∀ χ : BlockCandidateIndex M → ℝ, (∀ e, χ e ≤ 1) →
         ∀ i : Fin M, ∀ a ⊆ auxiliaryPrimes B,
         (∑ k : Fin M, finiteExpectation (independentPrimeSetMass B)
           (fun R => candidateSiteKernel B L T H M τ C χ i k a R.val)) ≤ K := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.finiteExpectation, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.candidateSiteKernel

2. def OAI.JointDickman.latentPrimeSiteKernel line 51
3. theorem OAI.JointDickman.latentPrimeSiteKernel_realizes line 56
4. theorem OAI.JointDickman.latentPrimeSiteKernel_row_mean line 63