TerminalPrimeGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A valid Ford row forbids three consecutive equal positive coordinates.

lemma OAI.TotientAsymptotic.ford_first_two_coefficient_sum line 10
lemma OAI.TotientAsymptotic.ford_row_forbids_flat_triple line 15
lemma OAI.TotientAsymptotic.terminal_strict_prime_gap line 48
Source documentation
At one of the last two boundaries there is a strict prime gap, and the residual largest coordinate is exactly the final one.
```
lemma terminal_strict_prime_gap {x : ℝ} {n L : ℕ} (hL : 3 ≤ L)
    (hpos : 0 < fordPrimeCoordinate n L)
    (hrow : fordRowSum L (fordPrimeCoordinate n) (L-2) ≤
      xi x (L-2)*fordPrimeCoordinate n (L-2)) :
    ∃ j : ℕ,L-1 ≤ j ∧ j ≤ L ∧
      fordPrime n j < fordPrime n (j-1) ∧
      fordPrimeCoordinate n j=fordPrimeCoordinate n L := by
…
```
Mentions: OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.fordPrimeCoordinate, OAI.TotientAsymptotic.fordRowSum, OAI.TotientAsymptotic.xi, OAI.TotientAsymptotic.fordPrime