CandidateReverseConditional.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform conditional mean for the actual forward candidate entry

theorem OAI.JointDickman.latentCandidateKernel_reverse_conditional_mean line 13

Source documentation

The other endpoint types may be completely arbitrary. Averaging just the lower endpoint gives the manuscript's uniform bound.

theorem latentCandidateKernel_reverse_conditional_mean
    (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) →
      ∀ (S : Fin M → Finset ℕ) (χ : BlockCandidateIndex M → ℝ),
      (∀ e, χ e ≤ 1) → ∀ i k : Fin M, i < k → S k ⊆ auxiliaryPrimes B →
      finiteExpectation (independentPrimeSetMass B)
        (fun R => latentCandidateKernel B L T H M τ C (Function.update S i R.val) χ i k) ≤
          K/(T : ℝ)*singularFactor 24 (k.val-i.val) := by
…

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