OAI/Probability/InvariantIsing/Magnetic/MagneticVariational.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The prescribed-magnetization variational expression in (7.3)--(7.4). One common covariance path is used for every field group.

  1. def OAI.InvariantIsing.magneticGroupValue line 14

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:154 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.magneticGroupValue@path.

  2. def OAI.InvariantIsing.magneticEntropyFunctional line 17

    Also declared: ComparatorChallenges/InvariantIsing.lean:159 (same declaration text).

  3. def OAI.InvariantIsing.magneticVariationalFunctional line 21

    Also declared: ComparatorChallenges/InvariantIsing.lean:163 (same declaration text).

  4. def OAI.InvariantIsing.RationalMagnetization line 24

    Also declared: ComparatorChallenges/InvariantIsing.lean:166 (same declaration text).

  5. instance OAI.InvariantIsing.(instance at line 26) line 26
  6. def OAI.InvariantIsing.finiteMagneticFunctional line 29

    Also declared: ComparatorChallenges/InvariantIsing.lean:168 (same declaration text).

  7. lemma OAI.InvariantIsing.magneticGroupValue_zero line 34
  8. lemma OAI.InvariantIsing.magneticGroupValue_le line 40
  9. lemma OAI.InvariantIsing.magneticEntropyFunctional_le line 50
  10. lemma OAI.InvariantIsing.magneticEntropyFunctional_zero line 60
  11. lemma OAI.InvariantIsing.magneticVariationalFunctional_zero line 65
  12. lemma OAI.InvariantIsing.magneticVariationalFunctional_le line 71
  13. lemma OAI.InvariantIsing.finiteMagneticFunctional_lower line 79
  14. lemma OAI.InvariantIsing.finiteMagneticFunctional_upper line 89