ConstructionDichotomyDenominator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Denominators after the construction's dilation

The actual dilation contains every primary part of a period of size at most twice the cutoff whose prime is at most the square of the dimension. Thus a reduced denominator is either one or exceeds the square of the dimension.

theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.short_period_dvd_lambda line 18
Source documentation
The actual dilation kills every period up to the dimension squared.
```
theorem short_period_dvd_lambda {k h : ℕ} (hh : 0 < h)
    (hmax : h ≤ 2 * cutoff k) (hshort : h ≤ dimension k ^ 2) :
    h ∣ lambda k :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.reducedDenominator_gt_of_not_dvd line 25
Source documentation
A nonintegral dilated fraction has denominator larger than the dimension squared. This applies to every natural numerator, including zero.
```
theorem reducedDenominator_gt_of_not_dvd {k h t : ℕ} (hh : 0 < h)
    (hmax : h ≤ 2 * cutoff k) (hnot : ¬ h ∣ lambda k * t) :
    dimension k ^ 2 < h / Nat.gcd h (lambda k * t) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda