OAI/Probability/Ballisticity/Estimates/RawPairRetention.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.rawPairMixture line 15
  2. lemma OAI.DirectionalTransience.rawPairMixture_apply line 19
  3. lemma OAI.DirectionalTransience.rawPairMixture_le_one line 24
  4. def OAI.DirectionalTransience.retainedPairLaw line 33
  5. lemma OAI.DirectionalTransience.retainedPairLaw_mass line 38
  6. lemma OAI.DirectionalTransience.retainedPairLaw_le line 44
  7. lemma OAI.DirectionalTransience.retainedPairLaw_support line 48
  8. lemma OAI.DirectionalTransience.rawPairMixture_joint_rows line 53
  9. lemma OAI.DirectionalTransience.retainedPairLaw_joint_rows line 79
  10. lemma OAI.DirectionalTransience.measurable_normalizedMeasure line 101
  11. lemma OAI.DirectionalTransience.normalizedMeasure_absolutelyContinuous line 108
  12. lemma OAI.DirectionalTransience.normalized_retainedPair_probability line 113
  13. lemma OAI.DirectionalTransience.normalized_retainedPair_support line 123
  14. lemma OAI.DirectionalTransience.normalized_retainedPair_joint_rows line 128
  15. def OAI.DirectionalTransience.BufferStageEvent line 145
  16. lemma OAI.DirectionalTransience.bufferStageEvent_iff line 150
  17. lemma OAI.DirectionalTransience.strip_mono_nat_height line 166
  18. lemma OAI.DirectionalTransience.measurableSet_bufferStageEvent_rows line 172