EntropyPairLimits.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Limits for an actual family of constructed bodies

The family is indexed by rank j + 1, so every individual body has a positive dimension and positive primal entropy. Its defining properties concern the literal covering numbers; the limit arguments do not replace them by new abstract quantities.

theorem OAI.MetricEntropyDuality.tendsto_entropyBudget_successor_zero line 19
theorem OAI.MetricEntropyDuality.EntropyPair.family_dimension_atTop line 32
Source documentation
The actual dimensions tend to infinity; no monotonicity is required.
```
theorem family_dimension_atTop {a : ℝ}
    (P : ∀ j : ℕ, EntropyPair a (j + 1) ((j + 1 : ℕ) : ℝ)) :
    Tendsto (fun j => (P j).dimension) atTop atTop := by
…
```
Mentions: OAI.MetricEntropyDuality.EntropyPair
theorem OAI.MetricEntropyDuality.EntropyPair.family_ratio_tendsto_zero line 40
Source documentation
The quotient here is the actual dual entropy divided by the actual, strictly positive primal entropy at every index.
```
theorem family_ratio_tendsto_zero {a : ℝ}
    (P : ∀ j : ℕ, EntropyPair a (j + 1) ((j + 1 : ℕ) : ℝ)) :
    Tendsto (fun j => entropyRatio a (P j).body) atTop (𝓝 0) :=
…
```
Mentions: OAI.MetricEntropyDuality.EntropyPair, OAI.MetricEntropyDuality.entropyRatio