OAI/Probability/InvariantIsing/Cavity/CavityEnvelopeTelescoping.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A vanishing-error comparison transfers a cavity increment bound through the scalar pressure envelope and back to the ordinary normalized pressure.

  1. theorem OAI.InvariantIsing.cavity_envelope_progression_lower line 14