OAI/Probability/SKRatio/Matrices/PathEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.PathBridge.pathEnergy line 13
2. lemma OAI.SKRatioGaussian.PathBridge.energy_exponential_prod line 15
3. lemma OAI.SKRatioGaussian.PathBridge.pathEnergy_exponential_integrable line 19
4. lemma OAI.SKRatioGaussian.PathBridge.pathEnergy_exponential_integral line 25
5. theorem OAI.SKRatioGaussian.PathBridge.pathEnergy_dimension_tail line 32
6. theorem OAI.SKRatioGaussian.PathBridge.scaledPath_dimension_tail line 60