TailStability.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Collision stability on the two summand tails

This specializes the finite collision bound to the complementary supports forced by an eventual prime decomposition. Prime-sum estimates remain explicit hypotheses; no statement about the existence of a decomposition is assumed as an analytic input.

def OAI.Ostmann.negativeResidue line 20
Source documentation
Natural-number label for the negative residue of a summand element.
```
def negativeResidue (p a : ℕ) : ℕ := (-(a : ZMod p)).val
```
theorem OAI.Ostmann.negativeResidue_eq_iff line 22
def OAI.Ostmann.tailSupport line 29
Source documentation
All residues of the first summand's infinite tail, labeled in [0,p).
```
noncomputable def tailSupport (A : Set ℕ) (N p : ℕ) : Finset ℕ := by
…
```
theorem OAI.Ostmann.tailSupport_subset line 33
theorem OAI.Ostmann.mod_mem_tailSupport line 38
theorem OAI.Ostmann.tailSupport_nonempty line 47
theorem OAI.Ostmann.negativeResidue_mem_complement line 52
theorem OAI.Ostmann.tailSupport_complement_nonempty line 66
theorem OAI.Ostmann.tailSupport_card_add_complement line 73
def OAI.Ostmann.tailCollisionDefect line 79
Source documentation
The finite defect for the two summands, with the second one reflected.
```
noncomputable def tailCollisionDefect (A : Set ℕ) (N p : ℕ) (A₀ B₀ : Finset ℕ)
    (μ ν : ℕ → ℝ) : ℝ :=
…
```

theorem OAI.Ostmann.EventuallyPrimeSumset.tail_collision_stability line 87

Source documentation

The finite quantitative content of Lemma 2.5 for a hypothetical decomposition. Only the two displayed prime-sum estimates are left as published numerical inputs; the support and pair-count arguments are proved.

theorem EventuallyPrimeSumset.tail_collision_stability {A B : Set ℕ}
    (h : EventuallyPrimeSumset A B) (hA : A.Infinite) (hB : B.Infinite) :
    ∃ N, ∀ (P A₀ B₀ : Finset ℕ) (μ ν : ℕ → ℝ) (X Q : ℕ) (m K C : ℝ),
      1 ≤ X →
      (∀ p ∈ P, p.Prime ∧ p ≤ 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 →
      (∑ p ∈ P, Real.log (p : ℝ)) ≤ K * Q →
…

Mentions: OAI.Ostmann.EventuallyPrimeSumset