GenericAsymptotics.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Growth comparisons for the absolute parameter threshold

These comparisons concern only the progression length and fixed real constants. They contain no color-count parameter and can therefore be combined before the digit-product transfer to choose one absolute threshold.

theorem OAI.QuantitativeVanDerWaerden.Scaling.eventually_rpow_log_le_real line 26
Source documentation
A fixed power times a logarithm is eventually bounded by any prescribed positive multiple of a strictly larger power.
```
theorem eventually_rpow_log_le_real {a b C eps : ℝ}
    (hab : a < b) (hC : 0 ≤ C) (he : 0 < eps) :
    ∀ᶠ x : ℝ in atTop, C * x ^ a * Real.log x ≤ eps * x ^ b := by
…
```

theorem OAI.QuantitativeVanDerWaerden.Scaling.eventually_rpow_log_le line 51

Source documentation

Natural-input version of the power-logarithm comparison.

theorem eventually_rpow_log_le {a b C eps : ℝ}
    (hab : a < b) (hC : 0 ≤ C) (he : 0 < eps) :
    ∀ᶠ k : ℕ in atTop,
      C * (k : ℝ) ^ a * Real.log k ≤ eps * (k : ℝ) ^ b :=
…

theorem OAI.QuantitativeVanDerWaerden.Scaling.eventually_rpow_le_real line 59
Source documentation
A fixed multiple of a power is eventually smaller than a prescribed positive multiple of any strictly larger power.
```
theorem eventually_rpow_le_real {a b C eps : ℝ}
    (hab : a < b) (_hC : 0 ≤ C) (he : 0 < eps) :
    ∀ᶠ x : ℝ in atTop, C * x ^ a ≤ eps * x ^ b := by
…
```

theorem OAI.QuantitativeVanDerWaerden.Scaling.eventually_rpow_le line 75

Source documentation

Natural-input version of the power comparison.

theorem eventually_rpow_le {a b C eps : ℝ}
    (hab : a < b) (hC : 0 ≤ C) (he : 0 < eps) :
    ∀ᶠ k : ℕ in atTop, C * (k : ℝ) ^ a ≤ eps * (k : ℝ) ^ b :=
…

theorem OAI.QuantitativeVanDerWaerden.Scaling.tendsto_nat_rpow_atTop line 81
Source documentation
Every positive real power of natural numbers tends to infinity.
```
theorem tendsto_nat_rpow_atTop {t : ℝ} (ht : 0 < t) :
    Tendsto (fun k : ℕ => (k : ℝ) ^ t) atTop atTop :=
…
```
theorem OAI.QuantitativeVanDerWaerden.Scaling.eventually_le_nat_rpow line 87
Source documentation
An arbitrary fixed lower threshold is eventually crossed by a positive real power of natural numbers.
```
theorem eventually_le_nat_rpow {t : ℝ} (ht : 0 < t) (L : ℝ) :
    ∀ᶠ k : ℕ in atTop, L ≤ (k : ℝ) ^ t :=
…
```
theorem OAI.QuantitativeVanDerWaerden.Scaling.tendsto_nat_rpow_neg_zero line 92
Source documentation
Negative powers of natural numbers tend to zero.
```
theorem tendsto_nat_rpow_neg_zero {t : ℝ} (ht : 0 < t) :
    Tendsto (fun k : ℕ => (k : ℝ) ^ (-t)) atTop (𝓝 0) :=
…
```
theorem OAI.QuantitativeVanDerWaerden.Scaling.tendsto_exp_rpow_log_sub_rpow_real line 98
Source documentation
A positive power in the negative exponent dominates any lower power times a logarithm. The hypothesis 0 < t is needed for decay to zero.
```
theorem tendsto_exp_rpow_log_sub_rpow_real {a t C b : ℝ}
    (hat : a < t) (hC : 0 ≤ C) (hb : 0 < b) (ht : 0 < t) :
    Tendsto (fun x : ℝ => Real.exp (C * x ^ a * Real.log x - b * x ^ t))
      atTop (𝓝 0) := by
…
```

theorem OAI.QuantitativeVanDerWaerden.Scaling.tendsto_exp_rpow_log_sub_rpow line 113

Source documentation

Natural-input exponential decay, used in both perturbation union bounds.

theorem tendsto_exp_rpow_log_sub_rpow {a t C b : ℝ}
    (hat : a < t) (hC : 0 ≤ C) (hb : 0 < b) (ht : 0 < t) :
    Tendsto (fun k : ℕ =>
      Real.exp (C * (k : ℝ) ^ a * Real.log k - b * (k : ℝ) ^ t))
      atTop (𝓝 0) := by
…

theorem OAI.QuantitativeVanDerWaerden.Scaling.tendsto_rpow_mul_exp_neg_rpow line 124
Source documentation
An exponential of a negative positive power dominates every polynomial prefactor, including the finite number of local pattern lengths.
```
theorem tendsto_rpow_mul_exp_neg_rpow {a b t : ℝ}
    (hb : 0 < b) (ht : 0 < t) :
    Tendsto (fun k : ℕ =>
      (k : ℝ) ^ a * Real.exp (-b * (k : ℝ) ^ t)) atTop (𝓝 0) := by
…
```