Asymptotics.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Entropy-ratio convergence and growing ambient dimension

For fixed degree and pivot count, the explicit rational entropy bound tends to zero. The dimension conclusions use the actual cardinality lower bound from the construction, together with the fact that a prime field has at least two elements.

def OAI.MetricEntropyDuality.entropyRatioBound line 22
Source documentation
An asymptotic upper bound for the entropy ratio.
```
noncomputable def entropyRatioBound (h s r : ℕ) : ℝ :=
…
```
theorem OAI.MetricEntropyDuality.tendsto_entropyRatioBound_zero line 25
theorem OAI.MetricEntropyDuality.tendsto_zero_of_le_entropyRatioBound line 42
Source documentation
Eventual two-sided estimates suffice; no monotonicity of the actual entropy ratios is required.
```
theorem tendsto_zero_of_le_entropyRatioBound {h s : ℕ} {f : ℕ → ℝ}
    (hbound : ∀ᶠ r in atTop, 0 ≤ f r ∧ f r ≤ entropyRatioBound h s r) :
    Tendsto f atTop (𝓝 0) :=
…
```
Mentions: OAI.MetricEntropyDuality.entropyRatioBound
theorem OAI.MetricEntropyDuality.tendsto_zero_of_positive_rank_bound line 50
Source documentation
A construction indexed only by positive ranks supplies the needed eventual entropy estimates directly.
```
theorem tendsto_zero_of_positive_rank_bound {h s : ℕ} {f : ℕ → ℝ}
    (hbound : ∀ r, 0 < r → 0 ≤ f r ∧ f r ≤ entropyRatioBound h s r) :
    Tendsto f atTop (𝓝 0) :=
…
```
Mentions: OAI.MetricEntropyDuality.entropyRatioBound
theorem OAI.MetricEntropyDuality.tendsto_formDimension_atTop line 56
theorem OAI.MetricEntropyDuality.tendsto_ambientDimension_atTop line 63
Source documentation
Actual ambient dimensions dominate the rank, even when the chosen primes and dimensions fluctuate with it.
```
theorem tendsto_ambientDimension_atTop {h : ℕ} (hh : 0 < h)
    {p n : ℕ → ℕ} (hp : ∀ r, 0 < r → 2 ≤ p r)
    (hn : ∀ r, 0 < r → p r ^ formDimension r h ≤ n r) :
    Tendsto n atTop atTop := by
…
```
Mentions: OAI.MetricEntropyDuality.formDimension

theorem OAI.MetricEntropyDuality.tendsto_ambientDimension_atTop_of_prime line 72

Source documentation

Primality supplies the field-size condition in the concrete sequence.

theorem tendsto_ambientDimension_atTop_of_prime {h : ℕ} (hh : 0 < h)
    {p n : ℕ → ℕ} (hp : ∀ r, 0 < r → (p r).Prime)
    (hn : ∀ r, 0 < r → p r ^ formDimension r h ≤ n r) :
    Tendsto n atTop atTop :=
…

Mentions: OAI.MetricEntropyDuality.formDimension