FiniteSummands.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-summand reduction follows from Dirichlet's theorem and the Chinese remainder theorem.

theorem OAI.Ostmann.not_eventuallyPrimeSumset_of_finite_left line 13
Source documentation
A finite nontrivial summand is incompatible with eventual equality to the primes. The only analytic input is Dirichlet's theorem for one reduced residue class, provided by Nat.forall_exists_prime_gt_and_modEq.
```
theorem not_eventuallyPrimeSumset_of_finite_left {A B : Set ℕ}
    (hA : A.Nontrivial) (hfin : A.Finite) : ¬ EventuallyPrimeSumset A B := by
…
```
Mentions: OAI.Ostmann.EventuallyPrimeSumset
theorem OAI.Ostmann.not_eventuallyPrimeSumset_of_finite_right line 19
Source documentation
The finite-summand reduction is symmetric.
```
theorem not_eventuallyPrimeSumset_of_finite_right {A B : Set ℕ}
    (hB : B.Nontrivial) (hfin : B.Finite) : ¬ EventuallyPrimeSumset A B := by
…
```
Mentions: OAI.Ostmann.EventuallyPrimeSumset
theorem OAI.Ostmann.infinite_summands line 25
Source documentation
Lemma 2.2: both summands of an eventual decomposition are infinite.
```
theorem infinite_summands {A B : Set ℕ} (hA : A.Nontrivial) (hB : B.Nontrivial)
    (h : EventuallyPrimeSumset A B) : A.Infinite ∧ B.Infinite := by
…
```
Mentions: OAI.Ostmann.EventuallyPrimeSumset