EntropyComparison.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Real scalar entropy comparisons

The encoding term is controlled by choosing the field size after all other parameters. The final lemmas transfer bounds for the finite approximation list to bounds for covering numbers. Their hypotheses are scalar inequalities, so natural cardinalities can be inserted by casting.

theorem OAI.MetricEntropyDuality.encoding_ratio_bounds line 23

Source documentation

A sufficiently large field size makes the encoding contribution arbitrarily small. This formulation also records its nonnegativity.

theorem encoding_ratio_bounds {r C D p : ℝ}
    (hr : 0 < r) (hC : 0 ≤ C) (hD : 0 < D)
    (hp : Real.exp (r * C / D) < p) (hp1 : 1 < p) :
    0 ≤ 2 * C / (D * Real.log p) ∧ 2 * C / (D * Real.log p) < 2 / r := by
…

theorem OAI.MetricEntropyDuality.encoding_ratio_lt line 37
theorem OAI.MetricEntropyDuality.encoding_ratio_le line 43

theorem OAI.MetricEntropyDuality.entropy_budget_lt line 51

Source documentation

The rank and field-size choices each contribute less than one quarter of the reciprocal proposed comparison constant.

theorem entropy_budget_lt {b C D H R p : ℝ}
    (hb : 1 ≤ b) (hC : 0 ≤ C) (hD : 0 < D) (hH : 0 ≤ H)
    (hR : 8 * b * H < R)
    (hp : Real.exp (8 * b * C / D) < p) (hp1 : 1 < p) :
    2 * H / R + 2 * C / (D * Real.log p) < 1 / (2 * b) := by
…

theorem OAI.MetricEntropyDuality.entropy_ratio_nonneg line 70
Source documentation
The entropy ratio is nonnegative when both covering counts have the usual positive lower bounds.
```
theorem entropy_ratio_nonneg {N dual : ℝ} (hN : 1 < N) (hdual : 1 ≤ dual) :
    0 ≤ Real.log dual / Real.log N :=
…
```

theorem OAI.MetricEntropyDuality.entropy_ratio_bounds line 76

Source documentation

Increasing the denominator and decreasing the nonnegative numerator preserves the upper entropy-ratio bound.

theorem entropy_ratio_bounds {N m dual Q : ℝ}
    (hm : 1 < m) (hNm : m ≤ N) (hdual : 1 ≤ dual) (hdualQ : dual ≤ Q ^ 2) :
    0 ≤ Real.log dual / Real.log N ∧
      Real.log dual / Real.log N ≤ Real.log (Q ^ 2) / Real.log m := by
…

theorem OAI.MetricEntropyDuality.entropy_strict_comparison line 96

Source documentation

The strict finite entropy-ratio estimate contradicts the proposed covering comparison after inserting the geometric lower and upper bounds.

theorem entropy_strict_comparison {N m dual Q b : ℝ}
    (hm : 1 < m) (hNm : m ≤ N) (hdual : 1 ≤ dual) (hdualQ : dual ≤ Q ^ 2)
    (hb : 1 ≤ b)
    (hratio : Real.log (Q ^ 2) / Real.log m < 1 / (2 * b)) :
    b * Real.log dual < Real.log N := by
…