OuterRowRealBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The natural-number row bound m / 10 ≤ n implies a real lower bound with an absolute loss of one, suitable for the exponential incidence estimates.

theorem OAI.QuantitativeVanDerWaerden.real_div_ten_sub_one_lt line 17
Source documentation
Losing one converts the floored row-size bound to a strict real bound.
```
theorem real_div_ten_sub_one_lt {m n : ℕ} (h : m / 10 ≤ n) :
    (m : ℝ) / 10 - 1 < (n : ℝ) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.real_div_ten_sub_one_le line 24
Source documentation
The real row-size lower bound used in weighted incidence sums.
```
theorem real_div_ten_sub_one_le {m n : ℕ} (h : m / 10 ≤ n) :
    (m : ℝ) / 10 - 1 ≤ (n : ℝ) :=
…
```