OAI/Probability/Ballisticity/Estimates/IndependentRecenterMap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.independent_recenter_map line 281
2. lemma OAI.DirectionalTransience.independent_physicalGap_integral line 299
3. lemma OAI.DirectionalTransience.clippedAbsThreeHalves_neg line 313
4. lemma OAI.DirectionalTransience.independent_physicalGap_clipped line 316
5. lemma OAI.DirectionalTransience.prefixVariation_le_one line 360
6. theorem OAI.DirectionalTransience.shared_observed_clipped_drift_gaussian line 379