OAI/Probability/BinarySweep/Processes/Basic.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryCoordinateSweeps.Coins line 11
  2. def OAI.BinaryCoordinateSweeps.physical line 13
  3. def OAI.BinaryCoordinateSweeps.physicalHistory line 21
  4. def OAI.BinaryCoordinateSweeps.physicalLaw line 24
  5. def OAI.BinaryCoordinateSweeps.c0 line 27
  6. def OAI.BinaryCoordinateSweeps.e0 line 28
  7. def OAI.BinaryCoordinateSweeps.cExponent line 29
  8. def OAI.BinaryCoordinateSweeps.eExponent line 30
  9. def OAI.BinaryCoordinateSweeps.traceMoment line 32
  10. def OAI.BinaryCoordinateSweeps.logMoment line 36
  11. lemma OAI.BinaryCoordinateSweeps.finiteLaw_nonneg line 41
  12. lemma OAI.BinaryCoordinateSweeps.finiteLaw_sum line 45
  13. lemma OAI.BinaryCoordinateSweeps.uniformLaw_sum line 51
  14. lemma OAI.BinaryCoordinateSweeps.finiteLaw_eq_zero_outside line 54
  15. lemma OAI.BinaryCoordinateSweeps.event_le_totalVariation line 63
  16. theorem OAI.BinaryCoordinateSweeps.uniform_image_support_obstruction line 79
  17. theorem OAI.BinaryCoordinateSweeps.physical_support_obstruction line 111
  18. def OAI.BinaryCoordinateSweeps.supportTimeBound line 118
  19. theorem OAI.BinaryCoordinateSweeps.physical_threshold_time line 122