OAI/Probability/Ballisticity/Estimates/Dust.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalTransience.CurrentData line 13
  2. def OAI.DirectionalTransience.currentDust line 15
  3. lemma OAI.DirectionalTransience.currentDust_measurable line 17
  4. def OAI.DirectionalTransience.currentDustFrequency line 21
  5. lemma OAI.DirectionalTransience.currentDustFrequency_measurable line 24
  6. def OAI.DirectionalTransience.currentDustWeight line 32
  7. lemma OAI.DirectionalTransience.currentDustWeight_measurable line 35
  8. def OAI.DirectionalTransience.upperNoDropMean line 45
  9. lemma OAI.DirectionalTransience.upperNoDrop_toReal_bound line 48
  10. lemma OAI.DirectionalTransience.upperNoDropMean_pos line 53
  11. lemma OAI.DirectionalTransience.current_reference_dust_law line 67
  12. lemma OAI.DirectionalTransience.reference_ae_fields line 83
  13. lemma OAI.DirectionalTransience.current_reference_nodrop_le line 94
  14. lemma OAI.DirectionalTransience.average_zero_of_survival line 125
  15. lemma OAI.DirectionalTransience.symmetric_indicator_zero_of_average line 144