OAI/Probability/Ballisticity/Estimates/IidListProcess.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.iid_list_hasLaw line 14
  2. lemma OAI.DirectionalTransience.partialSumMax_initial_congr line 31
  3. def OAI.DirectionalTransience.listCenteredMax line 42
  4. lemma OAI.DirectionalTransience.listCenteredMax_ofFn line 45
  5. def OAI.DirectionalTransience.symmetricClip line 64
  6. lemma OAI.DirectionalTransience.symmetricClip_apply line 78
  7. lemma OAI.DirectionalTransience.symmetricClip_bound line 80
  8. lemma OAI.DirectionalTransience.symmetricClip_neg line 84
  9. lemma OAI.DirectionalTransience.symmetricClip_uniformContinuous line 98
  10. lemma OAI.DirectionalTransience.symmetricClip_gaussian_integral line 105
  11. lemma OAI.DirectionalTransience.symmetricClip_eq_self line 125
  12. lemma OAI.DirectionalTransience.symmetricClip_nat_eventually line 129
  13. def OAI.DirectionalTransience.clippedBCF line 133
  14. lemma OAI.DirectionalTransience.clippedBCF_apply line 136
  15. lemma OAI.DirectionalTransience.clippedBCF_uniformContinuous line 138
  16. lemma OAI.DirectionalTransience.clippedBCF_norm_bound line 145
  17. lemma OAI.DirectionalTransience.clippedBCF_nat_tendsto line 148
  18. lemma OAI.DirectionalTransience.integral_clippedBCF_tendsto line 154
  19. lemma OAI.DirectionalTransience.integral_weighted_clippedBCF_tendsto line 165