OAI/Probability/BinarySweep/Processes/SupportTimeBoundBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinaryCoordinateSweeps.supportTimeBound_bounds line 11
  2. theorem OAI.BinaryCoordinateSweeps.support_ceiling_asymptotic line 74
  3. def OAI.BinaryCoordinateSweeps.boolSwitch line 86
  4. lemma OAI.BinaryCoordinateSweeps.sign_boolSwitch line 92
  5. lemma OAI.BinaryCoordinateSweeps.realSign_coordinateLayer line 101
  6. lemma OAI.BinaryCoordinateSweeps.sum_realSign_coordinateLayer line 112
  7. lemma OAI.BinaryCoordinateSweeps.realSign_binarySweep line 121
  8. lemma OAI.BinaryCoordinateSweeps.sum_realSign_binarySweep line 127
  9. lemma OAI.BinaryCoordinateSweeps.finiteLaw_expectation line 136
  10. theorem OAI.BinaryCoordinateSweeps.binary_sign_annihilated line 144
  11. lemma OAI.BinaryCoordinateSweeps.coordinateLayer_zero line 148
  12. lemma OAI.BinaryCoordinateSweeps.prod_reverse_ofFn_single line 155
  13. lemma OAI.BinaryCoordinateSweeps.binarySweep_zero line 164
  14. lemma OAI.BinaryCoordinateSweeps.binarySweep_singleLayer line 167
  15. def OAI.BinaryCoordinateSweeps.sweepReachable line 180
  16. lemma OAI.BinaryCoordinateSweeps.coordinateLayer_mem_reachable line 187
  17. lemma OAI.BinaryCoordinateSweeps.fiber_boolSwitch_eq_swap line 193