OAI/Probability/Ballisticity/Estimates/LocalStoppedSplice.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.prod_dependent_map_const line 12
  2. abbrev OAI.DirectionalTransience.LocalUpperField line 39
  3. def OAI.DirectionalTransience.localStoppedField line 41
  4. lemma OAI.DirectionalTransience.localStoppedField_measurable line 46
  5. lemma OAI.DirectionalTransience.localStoppedField_full_graft line 60
  6. theorem OAI.DirectionalTransience.localStoppedField_law line 76
  7. abbrev OAI.DirectionalTransience.ReferenceClasses.Offsets line 117
  8. structure OAI.DirectionalTransience.ReferenceClasses.Consistent line 119
  9. abbrev OAI.DirectionalTransience.ReferenceClasses.Data line 125
  10. def OAI.DirectionalTransience.ReferenceClasses.related line 127
  11. lemma OAI.DirectionalTransience.ReferenceClasses.related_self line 129
  12. lemma OAI.DirectionalTransience.ReferenceClasses.related_symm line 130
  13. lemma OAI.DirectionalTransience.ReferenceClasses.related_trans line 133
  14. def OAI.DirectionalTransience.ReferenceClasses.representative line 139
  15. lemma OAI.DirectionalTransience.ReferenceClasses.representative_related line 142
  16. lemma OAI.DirectionalTransience.ReferenceClasses.representative_le line 147
  17. lemma OAI.DirectionalTransience.ReferenceClasses.representative_eq_iff line 152
  18. def OAI.DirectionalTransience.ReferenceClasses.displacement line 162
  19. lemma OAI.DirectionalTransience.ReferenceClasses.displacement_spec line 165
  20. lemma OAI.DirectionalTransience.ReferenceClasses.offset_eq line 169
  21. def OAI.DirectionalTransience.ReferenceClasses.inputSite line 177
  22. lemma OAI.DirectionalTransience.ReferenceClasses.inputSite_eq_iff line 180
  23. lemma OAI.DirectionalTransience.ReferenceClasses.measurable_offset line 212
  24. lemma OAI.DirectionalTransience.ReferenceClasses.measurable_related line 216
  25. lemma OAI.DirectionalTransience.ReferenceClasses.measurable_representative line 221
  26. lemma OAI.DirectionalTransience.ReferenceClasses.measurable_displacement line 226
  27. lemma OAI.DirectionalTransience.ReferenceClasses.measurable_inputSite line 241
  28. abbrev OAI.DirectionalTransience.ReferenceClasses.Site line 247
  29. abbrev OAI.DirectionalTransience.ReferenceClasses.UpperField line 248
  30. abbrev OAI.DirectionalTransience.ReferenceClasses.AllFields line 249
  31. def OAI.DirectionalTransience.ReferenceClasses.fields line 251
  32. lemma OAI.DirectionalTransience.ReferenceClasses.measurable_fields line 254
  33. def OAI.DirectionalTransience.ReferenceClasses.reference line 261
  34. instance OAI.DirectionalTransience.ReferenceClasses.reference_markov line 267
  35. lemma OAI.DirectionalTransience.ReferenceClasses.reference_apply line 271
  36. lemma OAI.DirectionalTransience.ReferenceClasses.inputSite_injective_at_label line 279
  37. lemma OAI.DirectionalTransience.ReferenceClasses.reference_single_field line 286
  38. lemma OAI.DirectionalTransience.ReferenceClasses.inputSite_injective_distinct_classes line 296
  39. lemma OAI.DirectionalTransience.ReferenceClasses.reference_distinct_classes line 307