OAI/Probability/BinarySweep/Trajectories/PathTelescope.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.Sparse.prod_sub_one_telescope line 16
  2. abbrev OAI.BinaryCoordinateSweeps.Sparse.Suffixes line 30
  3. def OAI.BinaryCoordinateSweeps.Sparse.centeredLine line 32
  4. def OAI.BinaryCoordinateSweeps.Sparse.suffixLine line 34
  5. lemma OAI.BinaryCoordinateSweeps.Sparse.path_telescope_expansion line 38
  6. lemma OAI.BinaryCoordinateSweeps.Sparse.occurrences_le_of_injective line 62
  7. lemma OAI.BinaryCoordinateSweeps.Sparse.occurrences_sum line 71
  8. def OAI.BinaryCoordinateSweeps.Sparse.telescopeInjection line 78
  9. lemma OAI.BinaryCoordinateSweeps.Sparse.telescopeInjection_injective line 84
  10. lemma OAI.BinaryCoordinateSweeps.Sparse.telescope_occurrences_le line 97
  11. lemma OAI.BinaryCoordinateSweeps.Sparse.card_suffixes_le line 105
  12. theorem OAI.BinaryCoordinateSweeps.Sparse.pathMoment_light line 114
  13. lemma OAI.BinaryCoordinateSweeps.Sparse.fallingMoment_nonneg line 152
  14. lemma OAI.BinaryCoordinateSweeps.Sparse.fallingMoment_log line 156
  15. lemma OAI.BinaryCoordinateSweeps.Sparse.fallingMoment_le_exp line 173