OAI/NumberTheory/JointDickman/Amplification/EndpointRowEnvelope.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.endpointSplitWeight line 12
2. theorem OAI.JointDickman.endpointSplitWeight_nonneg line 15
3. theorem OAI.JointDickman.endpointSplitWeight_sum_le line 21

   Source documentation

   All admissible fair splits together have mass at most one, including when the fixed endpoint has no admissible split.

   theorem endpointSplitWeight_sum_le {B L : ℕ} {τ C : ℝ} (hB : 1 < B)
       {S : Finset ℕ} (hS : S ⊆ auxiliaryPrimes B) :
       (∑ A ∈ endpointSplits B L τ C S, endpointSplitWeight B L τ C S A) ≤ B := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.endpointSplits, OAI.JointDickman.endpointSplitWeight

4. def OAI.JointDickman.endpointRowEnvelope line 43
5. theorem OAI.JointDickman.endpointRowEnvelope_nonneg line 49
6. theorem OAI.JointDickman.endpointRowEnvelope_mean_bound line 60

   Source documentation

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

   theorem endpointRowEnvelope_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 => endpointRowEnvelope 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.endpointRowEnvelope, OAI.JointDickman.singularFactor