OAI/Probability/SKGap/Localization/JumpBilinear.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.jumpWeight_conditional_first line 170
2. lemma OAI.SKGapCutoff.jumpWeight_conditional_square line 189
3. theorem OAI.SKGapCutoff.jumpWeight_isometry line 208
4. lemma OAI.SKGapCutoff.exact_gradient_jumpWeight_isometry line 221
5. def OAI.SKGapCutoff.jumpBilinear line 229
6. lemma OAI.SKGapCutoff.backward_product_hasDerivAt line 232
7. lemma OAI.SKGapCutoff.interpolated_product_hasDerivAt line 245
8. lemma OAI.SKGapCutoff.jumpBilinear_continuous line 264
9. lemma OAI.SKGapCutoff.interpolated_bilinear_continuous line 269
10. theorem OAI.SKGapCutoff.semigroup_covariance_integral line 280
11. lemma OAI.SKGapCutoff.equilibriumPotential_pairing_covariance line 291
12. lemma OAI.SKGapCutoff.semigroup_covariance_zero_hasDerivAt line 322
13. lemma OAI.SKGapCutoff.semigroup_covariance_slope line 337
14. lemma OAI.SKGapCutoff.stationaryInner_covariance_slope line 343
15. theorem OAI.SKGapCutoff.equilibriumPotential_pairing_small_time line 352
16. lemma OAI.SKGapCutoff.exact_gradient_pairing_integral line 385
17. lemma OAI.SKGapCutoff.stationaryInner_centered_semigroup_tendsto_zero line 412
18. theorem OAI.SKGapCutoff.exact_gradient_pairing_integral_tendsto line 434
19. lemma OAI.SKGapCutoff.centered_semigroup_gap_variance line 444
20. lemma OAI.SKGapCutoff.stationaryInner_cauchy_sq line 467
21. lemma OAI.SKGapCutoff.gibbsVariance_nonneg line 472
22. theorem OAI.SKGapCutoff.exact_gradient_pairing_uniform_tail line 476