AveragedRootFluctuation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The independent-root fluctuation vanishes after averaging endpoint types

theorem OAI.JointDickman.candidateMean_total_mean line 13

Source documentation

The actual endpoint-dependent candidate list has bounded expected weight per block position.

theorem candidateMean_total_mean
    (hFord : FordUpperSieveInput) (hM : 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) →
      finiteExpectation (siteProductMass (fun _ : Fin M => independentPrimeSetMass B))
        (fun S => ∑ e : blockCandidates B L T H M τ C (fun i => (S i).val),
          candidateMeanWeight B L τ C (fun i => (S i).val) χ e.val) ≤ K*M := by
…

Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.finiteExpectation, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.blockCandidates, OAI.JointDickman.candidateMeanWeight

def OAI.JointDickman.averagedIndependentRootError line 37

theorem OAI.JointDickman.averagedIndependentRootError_bound line 48

Source documentation

No dependence on the regularity constant C, or on the endpoint types, remains in the error coefficient.

theorem averagedIndependentRootError_bound
    (hFord : FordUpperSieveInput) (hM : PrimeReciprocalMertensInput)
    {L : ℕ} (hL : 1 ≤ L) {τ : ℝ} (hτ : 0 ≤ τ) (hτsmall : τ ≤ samplingTau) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (T H M : ℕ),
      0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) → 0 < M →
      ∀ χ : BlockCandidateIndex M → ℝ, (∀ e, 0 ≤ χ e ∧ χ e ≤ 1) →
      averagedIndependentRootError B L T H M τ C χ ≤
        K*(B : ℝ)^(-(7/200 : ℝ)) := by
…

Mentions: OAI.JointDickman.samplingTau, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.averagedIndependentRootError