LatentMassMoments.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded row and normalized total second moments of the latent graph

theorem OAI.JointDickman.finite_average_square_bound line 12

theorem OAI.JointDickman.latentPrimeSiteKernel_moments line 35

Source documentation

Both conclusions of the manuscript's integrated-row-moments proposition hold for the actual independent-site kernel.

theorem latentPrimeSiteKernel_moments
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    {L : ℕ} (hL : 10000 ≤ L) {η cap : ℝ} (hη : 0 < η) (hcap : 0 < cap) :
    ∃ τ K D : ℝ, 0 < τ ∧ τ ≤ cap ∧ τ ≤ samplingTau ∧ 0 < K ∧ 0 < D ∧
      ∀ᶠ B : ℕ in atTop, ∀ (T H M : ℕ) (C : ℝ),
        0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) →
        T ≤ auxiliaryCutoff B → (T : ℝ) ≤ (B : ℝ)^2 →
        η*(B : ℝ)^(32/100 : ℝ) ≤ H → 0 < M →
        ∀ (χ : BlockCandidateIndex M → ℝ), (∀ e, 0 ≤ χ e ∧ χ e ≤ 1) →
        (∀ i : Fin M, siteRowSquareMass (fun _ : Fin M => independentPrimeSetMass B)
          (latentPrimeSiteKernel B L T H M τ C χ) i ≤ K*(B : ℝ)^(-(21/100 : ℝ))) ∧
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.samplingTau, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.siteRowSquareMass, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.latentPrimeSiteKernel