OAI/Probability/FreeIsing/Spins/Flip.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingSpin.flip line 11
  2. theorem OAI.Problem367.IsingSpin.flip_flip line 15
  3. theorem OAI.Problem367.IsingSpin.flip_injective line 18
  4. theorem OAI.Problem367.IsingSpin.flip_eq_flip line 21
  5. theorem OAI.Problem367.IsingSpin.flip_eq_iff line 24
  6. theorem OAI.Problem367.IsingSpin.measurable_flip line 28
  7. def OAI.Problem367.flipConfig line 32
  8. theorem OAI.Problem367.flipConfig_apply line 35
  9. theorem OAI.Problem367.flipConfig_flipConfig line 38
  10. theorem OAI.Problem367.measurable_flipConfig line 43
  11. def OAI.Problem367.flipConfigMeasurableEquiv line 48
  12. theorem OAI.Problem367.integral_eq_zero_of_flipConfig_odd line 56
  13. theorem OAI.Problem367.flipConfig_preimage_spin line 66
  14. theorem OAI.Problem367.measurableSet_spin_event line 72
  15. theorem OAI.Problem367.measure_even_event_inter_spin line 76
  16. theorem OAI.Problem367.twice_measure_even_event_inter_spin line 86
  17. theorem OAI.Problem367.setIntegral_spin_eq_half_of_flipConfig_even line 105
  18. theorem OAI.Problem367.freeCylinderWeight_flipConfig line 126
  19. theorem OAI.Problem367.HasFreeIsingLaw.map_flipConfig line 131