OAI/Probability/Ballisticity/Coupling/SeedMedian.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.IsIntegerMedian line 12
  2. lemma OAI.DirectionalTransience.exists_nat_integerMedian line 15
  3. def OAI.DirectionalTransience.selectedIntegerMedian line 22
  4. lemma OAI.DirectionalTransience.selectedIntegerMedian_spec line 25
  5. lemma OAI.DirectionalTransience.measurable_selectedIntegerMedian line 29
  6. def OAI.DirectionalTransience.orientedIntegerLaw line 38
  7. lemma OAI.DirectionalTransience.measurable_orientedIntegerLaw line 44
  8. def OAI.DirectionalTransience.seedMedian line 48
  9. lemma OAI.DirectionalTransience.measurable_seedMedian line 51
  10. def OAI.DirectionalTransience.seedHalfRaw line 54
  11. lemma OAI.DirectionalTransience.seedHalfRaw_mass line 59
  12. lemma OAI.DirectionalTransience.measurable_seedHalfRaw line 72
  13. instance OAI.DirectionalTransience.seedHalfRaw_finite line 85
  14. def OAI.DirectionalTransience.seedHalf line 89
  15. lemma OAI.DirectionalTransience.measurable_seedHalf line 93
  16. lemma OAI.DirectionalTransience.seedHalf_domination line 97
  17. lemma OAI.DirectionalTransience.seedHalf_ae line 111
  18. lemma OAI.DirectionalTransience.seedHalf_inherits line 123
  19. def OAI.DirectionalTransience.seedEndpointRaw line 139
  20. lemma OAI.DirectionalTransience.seedEndpointRaw_apply line 143
  21. lemma OAI.DirectionalTransience.seedEndpointRaw_le line 150
  22. lemma OAI.DirectionalTransience.seedEndpointRaw_univ_le line 157
  23. instance OAI.DirectionalTransience.seedEndpointRaw_finite line 169
  24. lemma OAI.DirectionalTransience.seedEndpointRaw_mono line 174
  25. lemma OAI.DirectionalTransience.seedEndpointRaw_smul line 181
  26. lemma OAI.DirectionalTransience.seedEndpointRaw_comp_le line 186
  27. lemma OAI.DirectionalTransience.seedEndpointRaw_ae line 205
  28. lemma OAI.DirectionalTransience.seedEndpointRaw_supported line 214
  29. lemma OAI.DirectionalTransience.measurable_seedEndpointRaw line 223
  30. lemma OAI.DirectionalTransience.seedEndpointRaw_joint_rows line 235
  31. lemma OAI.DirectionalTransience.seedEndpointRaw_jump_total line 260
  32. lemma OAI.DirectionalTransience.tube_le_seedCentral line 275