OAI/Probability/Ballisticity/Estimates/RawPairEndpoint.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.prefixEndpoint line 14
  2. lemma OAI.DirectionalTransience.measurable_prefixEndpoint line 18
  3. def OAI.DirectionalTransience.PairEndpointEvent line 23
  4. lemma OAI.DirectionalTransience.measurableSet_pairEndpointEvent line 29
  5. def OAI.DirectionalTransience.rawPairEndpointMass line 38
  6. lemma OAI.DirectionalTransience.signedCoordinate_sub_add line 43
  7. lemma OAI.DirectionalTransience.tubePrefix_endpoint_bound line 49
  8. lemma OAI.DirectionalTransience.endpointPrefix_endpoint_ae line 59
  9. lemma OAI.DirectionalTransience.quenched_pair_regular line 73
  10. lemma OAI.DirectionalTransience.central_pair_mass_le line 80
  11. lemma OAI.DirectionalTransience.jump_central_pair_mass_le line 102
  12. lemma OAI.DirectionalTransience.integral_lower_from_fraction line 154
  13. def OAI.DirectionalTransience.pairCentralRetainedMass line 175
  14. def OAI.DirectionalTransience.pairJumpRetainedMass line 178
  15. lemma OAI.DirectionalTransience.centralPrefixMass_bounds line 183
  16. lemma OAI.DirectionalTransience.jumpPrefixMass_bounds line 187
  17. lemma OAI.DirectionalTransience.pair_retained_mass_of_favorable_fraction line 191