DimensionRatio.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact dimension ratio and rank lower bound

These are identities for the canonical symmetric-form coefficient count. The ratio is used in the entropy estimate; the lower bound ensures that the constructed ambient dimensions diverge as the rank increases.

theorem OAI.MetricEntropyDuality.formDimension_mul_degree line 20
Source documentation
The multiplicative recurrence avoids any natural-number division.
```
theorem formDimension_mul_degree {r h : ℕ} (hr : 0 < r) (hh : 0 < h) :
    formDimension r h * h = formDimension r (h - 1) * (r + h - 1) := by
…
```
Mentions: OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.formDimension_prev_div line 32
Source documentation
The exact ratio of the previous-degree and current-degree dimensions.
```
theorem formDimension_prev_div {r h : ℕ} (hr : 0 < r) (hh : 0 < h) :
    (formDimension r (h - 1) : ℝ) / (formDimension r h : ℝ) =
      (h : ℝ) / ((r : ℝ) + h - 1) := by
…
```
Mentions: OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.rank_le_formDimension line 50
Source documentation
Every positive degree has at least as many coefficients as the rank.
```
theorem rank_le_formDimension {r h : ℕ} (hr : 0 < r) (hh : 0 < h) :
    r ≤ formDimension r h := by
…
```
Mentions: OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.formDimension_le_prime_power line 68
Source documentation
A field with at least two elements has more coefficient vectors than the number of coefficient coordinates.
```
theorem formDimension_le_prime_power {r h p : ℕ} (hp : 2 ≤ p) :
    formDimension r h ≤ p ^ formDimension r h :=
…
```
Mentions: OAI.MetricEntropyDuality.formDimension

theorem OAI.MetricEntropyDuality.dimension_growth_chain line 74

Source documentation

The explicit chain connecting rank to the actual ambient dimension.

theorem dimension_growth_chain {r h p n : ℕ} (hr : 0 < r) (hh : 0 < h)
    (hp : 2 ≤ p) (hn : p ^ formDimension r h ≤ n) :
    r ≤ formDimension r h ∧ formDimension r h ≤ p ^ formDimension r h ∧
      p ^ formDimension r h ≤ n :=
…

Mentions: OAI.MetricEntropyDuality.formDimension

theorem OAI.MetricEntropyDuality.rank_le_ambientDimension line 80
theorem OAI.MetricEntropyDuality.ambientDimension_pos line 84