MatrixEntropy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Entropy bounds for the actual matrix-to-body output

This intermediate lemma joins the proved geometric conversion to the scalar entropy estimates. The final construction supplies its literal matrix, separation and approximation list from the finite-field and compression theorems; none of these inputs is left as a final endpoint premise.

theorem OAI.MetricEntropyDuality.entropyPair_of_matrix line 28

Source documentation

Turn an actual separated and compressed matrix into the complete output record, including finite-cover witnesses and positivity of both cover counts.

theorem entropyPair_of_matrix {X : Type uX} {Y : Type uY} [Fintype X] [Fintype Y]
    [Nonempty X] [Nonempty Y] (a : ℝ) (ha : 1 ≤ a) (r : ℕ) (hr : 0 < r)
    (B : ℝ) (hB : 0 < B) (p : ℕ) (hp : p.Prime)
    (hprime : Real.exp (B * encodingCost (compressionRadius a) (accuracy a)
      (directionCount r (compressionRadius a) (accuracy a)) /
        (formDimension r (compressionRadius a) : ℝ)) < (p : ℝ))
    (g : Y → X → ℝ)
    (hrows : Fintype.card X = p ^ formDimension r (compressionRadius a))
    (hcolumns : Fintype.card X ≤ Fintype.card Y)
    (hsep : ∀ x x', x ≠ x' → ∃ y, 1 ≤ |g y x - g y x'|)
    (A : Finset (RealSpace X))
    (hA : UniformApproximation g (6 * accuracy a) A)
…

Mentions: OAI.MetricEntropyDuality.encodingCost, OAI.MetricEntropyDuality.compressionRadius, OAI.MetricEntropyDuality.accuracy, OAI.MetricEntropyDuality.directionCount, OAI.MetricEntropyDuality.formDimension, OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformApproximation