OAI/Probability/Ballisticity/Estimates/ProperProfile.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.horizontalLayerEquiv line 13
  2. def OAI.DirectionalTransience.IsProperProfile line 19
  3. lemma OAI.DirectionalTransience.isProperProfile_measurable line 22
  4. abbrev OAI.DirectionalTransience.ProperProfile line 28
  5. def OAI.DirectionalTransience.properProfileKernel line 30
  6. lemma OAI.DirectionalTransience.properProfileKernel_apply line 37
  7. lemma OAI.DirectionalTransience.properProfileKernel_total line 47
  8. instance OAI.DirectionalTransience.properProfileKernel_finite line 52
  9. lemma OAI.DirectionalTransience.properProfileKernel_full line 55
  10. def OAI.DirectionalTransience.markedProfile line 61
  11. lemma OAI.DirectionalTransience.markedProfile_measurable line 64
  12. def OAI.DirectionalTransience.properData line 70
  13. lemma OAI.DirectionalTransience.properData_measurable line 73
  14. lemma OAI.DirectionalTransience.properData_eq line 83
  15. lemma OAI.DirectionalTransience.StationaryArrayLaw.marked_profile_proper line 90
  16. lemma OAI.DirectionalTransience.StationaryArrayLaw.properProfile_nonempty line 103
  17. def OAI.DirectionalTransience.fillUpper line 121
  18. lemma OAI.DirectionalTransience.fillUpper_measurable line 124
  19. lemma OAI.DirectionalTransience.fillUpper_eq line 127
  20. lemma OAI.DirectionalTransience.fillUpper_reference line 131
  21. lemma OAI.DirectionalTransience.fillUpper_joint_reference line 148
  22. lemma OAI.DirectionalTransience.fillUpper_finite_entropy line 170