OAI/Probability/InvariantIsing/Cavity/CavityTensorPressureMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal physical Haar/tree logarithmic mean equals dimension times the pressure used to choose the perturbation minima.

  1. lemma OAI.InvariantIsing.cavity_oriented_tensor_log_mean line 16
  2. theorem OAI.InvariantIsing.cavity_tensor_pressure_mean line 29