OAI/Probability/InvariantIsing/Cavity/CavityTensorLogLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The physical and namespaced tensor models have the same expected logarithmic partition, preserving the fixed rotation and cascade tree.

  1. theorem OAI.InvariantIsing.tensorLeaf_log_mean_law line 14
  2. theorem OAI.InvariantIsing.cavity_rotation_tensor_log_mean line 42