Residues.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Complementary residue supports

The elementary reduction in §2 of the manuscript. Only the exclusion of composite sums is used to separate the tail supports at a prime.

def OAI.Ostmann.tailResidues line 16
Source documentation
Residues of a summand after deleting the initial interval through N + p.
```
def tailResidues (A : Set ℕ) (N p : ℕ) : Set (ZMod p) :=
…
```
def OAI.Ostmann.negTailResidues line 20
Source documentation
Residues of the negative of the other summand, with the same deletion.
```
def negTailResidues (B : Set ℕ) (N p : ℕ) : Set (ZMod p) :=
…
```

theorem OAI.Ostmann.EventuallyPrimeSumset.prime_not_dvd_large_sum line 24

Source documentation

Large sums in an eventual prime decomposition have no smaller prime divisor.

theorem EventuallyPrimeSumset.prime_not_dvd_large_sum {A B : Set ℕ}
    (h : EventuallyPrimeSumset A B) :
    ∃ N, ∀ p, p.Prime → ∀ a ∈ A, ∀ b ∈ B,
      N ≤ a + b → p < a + b → ¬ p ∣ a + b := by
…

Mentions: OAI.Ostmann.EventuallyPrimeSumset

theorem OAI.Ostmann.EventuallyPrimeSumset.disjoint_tail_residues line 36
Source documentation
The two tails have disjoint images modulo every prime (§2).
```
theorem EventuallyPrimeSumset.disjoint_tail_residues {A B : Set ℕ}
    (h : EventuallyPrimeSumset A B) :
    ∃ N, ∀ p, p.Prime → Disjoint (tailResidues A N p) (negTailResidues B N p) := by
…
```
Mentions: OAI.Ostmann.EventuallyPrimeSumset, OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues
theorem OAI.Ostmann.tailResidues_nonempty line 51
Source documentation
The residue-support reduction requires only unboundedness of a summand.
```
theorem tailResidues_nonempty {A : Set ℕ} (hA : A.Infinite) (N p : ℕ) :
    (tailResidues A N p).Nonempty := by
…
```
Mentions: OAI.Ostmann.tailResidues
theorem OAI.Ostmann.negTailResidues_nonempty line 57

theorem OAI.Ostmann.EventuallyPrimeSumset.complementary_supports line 64

Source documentation

A hypothetical decomposition yields nonempty complementary supports at every prime.

theorem EventuallyPrimeSumset.complementary_supports {A B : Set ℕ}
    (h : EventuallyPrimeSumset A B) (hA : A.Infinite) (hB : B.Infinite) :
    ∃ N, ∀ p, p.Prime → ∃ S : Set (ZMod p),
      S.Nonempty ∧ Sᶜ.Nonempty ∧ tailResidues A N p ⊆ S ∧ negTailResidues B N p ⊆ Sᶜ := by
…

Mentions: OAI.Ostmann.EventuallyPrimeSumset, OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues