OAI/Probability/BinarySweep/FiniteLaws/CyclicHolder.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Cyclic.chainWeight line 12
  2. lemma OAI.BinaryCoordinateSweeps.Cyclic.chainWeight_cons line 16
  3. lemma OAI.BinaryCoordinateSweeps.Cyclic.sum_chainWeight line 24
  4. def OAI.BinaryCoordinateSweeps.Cyclic.deletedWeight line 37
  5. lemma OAI.BinaryCoordinateSweeps.Cyclic.deletedWeight_last line 42
  6. lemma OAI.BinaryCoordinateSweeps.Cyclic.deletedWeight_reindex line 50
  7. lemma OAI.BinaryCoordinateSweeps.Cyclic.sum_deletedWeight line 70
  8. lemma OAI.BinaryCoordinateSweeps.Cyclic.deletedWeight_nonneg line 86
  9. lemma OAI.BinaryCoordinateSweeps.Cyclic.prod_deletedWeight line 96
  10. lemma OAI.BinaryCoordinateSweeps.Cyclic.prod_deletedWeight_rpow line 113
  11. theorem OAI.BinaryCoordinateSweeps.Cyclic.sum_cycle_rpow_le_card line 126