OAI/Probability/Ballisticity/Geometry/OccupationWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.typedCurrentArrayWindow_iterate_actual line 13
2. lemma OAI.DirectionalTransience.rawCurrentOccupation_actual line 28
3. lemma OAI.DirectionalTransience.Entropy.normalize_map_measure line 55
4. lemma OAI.DirectionalTransience.Entropy.normalize_maps_equal line 73
5. lemma OAI.DirectionalTransience.Entropy.real_mass_eq_of_maps_equal line 84