# The corners theorem and Roth's theorem #

This file proves the corners theorem and Roth's theorem on arithmetic progressions of length three.

## References #

An explicit form for the constant in the corners theorem.

Note that this depends on `SzemerediRegularity.bound`

, which is a tower-type exponential. This means
`cornersTheoremBound`

is in practice absolutely tiny.

## Equations

- cornersTheoremBound ε = ⌊(SimpleGraph.triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ + 1

## Instances For

The **corners theorem** for finite abelian groups.

The maximum density of a corner-free set in `G × G`

goes to zero as `|G|`

tends to infinity.

The **corners theorem** for `ℕ`

.

The maximum density of a corner-free set in `{1, ..., n} × {1, ..., n}`

goes to zero as `n`

tends to
infinity.

**Roth's theorem** for finite abelian groups.

The maximum density of a 3AP-free set in `G`

goes to zero as `|G|`

tends to infinity.

**Roth's theorem** for `ℕ`

.

The maximum density of a 3AP-free set in `{1, ..., n}`

goes to zero as `n`

tends to infinity.