OAI/NumberTheory/JointDickman/Amplification/ReverseRowEnvelope.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.reverseEndpointRowEnvelope line 12
2. theorem OAI.JointDickman.reverseEndpointRowEnvelope_nonneg line 18
3. theorem OAI.JointDickman.reverseEndpointRowEnvelope_mean_bound line 29

   Source documentation

   The estimate is uniform in the fixed endpoint and in L, tau and C.

   theorem reverseEndpointRowEnvelope_mean_bound
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (L T j : ℕ) (τ C : ℝ),
         0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) → j ≠ 0 →
         ∀ S ⊆ auxiliaryPrimes B,
         finiteExpectation (independentPrimeSetMass B)
           (fun R => reverseEndpointRowEnvelope B L T j τ C S R.val) ≤
             K/(T : ℝ)*singularFactor 24 j := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.finiteExpectation, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.reverseEndpointRowEnvelope, OAI.JointDickman.singularFactor