OAI/Probability/InvariantIsing/Magnetic/MagneticHeatWeighted.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual drift-free equation for q²Hᵤᵤ along the inverse mean. All time derivatives come from normalized Gaussian averages.

  1. def OAI.InvariantIsing.magneticHeatWeighted line 16
  2. lemma OAI.InvariantIsing.magneticHeatWeighted_eq line 22
  3. theorem OAI.InvariantIsing.magneticHeatWeighted_inverse_hasDerivAt line 35