OAI/Probability/InvariantIsing/Cavity/CavityPhysicalProjectorIncrement.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.cavity_physical_projector_increment line 15