OAI/Probability/InvariantIsing/Magnetic/MagneticEntropyMaximum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Magnetic entropy identification from the proved scalar supporting inequality, with no additional concavity premise.

  1. theorem OAI.InvariantIsing.magnetic_entropy_sequence line 13
  2. theorem OAI.InvariantIsing.magnetic_entropy_trial_tendsto line 25
  3. theorem OAI.InvariantIsing.magnetic_entropy_trial_eventually_lower line 41