OAI/Probability/BinarySweep/Processes/PointMassOne.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.pointMassOne_probability line 13
  2. lemma OAI.BinaryCoordinateSweeps.convolution_one_left line 19
  3. lemma OAI.BinaryCoordinateSweeps.convolution_one_right line 24
  4. lemma OAI.BinaryCoordinateSweeps.convolutionPower_probability line 29
  5. lemma OAI.BinaryCoordinateSweeps.convolutionPower_add line 35
  6. lemma OAI.BinaryCoordinateSweeps.convolutionPower_one line 43
  7. lemma OAI.BinaryCoordinateSweeps.convolutionPower_succ_right line 46
  8. lemma OAI.BinaryCoordinateSweeps.convolutionPower_block_bound line 50
  9. lemma OAI.BinaryCoordinateSweeps.convolutionPower_all_time_bound line 67
  10. lemma OAI.BinaryCoordinateSweeps.uniformLaw_le_one line 79
  11. theorem OAI.BinaryCoordinateSweeps.convolutionPower_tendsto_uniform line 83
  12. lemma OAI.BinaryCoordinateSweeps.finiteLaw_pos_of_mem line 108
  13. lemma OAI.BinaryCoordinateSweeps.convolution_pos_at_mul line 119
  14. lemma OAI.BinaryCoordinateSweeps.convolutionPower_pos_list line 127
  15. lemma OAI.BinaryCoordinateSweeps.convolutionPower_pos_later line 137
  16. lemma OAI.BinaryCoordinateSweeps.finiteLaw_fullSupport_power line 149
  17. theorem OAI.BinaryCoordinateSweeps.fixed_dimension_sweep_convergence line 166
  18. lemma OAI.BinaryCoordinateSweeps.finiteLaw_reindex line 177
  19. lemma OAI.BinaryCoordinateSweeps.finiteLaw_independent_mul line 184