OAI/Probability/InvariantIsing/Cavity/CavityOrbitAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The stabilizer average only needs boundedness on the actual frame orbit. This includes logarithmic observables with unbounded extensions.

  1. theorem OAI.InvariantIsing.cavity_labeled_stabilizer_average_on_orbit line 14