OAI/Probability/InvariantIsing/Magnetic/MagneticCanonicalSpin.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual canonical spin law, including the ordinary Gaussian root. Its mean is the physical bias derivative, so optimizing the bias gives the requested group magnetizations exactly.

  1. def OAI.InvariantIsing.fieldCanonicalSpinLaw line 17
  2. instance OAI.InvariantIsing.fieldCanonicalSpinLaw_probability line 24
  3. theorem OAI.InvariantIsing.fieldCanonicalSpinLaw_mean line 29
  4. theorem OAI.InvariantIsing.fieldCanonicalSpinLaw_magnetic_mean line 40
  5. lemma OAI.InvariantIsing.spin_true_mean_of_spin_mean line 44
  6. theorem OAI.InvariantIsing.spinGroupCount_mean_of_site_means line 54
  7. theorem OAI.InvariantIsing.magneticCanonical_projection_distance line 75