OAI/Probability/Ballisticity/Estimates/SuccessfulAverage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.measurable_crossingQuenched line 184
  2. lemma OAI.DirectionalTransience.quenched_noDrop_subset_cross_ae line 189
  3. def OAI.DirectionalTransience.successfulAverage line 197
  4. lemma OAI.DirectionalTransience.successfulAverage_apply line 201
  5. lemma OAI.DirectionalTransience.successfulAverage_probability line 210
  6. lemma OAI.DirectionalTransience.raw_crossingDensity_le_successful line 227
  7. lemma OAI.DirectionalTransience.raw_crossingDensity_le_conditioned line 242
  8. lemma OAI.DirectionalTransience.raw_crossingDensity_mass_tendsto line 254
  9. theorem OAI.DirectionalTransience.successfulAverage_comparison line 280