OAI/Probability/InvariantIsing/Magnetic/MagneticWeightedGenerator.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted continuation curvature has a bounded potential in the physical inverse-mean coordinate.

  1. lemma OAI.InvariantIsing.weighted_inverse_continuation_generator line 12
  2. lemma OAI.InvariantIsing.fieldBiasFourth_quotient_bound line 21
  3. lemma OAI.InvariantIsing.magnetic_weighted_curvature_second_bound line 27
  4. lemma OAI.InvariantIsing.magnetic_weighted_potential_bound line 47