OAI/NumberTheory/JointDickman/Amplification/EndpointConditionalMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.supportedEndpointTest line 12
2. theorem OAI.JointDickman.supportedEndpointTest_nonneg line 16
3. theorem OAI.JointDickman.supportedEndpointTest_ge line 23
4. theorem OAI.JointDickman.supportedEndpointTest_mean_bound line 38

   Source documentation

   Uniformly in all truncations and every fixed rough first coefficient, the averaged second endpoint contributes O(Sigma(j)/T).

   theorem supportedEndpointTest_mean_bound
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (L T b j : ℕ) (τ C : ℝ),
         0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) → j ≠ 0 →
         Disjoint b.primeFactors (Nat.primesLE (auxiliaryCutoff B)) →
         (∑ S ∈ (auxiliaryPrimes B).powerset,
           bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) S*
           ∑ A ∈ endpointSplits B L τ C S,
             regularCoefficientWeight B L τ C (∏ p ∈ A, p)*
               regularResidueWeight B L τ C (S \ A)*
                 supportedEndpointTest B T b j (∏ p ∈ A, p)) ≤
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.endpointSplits, OAI.JointDickman.regularCoefficientWeight, OAI.JointDickman.regularResidueWeight, OAI.JointDickman.supportedEndpointTest