CandidateConditionalMean.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform conditional mean for the actual forward candidate entry

theorem OAI.JointDickman.latentCandidateKernel_forward_conditional_mean line 13

Source documentation

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

theorem latentCandidateKernel_forward_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 i ⊆ auxiliaryPrimes B →
      finiteExpectation (independentPrimeSetMass B)
        (fun R => latentCandidateKernel B L T H M τ C (Function.update S k 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

theorem OAI.JointDickman.latentCandidateKernel_forward_mean line 40

Source documentation

The same estimate integrated over the independent endpoint law.

theorem latentCandidateKernel_forward_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) →
      ∀ χ : BlockCandidateIndex M → ℝ, (∀ e, χ e ≤ 1) → ∀ i k : Fin M, i < k →
      finiteExpectation (siteProductMass (fun _ : Fin M => independentPrimeSetMass B))
        (fun S => latentCandidateKernel B L T H M τ C (fun i => (S i).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.finiteExpectation, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.latentCandidateKernel, OAI.JointDickman.singularFactor