OAI/Probability/FreeIsing/Estimates/FairSpin.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.fairSpin line 11
  2. lemma OAI.Problem367.measurable_fairSpin line 14
  3. lemma OAI.Problem367.fairSpin_neg_preimage line 17
  4. lemma OAI.Problem367.fairSpin_pos_preimage line 21
  5. lemma OAI.Problem367.fairSpin_neg_mass line 25
  6. lemma OAI.Problem367.fairSpin_pos_mass line 38
  7. lemma OAI.Problem367.fairSpin_mass line 51
  8. def OAI.Problem367.fairSpinFactor line 56
  9. lemma OAI.Problem367.measurable_fairSpinFactor line 59
  10. lemma OAI.Problem367.fairSpinFactor_relabel line 62
  11. lemma OAI.Problem367.fairSpin_measurable_singleton line 65
  12. lemma OAI.Problem367.fairSpinFactor_cylinder line 68