OAI/Probability/SignedSweeps/SubsetSweep.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.realSiteRepresentation line 14
  2. def OAI.SignedSweeps.subsetRepresentation line 22
  3. lemma OAI.SignedSweeps.fairAction_site line 30
  4. lemma OAI.SignedSweeps.fairAction_subset line 38
  5. lemma OAI.SignedSweeps.switch_product_inclusion_bound line 57
  6. lemma OAI.SignedSweeps.coordinate_inclusion_bound line 80
  7. def OAI.SignedSweeps.realSiteSweep line 92
  8. def OAI.SignedSweeps.subsetSweep line 96
  9. lemma OAI.SignedSweeps.subsetSweep_inclusion_bound line 100
  10. lemma OAI.SignedSweeps.realSiteAverage_complexify line 118
  11. lemma OAI.SignedSweeps.realSiteSweep_complexify line 128
  12. lemma OAI.SignedSweeps.realSiteSweep_uniform line 146
  13. lemma OAI.SignedSweeps.subset_indicator_product line 163
  14. lemma OAI.SignedSweeps.subsetSweep_upper_inclusion line 186