OAI/Probability/Ballisticity/Estimates/ReferenceContinuity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.ReferenceClasses.finite_value_clopen line 16
2. lemma OAI.DirectionalTransience.ReferenceClasses.offset_clopen line 22
3. lemma OAI.DirectionalTransience.ReferenceClasses.consistent_closed line 26
4. instance OAI.DirectionalTransience.ReferenceClasses.data_compact line 65
5. lemma OAI.DirectionalTransience.ReferenceClasses.map_iid_eq_of_same_fibers line 73
6. lemma OAI.DirectionalTransience.ReferenceClasses.reference_projection_eq line 104
7. lemma OAI.DirectionalTransience.ReferenceClasses.inputSite_collision_clopen line 118
8. lemma OAI.DirectionalTransience.ReferenceClasses.reference_projection_locally_constant line 129