OAI/Probability/InvariantIsing/Magnetic/MagneticStationaryFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed terminal potential as an actual two-coordinate family. This permits use of the established affine Gaussian differentiation theorem for the inverse-coordinate time comparison.

  1. def OAI.InvariantIsing.magneticStationaryFamily line 15