OAI/NumberTheory/JointDickman/Probability/CandidateRootKernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.candidateRootWeight line 15

   Source documentation

   The five endpoint/coefficient factors and the sixth, auxiliary-root factor in the manuscript's kernel, including its normalization.

   noncomputable def candidateRootWeight {M : ℕ} (B L : ℕ) (τ C : ℝ)
       (S : Fin M → Finset ℕ) (χ : BlockCandidateIndex M → ℝ)
       (e : BlockCandidateIndex M) (R : Finset ℕ) : ℝ :=
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex

2. def OAI.JointDickman.independentPrimeSetMass line 25
3. theorem OAI.JointDickman.independentPrimeSetMass_nonneg line 28
4. theorem OAI.JointDickman.independentPrimeSetMass_sum line 35
5. theorem OAI.JointDickman.candidateRootWeight_nonneg line 38
6. theorem OAI.JointDickman.candidateRootWeight_small line 52
7. def OAI.JointDickman.candidateMeanWeight line 70
8. def OAI.JointDickman.latentCandidateKernel line 76
9. def OAI.JointDickman.independentCandidateKernel line 81
10. theorem OAI.JointDickman.candidateMatrix_sub line 88
11. theorem OAI.JointDickman.candidate_root_fluctuation_bound line 98
12. theorem OAI.JointDickman.candidate_root_weight_square_cap line 121
13. theorem OAI.JointDickman.actual_candidate_root_fluctuation line 145

    Source documentation

    The estimate holds for the actual endpoint-dependent candidate list.

    theorem actual_candidate_root_fluctuation {L : ℕ} (hL : 1 ≤ L) {τ : ℝ}
        (hτ : 0 ≤ τ) (hτsmall : τ ≤ samplingTau) :
        ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (T H M : ℕ), 0 < M →
          ∀ (S : Fin M → Finset ℕ) (χ : BlockCandidateIndex M → ℝ),
          (∀ e, 0 ≤ χ e ∧ χ e ≤ 1) →
          finiteExpectation (siteProductMass (fun _ : blockCandidates B L T H M τ C S =>
            independentPrimeSetMass B)) (fun R => kernelCutNorm (fun i k =>
              independentCandidateKernel B L T H M τ C S χ R i k-
                latentCandidateKernel B L T H M τ C S χ i k)) ≤
            (B : ℝ)^(-(7/200 : ℝ))*(3*Real.log 2+
              4*(∑ e : blockCandidates B L T H M τ C S,
                candidateMeanWeight B L τ C S χ e.val)/(M : ℝ)) := by
    …

    Mentions: OAI.JointDickman.samplingTau, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.finiteExpectation, OAI.JointDickman.blockCandidates, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.kernelCutNorm, OAI.JointDickman.independentCandidateKernel, OAI.JointDickman.latentCandidateKernel, OAI.JointDickman.candidateMeanWeight