OAI/LinearAlgebra/MatrixMultiplication/Entropy/IndependentConditioning.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. theorem OAI.MatrixMultiplication.CompletionLaws.condition_map_mass line 17
  2. theorem OAI.MatrixMultiplication.CompletionLaws.joint_event_sum line 27
  3. theorem OAI.MatrixMultiplication.CompletionLaws.condition_independent_coordinate_mass line 53
  4. theorem OAI.MatrixMultiplication.CompletionLaws.uniform_coordinate_independent_condition line 67