OAI/Probability/SKGap/Brownian/IndependentPathTail.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.PathBridge.pathEnergy line 13
2. lemma OAI.SKGap.PathBridge.energy_exponential_prod line 15
3. lemma OAI.SKGap.PathBridge.pathEnergy_exponential_integrable line 19
4. lemma OAI.SKGap.PathBridge.pathEnergy_exponential_integral line 25
5. theorem OAI.SKGap.PathBridge.pathEnergy_dimension_tail line 32
6. theorem OAI.SKGap.PathBridge.scaledPath_dimension_tail line 60
7. def OAI.SKGap.PathBridge.brownianUnitLaw line 87
8. lemma OAI.SKGap.PathBridge.brownianUnitLaw_probability line 91
9. theorem OAI.SKGap.PathBridge.brownianUnitLaw_eq line 97
10. theorem OAI.SKGap.PathBridge.brownian_normalized_increment_tail line 154