IndependentRootMean.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The bounded scalar root mean in the latent kernel

def OAI.JointDickman.independentRootMean line 13
theorem OAI.JointDickman.regularResidueWeight_le_base line 17
theorem OAI.JointDickman.independent_root_base_mean line 25
theorem OAI.JointDickman.independentRootMean_nonneg line 51
theorem OAI.JointDickman.independentRootMean_bounded line 58
Source documentation
Only reciprocal-prime Mertens is used to bound the root mean, uniformly in all truncation parameters.
```
theorem independentRootMean_bounded (hM : PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (L : ℕ) (τ C : ℝ),
      independentRootMean B L τ C ≤ K := by
…
```
Mentions: OAI.JointDickman.independentRootMean

theorem OAI.JointDickman.candidateMeanWeight_eq line 77

Source documentation

Averaging the sixth factor produces precisely the scalar k_B in manuscript equation (20).

theorem candidateMeanWeight_eq {M : ℕ} (B L : ℕ) (τ C : ℝ)
    (S : Fin M → Finset ℕ) (χ : BlockCandidateIndex M → ℝ)
    (e : BlockCandidateIndex M) :
    candidateMeanWeight B L τ C S χ e =
      (regularCoefficientWeight B L τ C (candidateLow e)*
        regularResidueWeight B L τ C (S e.1.1 \ e.2.1)*
        (regularCoefficientWeight B L τ C (candidateHigh e)*
          regularResidueWeight B L τ C (S e.1.2 \ e.2.2))*
        regularCoefficientWeight B L τ C (candidateQuotient e))/(B : ℝ)*χ e*
          independentRootMean B L τ C := by
…

Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.candidateMeanWeight, OAI.JointDickman.regularCoefficientWeight, OAI.JointDickman.candidateLow, OAI.JointDickman.regularResidueWeight, OAI.JointDickman.candidateHigh, OAI.JointDickman.candidateQuotient, OAI.JointDickman.independentRootMean