OAI/Probability/InvariantIsing/Magnetic/MagneticFieldLevels.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual conditional squared spin means at prescribed magnetization. The root Gaussian is averaged at the optimizing bias.

  1. lemma OAI.InvariantIsing.field_measurable_tanh line 15
  2. def OAI.InvariantIsing.magneticLevelAtBias line 20
  3. lemma OAI.InvariantIsing.magneticLevelAtBias_allSquares line 26
  4. lemma OAI.InvariantIsing.magneticLevelAtBias_zero line 38
  5. lemma OAI.InvariantIsing.magneticLevelAtBias_mem_unit line 43
  6. lemma OAI.InvariantIsing.magneticLevelAtBias_monotone line 57
  7. lemma OAI.InvariantIsing.fieldBiasMean_sq_le_magneticLevel line 73
  8. def OAI.InvariantIsing.magneticFieldLevel line 94
  9. lemma OAI.InvariantIsing.magneticFieldLevel_mem_unit line 97
  10. lemma OAI.InvariantIsing.magneticFieldLevel_monotone line 101
  11. lemma OAI.InvariantIsing.sq_magnetization_le_magneticFieldLevel line 104
  12. def OAI.InvariantIsing.magneticFieldPath line 109
  13. lemma OAI.InvariantIsing.magneticFieldLevel_zero line 113