OAI/Probability/Ballisticity/Estimates/ClippedInverse.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.quenched_stayUntil_ball_locality line 12
  2. lemma OAI.DirectionalTransience.noDropFinite_measurable_ball line 23
  3. lemma OAI.DirectionalTransience.noDropFinite_translation line 30
  4. lemma OAI.DirectionalTransience.noDropQuenched_le_finite line 46
  5. lemma OAI.DirectionalTransience.noDropFinite_tendsto line 50
  6. def OAI.DirectionalTransience.clippedInverse line 63
  7. lemma OAI.DirectionalTransience.clippedInverse_measurable line 66
  8. lemma OAI.DirectionalTransience.clippedInverse_bounds line 69
  9. lemma OAI.DirectionalTransience.clippedInverse_antitone line 74
  10. lemma OAI.DirectionalTransience.clippedInverse_tendsto line 80
  11. lemma OAI.DirectionalTransience.noDrop_clipped_inverse_L1 line 87
  12. lemma OAI.DirectionalTransience.fresh_rows_prod line 112
  13. lemma OAI.DirectionalTransience.nonneg_prod_le_const line 141
  14. lemma OAI.DirectionalTransience.prod_difference_bound line 148
  15. lemma OAI.DirectionalTransience.clipped_inverse_integral_translation line 184
  16. lemma OAI.DirectionalTransience.clipped_inverse_finite_integral_translation line 196
  17. lemma OAI.DirectionalTransience.integrable_of_nonneg_bound line 208
  18. lemma OAI.DirectionalTransience.clipped_inverse_integrable line 215
  19. lemma OAI.DirectionalTransience.clipped_inverse_integral_gap line 222
  20. lemma OAI.DirectionalTransience.separated_clipped_inverse_product line 237
  21. lemma OAI.DirectionalTransience.latticeBall_disjoint_of_coordinate_gap line 315
  22. lemma OAI.DirectionalTransience.noDrop_real_inverse_moment line 327
  23. lemma OAI.DirectionalTransience.prod_max_bound line 344
  24. lemma OAI.DirectionalTransience.noDropQuenched_toReal_le_one line 364
  25. def OAI.DirectionalTransience.noDropProduct line 369
  26. def OAI.DirectionalTransience.clippedNoDropProduct line 372
  27. lemma OAI.DirectionalTransience.noDropProduct_bounds line 376
  28. lemma OAI.DirectionalTransience.clippedNoDropProduct_bounds line 382
  29. lemma OAI.DirectionalTransience.clippedNoDropProduct_error line 393
  30. lemma OAI.DirectionalTransience.noDropProduct_measurable line 400
  31. lemma OAI.DirectionalTransience.clippedNoDropProduct_measurable line 406
  32. lemma OAI.DirectionalTransience.clippedNoDropProduct_inverse line 413
  33. lemma OAI.DirectionalTransience.separated_noDropProduct_inverse_bound line 420