EntropyBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

From finite compression counts to entropy bounds

The counting premise is the literal finite encoding bound. Its logarithmic conversion and the exact symmetric-form dimension ratio give the scalar entropy comparison used after the matrix-to-body construction.

theorem OAI.MetricEntropyDuality.log_count_le_encodingCost line 25

Source documentation

Taking logarithms of the literal finite encoding count.

theorem log_count_le_encodingCost {h u q Q : ℕ} {θ : ℝ}
    (hu : 0 < u) (hq : 0 < q) (hθ : 0 < θ) (hQ : 0 < Q)
    (hcount : (Q : ℝ) ≤ (u : ℝ) * (q : ℝ) ^ (h * pivotSlots θ) *
      (1 + (pivotSlots θ : ℝ) * (2 : ℝ) ^ u / θ) ^
        (h * pivotSlots θ * 2 ^ u)) :
    Real.log (Q : ℝ) ≤ (h : ℝ) * (pivotSlots θ : ℝ) * Real.log (q : ℝ) +
      encodingCost h θ u := by
…

Mentions: OAI.MetricEntropyDuality.pivotSlots, OAI.MetricEntropyDuality.encodingCost

theorem OAI.MetricEntropyDuality.log_card_le_encodingCost line 49

Source documentation

Finite-list version retaining the actual nonempty approximating family.

theorem log_card_le_encodingCost {α : Type uα} {A : Finset α} {h u q : ℕ} {θ : ℝ}
    (hu : 0 < u) (hq : 0 < q) (hθ : 0 < θ) (hA : A.Nonempty)
    (hcount : (A.card : ℝ) ≤ (u : ℝ) * (q : ℝ) ^ (h * pivotSlots θ) *
      (1 + (pivotSlots θ : ℝ) * (2 : ℝ) ^ u / θ) ^
        (h * pivotSlots θ * 2 ^ u)) :
    Real.log (A.card : ℝ) ≤ (h : ℝ) * (pivotSlots θ : ℝ) * Real.log (q : ℝ) +
      encodingCost h θ u :=
…

Mentions: OAI.MetricEntropyDuality.pivotSlots, OAI.MetricEntropyDuality.encodingCost

theorem OAI.MetricEntropyDuality.log_square_ratio_le_of_log_bound line 59

Source documentation

The algebraic ratio calculation before substituting symmetric dimensions.

theorem log_square_ratio_le_of_log_bound {Q p D E h s C : ℝ}
    (hp : 1 < p) (hD : 0 < D)
    (hQ : Real.log Q ≤ h * s * E * Real.log p + C) :
    Real.log (Q ^ 2) / (D * Real.log p) ≤
      2 * h * s * (E / D) + 2 * C / (D * Real.log p) := by
…

theorem OAI.MetricEntropyDuality.form_entropy_ratio_le line 76

Source documentation

The exact binomial ratio converts label entropy into the rank term.

theorem form_entropy_ratio_le {r h s p Q : ℕ} {C : ℝ}
    (hr : 0 < r) (hh : 0 < h) (hp : 1 < p)
    (hQ : Real.log (Q : ℝ) ≤ (h : ℝ) * (s : ℝ) *
      Real.log ((p : ℝ) ^ formDimension r (h - 1)) + C) :
    Real.log ((Q : ℝ) ^ 2) / Real.log ((p : ℝ) ^ formDimension r h) ≤
      2 * (h : ℝ) ^ 2 * (s : ℝ) / ((r : ℝ) + h - 1) +
        2 * C / ((formDimension r h : ℝ) * Real.log (p : ℝ)) := by
…

Mentions: OAI.MetricEntropyDuality.formDimension

theorem OAI.MetricEntropyDuality.form_entropy_ratio_le_of_count line 98

Source documentation

Specialization using the actual finite positive-list count and the label bound q = p ^ D_(h-1).

theorem form_entropy_ratio_le_of_count {r h p u Q : ℕ} {θ : ℝ}
    (hr : 0 < r) (hh : 0 < h) (hp : 1 < p) (hu : 0 < u)
    (hθ : 0 < θ) (hQ : 0 < Q)
    (hcount : (Q : ℝ) ≤ (u : ℝ) *
      ((p ^ formDimension r (h - 1) : ℕ) : ℝ) ^ (h * pivotSlots θ) *
        (1 + (pivotSlots θ : ℝ) * (2 : ℝ) ^ u / θ) ^
          (h * pivotSlots θ * 2 ^ u)) :
    Real.log ((Q : ℝ) ^ 2) / Real.log ((p : ℝ) ^ formDimension r h) ≤
      2 * (h : ℝ) ^ 2 * (pivotSlots θ : ℝ) / ((r : ℝ) + h - 1) +
        2 * encodingCost h θ u / ((formDimension r h : ℝ) * Real.log (p : ℝ)) := by
…

Mentions: OAI.MetricEntropyDuality.formDimension, OAI.MetricEntropyDuality.pivotSlots, OAI.MetricEntropyDuality.encodingCost