OAI/Probability/Ballisticity/Walk/StateTrajectory.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.DirectionalTransience.environmentLaw_probability line 15
  2. instance OAI.DirectionalTransience.initialLaw_probability line 20
  3. instance OAI.DirectionalTransience.annealedLaw_probability line 25
  4. lemma OAI.DirectionalTransience.environment_site_law line 30
  5. lemma OAI.DirectionalTransience.environment_uniform_elliptic line 35
  6. lemma OAI.DirectionalTransience.row_entry_le_one line 42
  7. lemma OAI.DirectionalTransience.hasVelocity_unique line 47
  8. def OAI.DirectionalTransience.stateTrajectory line 52
  9. instance OAI.DirectionalTransience.stateTrajectory_markov line 56
  10. def OAI.DirectionalTransience.quenchedKernel line 60
  11. instance OAI.DirectionalTransience.quenchedKernel_markov line 63
  12. lemma OAI.DirectionalTransience.stateTrajectory_eq line 67
  13. lemma OAI.DirectionalTransience.annealed_eq_quenched_mixture line 74
  14. lemma OAI.DirectionalTransience.annealed_apply line 80
  15. lemma OAI.DirectionalTransience.environment_translation line 88
  16. lemma OAI.DirectionalTransience.stateTrajectory_initial line 94
  17. lemma OAI.DirectionalTransience.quenched_initial line 108
  18. lemma OAI.DirectionalTransience.quenched_initial_ae line 117
  19. instance OAI.DirectionalTransience.state_measurableEq line 125
  20. instance OAI.DirectionalTransience.state_measurableSingleton line 134
  21. def OAI.DirectionalTransience.AdmissibleStep line 137
  22. lemma OAI.DirectionalTransience.measurableSet_admissibleStep line 140
  23. lemma OAI.DirectionalTransience.transition_admissible line 150
  24. lemma OAI.DirectionalTransience.stateTrajectory_admissible line 161
  25. lemma OAI.DirectionalTransience.stateTrajectory_environment line 179
  26. lemma OAI.DirectionalTransience.quenched_nearest_neighbor line 195
  27. lemma OAI.DirectionalTransience.step_injective line 210
  28. lemma OAI.DirectionalTransience.transition_singleton_step line 220
  29. def OAI.DirectionalTransience.stateCylinder line 236
  30. lemma OAI.DirectionalTransience.measurableSet_stateCylinder line 239
  31. lemma OAI.DirectionalTransience.stateCylinder_eq_preimage line 246
  32. lemma OAI.DirectionalTransience.stateTrajectory_cylinder_succ line 257
  33. lemma OAI.DirectionalTransience.stateTrajectory_cylinder line 287
  34. abbrev OAI.DirectionalTransience.rowSigma line 302
  35. lemma OAI.DirectionalTransience.rowSigma_le line 305
  36. lemma OAI.DirectionalTransience.measurable_row_on line 308
  37. lemma OAI.DirectionalTransience.environment_indep_rows line 313
  38. lemma OAI.DirectionalTransience.rowSigma_mono line 320
  39. lemma OAI.DirectionalTransience.environment_tail_zero_one line 324