OAI/Probability/InvariantIsing/Magnetic/MagneticPhysicalIncrementLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A conditional physical cavity-increment lower bound with the actual perturbation minima constructed, rather than assumed.

  1. theorem OAI.InvariantIsing.magnetic_physical_increment_eventually_lower line 12