OAI/Probability/InvariantIsing/Magnetic/RestrictedPhysicalProjectorIncrement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An additive lower bound for the literal full-system log partition, written entirely in the physical projector and compression data.

  1. theorem OAI.InvariantIsing.restricted_physical_projector_increment line 15