OAI/Probability/SKGap/Localization/StationaryInner.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.stationaryInner line 9
2. def OAI.SKGapCutoff.weightedInner line 11
3. def OAI.SKGapCutoff.equilibriumPotential line 13
4. def OAI.SKGapCutoff.expectationLM line 18
5. def OAI.SKGapCutoff.expectationCLM line 23
6. lemma OAI.SKGapCutoff.gibbsExpectation_const line 26
7. lemma OAI.SKGapCutoff.gibbsExpectation_sum line 30
8. lemma OAI.SKGapCutoff.gibbsExpectation_sub line 36
9. lemma OAI.SKGapCutoff.gibbsExpectation_mul_const line 40
10. def OAI.SKGapCutoff.stationaryPairingCLM line 44
11. lemma OAI.SKGapCutoff.expectationCLM_apply line 52
12. lemma OAI.SKGapCutoff.stationaryPairingCLM_apply line 55
13. lemma OAI.SKGapCutoff.stationaryInner_symm line 58
14. lemma OAI.SKGapCutoff.dirichlet_symm line 62
15. lemma OAI.SKGapCutoff.scalar_generator_symmetric line 71
16. lemma OAI.SKGapCutoff.stationaryInner_pow_symm line 82
17. lemma OAI.SKGapCutoff.stationaryInner_exp_symm line 96
18. theorem OAI.SKGapCutoff.scalar_semigroup_symmetric line 113
19. lemma OAI.SKGapCutoff.gibbsExpectation_semigroup line 124
20. theorem OAI.SKGapCutoff.equilibriumPotential_centered line 135
21. lemma OAI.SKGapCutoff.exact_gradient_semigroup_identity line 147