OAI/Probability/InvariantIsing/Magnetic/RestrictedGroupedCappedLog.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fresh group rotations inside the actual capped logarithm. The base Gaussian Hamiltonian and its original Gibbs normalization are preserved by the labeled-projector stabilizer.

  1. theorem OAI.InvariantIsing.restricted_grouped_capped_log_average line 17