OAI/Probability/InvariantIsing/Core/FiniteProjectionTrial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A trial measure obtained by pushing canonical spins through a finite map. The log-partition loss consists of the expected energy loss and the entropy of the projection.

  1. theorem OAI.InvariantIsing.log_sum_exp_projection_bound line 14