DensePairing.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.dense_pairing line 9
Source documentation
A dense subset of an initial interval represents an interior integer as a sum of two of its elements, provided fewer than half its positive splits are spoiled by missing elements.
```
theorem dense_pairing {N n : ℕ} (G : Finset ℕ) (hn : n ≤ N)
    (hcard : 2 * (Finset.Icc 1 N \ G).card < n - 1) :
    ∃ u ∈ G, ∃ v ∈ G, u + v = n := by
…
```
Mentions: OAI.Problem337.v

theorem OAI.Problem337.dense_pairing_real line 42

Source documentation

The real-parameter form used in the dense-family argument.

theorem dense_pairing_real (X : ℝ) (G : Finset ℕ) (n : ℕ)
    (hX : 4 < X) (hnlow : X / 2 ≤ (n : ℝ)) (hnup : (n : ℝ) ≤ X)
    (hbad : ((Finset.Icc 1 ⌊X⌋₊ \ G).card : ℝ) ≤ X / 8) :
    ∃ u ∈ G, ∃ v ∈ G, u + v = n := by
…

Mentions: OAI.Problem337.v

theorem OAI.Problem337.floor_multiple_bounds line 55
Source documentation
The largest integer multiple not exceeding X is at least X / 2, provided the step size is positive and does not exceed X.
```
theorem floor_multiple_bounds {X a : ℝ} (ha : 0 < a) (haX : a ≤ X) :
    X / 2 ≤ (⌊X / a⌋₊ : ℝ) * a ∧ (⌊X / a⌋₊ : ℝ) * a ≤ X := by
…
```