OAI/Probability/Ballisticity/Model.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DirectionalTransience.Lattice line 10

   Also declared: ComparatorChallenges/DirectionalBallisticity.lean:10 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:10 (same declaration text).

2. abbrev OAI.DirectionalTransience.Direction line 11

   Also declared: ComparatorChallenges/DirectionalBallisticity.lean:11 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:11 (same declaration text).

3. abbrev OAI.DirectionalTransience.Vector line 12

   Also declared: ComparatorChallenges/DirectionalBallisticity.lean:12 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:12 (same declaration text).

4. abbrev OAI.DirectionalTransience.Row line 13

   Also declared: ComparatorChallenges/DirectionalBallisticity.lean:13 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:13 (same declaration text).

5. abbrev OAI.DirectionalTransience.Environment line 14

   Also declared: ComparatorChallenges/DirectionalBallisticity.lean:14 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:14 (same declaration text).

6. abbrev OAI.DirectionalTransience.State line 15

   Also declared: ComparatorChallenges/DirectionalBallisticity.lean:15 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:15 (same declaration text).

7. abbrev OAI.DirectionalTransience.Path line 16

   Also declared: ComparatorChallenges/DirectionalBallisticity.lean:16 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:16 (same declaration text).

8. def OAI.DirectionalTransience.step line 18

   Also declared: ComparatorChallenges/DirectionalBallisticity.lean:18 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:18 (same declaration text).

9. def OAI.DirectionalTransience.environmentLaw line 21

   Also declared: ComparatorChallenges/DirectionalBallisticity.lean:21 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:21 (same declaration text).

10. def OAI.DirectionalTransience.UniformElliptic line 24

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:24 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:24 (same declaration text).

11. lemma OAI.DirectionalTransience.measurable_current_row line 27

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:27 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:27 (same declaration text).

12. def OAI.DirectionalTransience.transition line 33

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:33 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:33 (same declaration text).

13. instance OAI.DirectionalTransience.transition_markov line 49

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:49 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:49 (same declaration text).

14. def OAI.DirectionalTransience.historyTransition line 59

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:59 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:59 (same declaration text).

15. instance OAI.DirectionalTransience.historyTransition_markov line 64

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:64 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:64 (same declaration text).

16. def OAI.DirectionalTransience.initialLaw line 68

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:68 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:68 (same declaration text).

17. def OAI.DirectionalTransience.annealedLaw line 71

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:71 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:71 (same declaration text).

18. def OAI.DirectionalTransience.dot line 75

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:75 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:75 (same declaration text).

19. def OAI.DirectionalTransience.realPosition line 77

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:77 (same declaration text), ComparatorChallenges/VelocityHemisphere.lean:77 (same declaration text).

20. def OAI.DirectionalTransience.DirectionallyTransient line 79

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:79 (same declaration text).

21. def OAI.DirectionalTransience.HasVelocity line 83

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:83 (same declaration text).

22. def OAI.DirectionalTransience.MainStatement line 89

    Also declared: ComparatorChallenges/DirectionalBallisticity.lean:89 (same declaration text).