OAI/Probability/SKRatio/Calculus/Energy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Calculus.energy_early_late_averaging line 12
2. theorem OAI.SKRatio.Calculus.transient_variance_of_energy_comparison line 47
3. def OAI.SKRatio.Calculus.stationaryEnergy line 64
4. lemma OAI.SKRatio.Calculus.stationaryEnergy_nonneg line 67
5. lemma OAI.SKRatio.Calculus.stationaryEnergy_eq line 72
6. lemma OAI.SKRatio.Calculus.equilibrium_variance_hasDerivAt line 89
7. theorem OAI.SKRatio.Calculus.equilibrium_variance_decay line 116
8. lemma OAI.SKRatio.Calculus.equilibrium_variance_le_one line 147
9. theorem OAI.SKRatio.Calculus.equilibrium_smoothing line 158
10. theorem OAI.SKRatio.Calculus.smoothing_of_energy_comparison line 167