OAI/NumberTheory/JointDickman/Probability/FairSplitPairRegularity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.fairSelectedRemainingMass_nonneg line 12
2. theorem OAI.JointDickman.fairSelectedRemainingMass_sum line 24
3. def OAI.JointDickman.fairRemainingPairFailure line 38
4. theorem OAI.JointDickman.fairRemainingPairFailure_union line 45
5. theorem OAI.JointDickman.fair_remaining_pair_regularity_loss line 73

   Source documentation

   Uniformly in the two selected coefficients, the two remaining subsets lose at most the selected marginal mass times the regularity error.

   theorem fair_remaining_pair_regularity_loss
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {κ : ℝ} (hκ : 0 < κ) :
       ∃ K : ℝ, 0 < K ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
         ∃ ε : ℕ → ℝ, (∀ B, 0 ≤ ε B) ∧ Tendsto ε atTop (𝓝 0) ∧
           ∀ᶠ B : ℕ in atTop, ∀ (A D : Finset ℕ) (C : ℝ), 0 ≤ C →
             A ⊆ auxiliaryPrimes B → D ⊆ auxiliaryPrimes B →
             (∏ p ∈ A, p : ℕ) ≤ Real.exp (κ * B) →
             (∏ p ∈ D, p : ℕ) ≤ Real.exp (κ * B) →
             fairRemainingPairFailure B L τ C A D ≤
               (bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1 / 2 : ℝ) / p) A *
                 bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1 / 2 : ℝ) / p) D) *
                   K * (ε B + Real.exp (-(1 / 10 : ℝ) * C)) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.fairRemainingPairFailure, OAI.JointDickman.bernoulliSubsetMass