OAI/Probability/SKGap/Localization/LinearObservable.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.stationary_deviation_le_oscillation line 16
2. lemma OAI.SKGapCutoff.semigroup_deviation_le_gradient line 22
3. theorem OAI.SKGapCutoff.continuous_tv_le_gradient line 32
4. lemma OAI.SKGapCutoff.worstContinuous_le_gradient line 56
5. def OAI.SKGapCutoff.linearObservable line 64
6. lemma OAI.SKGapCutoff.halfDiff_linearObservable line 67
7. lemma OAI.SKGapCutoff.linearObservable_centered line 77
8. lemma OAI.SKGapCutoff.dirichlet_linearObservable_le line 83
9. lemma OAI.SKGapCutoff.linearObservable_second_moment_le line 96
10. def OAI.SKGapCutoff.overlap line 111
11. lemma OAI.SKGapCutoff.overlap_coeff_norm_sq line 113
12. def OAI.SKGapCutoff.spinCorrelation line 115
13. lemma OAI.SKGapCutoff.overlap_correlates line 118
14. lemma OAI.SKGapCutoff.exists_overlap_mean_ge line 131
15. lemma OAI.SKGapCutoff.kernel_centered_second_moment line 140
16. theorem OAI.SKGapCutoff.worstContinuous_lower_from_spin line 150