OAI/Probability/SKRatio/Calculus/GibbsMeanCLM.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Calculus.gibbsMeanCLM line 14
2. lemma OAI.SKRatio.Calculus.gibbsMeanCLM_apply line 17
3. lemma OAI.SKRatio.Calculus.gibbsMean_generator line 21
4. lemma OAI.SKRatio.Calculus.functional_exp_invariant line 30
5. theorem OAI.SKRatio.Calculus.gibbsMean_semigroup line 45
6. theorem OAI.SKRatio.Calculus.continuousKernel_stationary line 56
7. def OAI.SKRatio.Calculus.continuousDistance line 63
8. lemma OAI.SKRatio.Calculus.continuousKernel_stochastic line 67
9. lemma OAI.SKRatio.Calculus.tv_le_continuousDistance line 72
10. lemma OAI.SKRatio.Calculus.continuousDistance_nonneg line 79
11. lemma OAI.SKRatio.Calculus.continuousDistance_le_one line 83
12. lemma OAI.SKRatio.Calculus.continuousDistance_antitone line 90
13. theorem OAI.SKRatio.Calculus.continuousDistance_smoothing line 107
14. lemma OAI.SKRatio.Calculus.gradientWeight_le_two line 137
15. lemma OAI.SKRatio.Calculus.weightedGradient_nonneg line 144
16. lemma OAI.SKRatio.Calculus.weightedGradient_le line 148
17. lemma OAI.SKRatio.Calculus.halfDiff_abs_le line 154
18. lemma OAI.SKRatio.Calculus.unweightedGradient_le_dim line 162
19. lemma OAI.SKRatio.Calculus.continuous_halfDiff line 171
20. lemma OAI.SKRatio.Calculus.continuous_weightedGradient line 175
21. def OAI.SKRatio.Calculus.backwardEnergy line 182
22. lemma OAI.SKRatio.Calculus.backwardEnergy_continuous line 186
23. lemma OAI.SKRatio.Calculus.backwardEnergy_nonneg line 192
24. lemma OAI.SKRatio.Calculus.backward_second_moment_hasDerivAt line 196
25. theorem OAI.SKRatio.Calculus.backward_variance_budget line 226
26. theorem OAI.SKRatio.Calculus.backward_energy_budget line 241