DenseSplit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.dense_split_of_complement_card line 8
Source documentation
The elementary dense-set step: fewer than half the possible summands can be missing, so one additive decomposition has both summands present.
```
theorem dense_split_of_complement_card
    (G : Finset ℕ) (N n : ℕ) (hnN : n ≤ N)
    (hcard : 2 * (Finset.Icc 1 N \ G).card < n - 1) :
    ∃ u ∈ G, ∃ w ∈ G, u + w = n := by
…
```

theorem OAI.Problem337.dense_split_of_real_card line 42

Source documentation

The numerical form used in the manuscript: an exceptional set of size at most X / 8 cannot obstruct all splits of an integer in [X/2, X].

theorem dense_split_of_real_card
    (G : Finset ℕ) (X : ℝ) (n : ℕ)
    (hX : 4 < X) (hnlo : X / 2 ≤ (n : ℝ)) (hnhi : (n : ℝ) ≤ X)
    (hcard : ((Finset.Icc 1 ⌊X⌋₊ \ G).card : ℝ) ≤ X / 8) :
    ∃ u ∈ G, ∃ w ∈ G, u + w = n := by
…