Dilation.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QuantitativeVanDerWaerden.dilationPrimes line 14
Source documentation
The primes up to the short-period cutoff.
```
def dilationPrimes (h₀ : ℕ) : Finset ℕ :=
…
```
theorem OAI.QuantitativeVanDerWaerden.mem_dilationPrimes line 17
def OAI.QuantitativeVanDerWaerden.dilation line 22
theorem OAI.QuantitativeVanDerWaerden.dilation_pos line 25
theorem OAI.QuantitativeVanDerWaerden.dilation_ne_zero line 31
theorem OAI.QuantitativeVanDerWaerden.prime_pow_dvd_dilation line 34
theorem OAI.QuantitativeVanDerWaerden.primary_part_dvd_dilation line 44
theorem OAI.QuantitativeVanDerWaerden.short_period_dvd_dilation line 51
Source documentation
Every positive period up to the cutoff is killed by the dilation.
```
theorem short_period_dvd_dilation {h₀ M h : ℕ}
    (hh : 0 < h) (hshort : h ≤ h₀) (hmax : h ≤ 2 * M) :
    h ∣ dilation h₀ M := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.dilation
theorem OAI.QuantitativeVanDerWaerden.dilation_le_pow line 62
Source documentation
The natural-number bound that yields log λ ≤ h₀ * log (2M).
```
theorem dilation_le_pow {h₀ M : ℕ} (hM : 0 < M) :
    dilation h₀ M ≤ (2 * M) ^ h₀ := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.dilation
theorem OAI.QuantitativeVanDerWaerden.log_dilation_le line 74
Source documentation
The explicit logarithmic size bound from the dilation lemma.
```
theorem log_dilation_le {h₀ M : ℕ} (hM : 0 < M) :
    Real.log (dilation h₀ M) ≤ (h₀ : ℝ) * Real.log (2 * M) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.dilation
theorem OAI.QuantitativeVanDerWaerden.dilation_coprime_prime_pow line 83
Source documentation
Large prime powers are relatively prime to the dilation.
```
theorem dilation_coprime_prime_pow {h₀ M P a : ℕ}
    (hP : P.Prime) (hlarge : h₀ < P) :
    Nat.Coprime (dilation h₀ M) (P ^ a) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.dilation

theorem OAI.QuantitativeVanDerWaerden.prime_dvd_reducedDenominator_gt_of_primary_parts line 96

Source documentation

If a multiplier contains every small primary part of the period, reducing the resulting fraction removes every small prime from its denominator.

theorem prime_dvd_reducedDenominator_gt_of_primary_parts
    {h h₀ L t : ℕ} (hh : 0 < h)
    (hL : ∀ p : ℕ, p.Prime → p ≤ h₀ → p ^ h.factorization p ∣ L)
    {p : ℕ} (hp : p.Prime) (hpd : p ∣ h / Nat.gcd h (L * t)) : h₀ < p := by
…

theorem OAI.QuantitativeVanDerWaerden.reducedDenominator_eq_one_or_gt_of_primary_parts line 118

theorem OAI.QuantitativeVanDerWaerden.prime_dvd_dilatedDenominator_gt line 133

Source documentation

Dilation removes every small prime from a reduced denominator.

theorem prime_dvd_dilatedDenominator_gt {h₀ M h p : ℕ} (t : ℤ)
    (hh : 0 < h) (hmax : h ≤ 2 * M) (hp : p.Prime)
    (hpd : p ∣ h / Int.gcd (h : ℤ) ((dilation h₀ M : ℤ) * t)) : h₀ < p := by
…

Mentions: OAI.QuantitativeVanDerWaerden.dilation

theorem OAI.QuantitativeVanDerWaerden.dilatedDenominator_eq_one_or_gt line 140