OAI/Probability/InvariantIsing/Core/ConditionalRelativeEntropy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact relative entropy of conditioning on a nonnull event.

  1. theorem OAI.InvariantIsing.conditioned_measure_entropy line 13