OAI/Probability/Ballisticity/Estimates/TailSampling.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TailSampling.cutKernel line 15
  2. lemma OAI.TailSampling.cutKernel_apply line 29
  3. lemma OAI.TailSampling.cutKernel_markov line 33
  4. lemma OAI.TailSampling.cutKernel_supported line 44
  5. lemma OAI.TailSampling.cutKernel_mass_mul line 49
  6. lemma OAI.TailSampling.coordinate_atom_pos line 55
  7. lemma OAI.TailGrowth.log_integral_lower_of_exp line 79
  8. lemma OAI.TailGrowth.log_integral_lower line 106
  9. lemma OAI.TailGrowth.measurable_statistic line 128
  10. lemma OAI.TailGrowth.statistic_translate line 135
  11. lemma OAI.TailGrowth.comp_mono_left line 155
  12. lemma OAI.TailGrowth.smul_mono_scalar line 164
  13. lemma OAI.TailGrowth.normalized_tail_dominated line 171
  14. lemma OAI.TailGrowth.continued_tail_dominated line 184
  15. lemma OAI.TailGrowth.stream_real_lower line 196
  16. lemma OAI.TailGrowth.prod_comp line 203