OAI/NumberTheory/JointDickman/Amplification/LatentRowSquareMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.independentPrimePair_expectation line 12
2. theorem OAI.JointDickman.latentPrimeSiteKernel_row_square_eq line 34
3. theorem OAI.JointDickman.latentPrimeSiteKernel_row_square_mass line 49

   Source documentation

   The actual latent kernel satisfies the integrated square-mass premise used by the finite sampling theorem, with the manuscript exponent.

   theorem latentPrimeSiteKernel_row_square_mass
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {L : ℕ} (hL : 10000 ≤ L) {η cap : ℝ} (hη : 0 < η) (hcap : 0 < cap) :
       ∃ τ K : ℝ, 0 < τ ∧ τ ≤ cap ∧ τ ≤ samplingTau ∧ 0 < K ∧
         ∀ᶠ 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 →
           ∀ (χ : BlockCandidateIndex M → ℝ), (∀ e, 0 ≤ χ e ∧ χ e ≤ 1) →
           ∀ i : Fin M,
             siteRowSquareMass (fun _ : Fin M => independentPrimeSetMass B)
   …

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