OAI/Probability/Ballisticity/Estimates/SmallScaleGaussianMass.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.dyadic_inv_tendsto line 15
  2. theorem OAI.DirectionalTransience.small_scale_gaussian_mass line 19
  3. def OAI.DirectionalTransience.bandTruncate line 75
  4. lemma OAI.DirectionalTransience.measurable_bandTruncate line 76
  5. lemma OAI.DirectionalTransience.bandTruncate_bound line 78
  6. lemma OAI.DirectionalTransience.bandTruncate_neg line 87
  7. lemma OAI.DirectionalTransience.bandTruncate_cost_identity line 90
  8. lemma OAI.DirectionalTransience.integral_truncatedTailCost line 110
  9. lemma OAI.DirectionalTransience.integrable_bandTruncate line 117
  10. lemma OAI.DirectionalTransience.integral_bandTruncate_zero line 123
  11. lemma OAI.DirectionalTransience.integral_bandTruncate_cost line 132