OAI/Probability/Ballisticity/Estimates/GaussianAbsTail.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.gaussian_abs_tail line 129
2. lemma OAI.DirectionalTransience.distribution_closed_limsup line 148
3. lemma OAI.DirectionalTransience.distribution_abs_limsup line 161
4. lemma OAI.DirectionalTransience.recordFluctuationScale_pos line 181
5. def OAI.DirectionalTransience.scaledRecordEndpoint line 193
6. lemma OAI.DirectionalTransience.measurable_scaledRecordEndpoint line 197
7. theorem OAI.DirectionalTransience.shared_endpoint_limits line 203