OAI/Probability/FreeIsing/Estimates/FreeLawSymmetry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.HasFreeIsingLaw.flip_invariant line 12
2. theorem OAI.Problem367.HasFreeIsingLaw.measurePreserving_flipConfig line 17
3. theorem OAI.Problem367.HasFreeIsingLaw.integral_odd line 22
4. theorem OAI.Problem367.HasFreeIsingLaw.measure_even_event_inter_spin line 28
5. theorem OAI.Problem367.HasFreeIsingLaw.setIntegral_spin_even line 35