PrimeSumInputs.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Ostmann.MertensLowerBound line 12
Source documentation
The precise one-sided consequence of Mertens' first theorem needed by the collision argument. C is fixed independently of the cutoff.
```
def MertensLowerBound (C : ℝ) : Prop :=
…
```
theorem OAI.Ostmann.prime_log_weight_le line 16

theorem OAI.Ostmann.EventuallyPrimeSumset.tail_collision_stability_of_mertens line 24

Source documentation

Collision stability on all primes up to Q, conditional on exactly the lower prime-sum estimate above. This is a component of the main proof, not the paper's infinite-summand theorem.

theorem EventuallyPrimeSumset.tail_collision_stability_of_mertens
    {A B : Set ℕ} (h : EventuallyPrimeSumset A B) (hA : A.Infinite) (hB : B.Infinite)
    {C : ℝ} (hM : MertensLowerBound C) :
    ∃ N, ∀ (A₀ B₀ : Finset ℕ) (μ ν : ℕ → ℝ) (X Q : ℕ) (m : ℝ),
      1 ≤ X → 1 ≤ Q →
      (∀ a ∈ A₀, a ∈ A ∧ N + Q < a ∧ a ≤ X) →
      (∀ b ∈ B₀, b ∈ B ∧ N + Q < b ∧ b ≤ X) →
      (∀ a ∈ A₀, 0 ≤ μ a) → (∀ b ∈ B₀, 0 ≤ ν b) →
      (∑ a ∈ A₀, μ a) = 1 → (∑ b ∈ B₀, ν b) = 1 →
      (∀ a ∈ A₀, μ a ≤ m) → (∀ b ∈ B₀, ν b ≤ m) → 0 ≤ m →
      0 ≤ (∑ p ∈ Nat.primesLE Q,
        Real.log (p : ℝ) * tailCollisionDefect A N p A₀ B₀ μ ν) ∧
…

Mentions: OAI.Ostmann.EventuallyPrimeSumset, OAI.Ostmann.MertensLowerBound, OAI.Ostmann.tailCollisionDefect