OAI/Probability/SKGap/Localization/Centered.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.centered line 10
2. lemma OAI.SKGapCutoff.gibbsExpectation_centered line 13
3. lemma OAI.SKGapCutoff.halfDiff_centered line 18
4. lemma OAI.SKGapCutoff.dirichlet_centered line 23
5. lemma OAI.SKGapCutoff.centered_variance line 27
6. lemma OAI.SKGapCutoff.spectral_dirichlet line 31
7. lemma OAI.SKGapCutoff.centered_spectral_coordinate_zero line 43
8. lemma OAI.SKGapCutoff.hasGap_of_positive_eigenvalues line 56
9. theorem OAI.SKGapCutoff.finite_gap_pos line 73
10. lemma OAI.SKGapCutoff.scalarEigenfunction_centered line 92
11. lemma OAI.SKGapCutoff.scalarEigenfunction_inner_self line 103
12. lemma OAI.SKGapCutoff.gap_le_positive_eigenvalue line 111
13. theorem OAI.SKGapCutoff.hasGap_iff_positive_eigenvalues line 130
14. theorem OAI.SKGapCutoff.quenchedGap_iff_spectral line 137