CandidateForwardMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Forward candidate mass and the vanishing independent-root error

theorem OAI.JointDickman.candidateMatrix_forward_total line 14

Source documentation

Each candidate is counted once in the strict upper triangle.

theorem candidateMatrix_forward_total {ι : Type*} [Fintype ι] {M : ℕ}
    (row col : ι → Fin M) (v : ι → ℝ) (hord : ∀ e, row e < col e) :
    (∑ i : Fin M, ∑ k : Fin M, if i < k then candidateMatrix row col v i k else 0) = ∑ e, v e := by
…

Mentions: OAI.JointDickman.candidateMatrix

theorem OAI.JointDickman.latentCandidateKernel_forward_zero line 57

Source documentation

The forward entry is zero once its lag is outside the candidate support.

theorem latentCandidateKernel_forward_zero {B L T H M : ℕ} {τ C : ℝ}
    (S : Fin M → Finset ℕ) (χ : BlockCandidateIndex M → ℝ) (i k : Fin M)
    (hik : i < k) (hlag : T ≤ k.val-i.val) :
    latentCandidateKernel B L T H M τ C S χ i k = 0 := by
…

Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.latentCandidateKernel

theorem OAI.JointDickman.latentCandidateKernel_forward_total_mean line 75

Source documentation

The conditional forward bounds have an absolute total per block row.

theorem latentCandidateKernel_forward_total_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) →
      finiteExpectation (siteProductMass (fun _ : Fin M => independentPrimeSetMass B))
        (fun S => ∑ i : Fin M, ∑ k : Fin M,
          if i < k then latentCandidateKernel B L T H M τ C (fun i => (S i).val) χ i k else 0) ≤
        K*M := by
…

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