OAI/NumberTheory/JointDickman/Amplification/ConditionalAdditionProduct.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.conditionalAdditionParameter line 14
2. theorem OAI.JointDickman.conditionalAdditionParameter_bounds line 17
3. theorem OAI.JointDickman.conditionalAdditionParameter_error line 23
4. theorem OAI.JointDickman.selected_reciprocal_bound line 42
5. theorem OAI.JointDickman.conditionalAdditionParameter_total_error line 63
6. theorem OAI.JointDickman.bernoulliSubsetMass_event_perturb line 88
7. theorem OAI.JointDickman.additionPrimes_subset_auxiliary line 108
8. theorem OAI.JointDickman.conditionalAddition_error_small line 117
9. def OAI.JointDickman.conditionalAdditionLogIntervalMass line 141
10. theorem OAI.JointDickman.conditional_addition_small_ball line 150

    Source documentation

    The small-ball estimate survives conditioning on any first coefficient in the required fixed exponential range. The changed parameters and omitted coefficient primes are accounted for explicitly.

    theorem conditional_addition_small_ball
        (hFord : PublishedInputs.FordUpperSieveInput)
        (hM : PublishedInputs.PrimeReciprocalMertensInput) {H κ : ℝ} (hH : 0 ≤ H) :
        ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (A : Finset ℕ) (Y v : ℝ),
          A ⊆ auxiliaryPrimes B → (∏ p ∈ A, p : ℕ) ≤ Real.exp (κ * B) →
          Real.log (auxiliaryCutoff B) ≤ Y → Y ≤ 8 * B →
          conditionalAdditionLogIntervalMass B A Y v H ≤ K / Y := by
    …

    Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.conditionalAdditionLogIntervalMass