OAI/Probability/SKGap/Localization/ScalarEigenfunction.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGapCutoff.spectral_parseval line 11
  2. lemma OAI.SKGapCutoff.spectral_generator_coordinates line 20
  3. lemma OAI.SKGapCutoff.spinEigenvalues_nonneg line 30
  4. lemma OAI.SKGapCutoff.sum_spinSpectralCoefficient_sq line 41
  5. lemma OAI.SKGapCutoff.spinSpectralMass_nonneg line 48
  6. lemma OAI.SKGapCutoff.sum_spinSpectralMass line 53
  7. theorem OAI.SKGapCutoff.spinSpectralMeasure_probability line 62
  8. lemma OAI.SKGapCutoff.spinSpectralMeasure_integral line 71
  9. lemma OAI.SKGapCutoff.spinSpectralMeasure_integral_trace line 82
  10. lemma OAI.SKGapCutoff.spin_first_moment_sum line 91
  11. lemma OAI.SKGapCutoff.spin_second_moment_sum line 106
  12. theorem OAI.SKGapCutoff.spinSpectralMeasure_moments line 123
  13. def OAI.SKGapCutoff.scalarEigenfunction line 135
  14. lemma OAI.SKGapCutoff.lift_scalarEigenfunction line 140
  15. lemma OAI.SKGapCutoff.generator_scalarEigenfunction line 146
  16. lemma OAI.SKGapCutoff.semigroup_scalarEigenfunction line 161
  17. lemma OAI.SKGapCutoff.spectral_coordinates_inner line 171
  18. lemma OAI.SKGapCutoff.spectral_semigroup_coordinates line 179
  19. theorem OAI.SKGapCutoff.spinSpectralMeasure_correlation line 190
  20. lemma OAI.SKGapCutoff.replace_eq_of_halfDiff_zero line 205
  21. lemma OAI.SKGapCutoff.constant_of_halfDiff_zero line 215
  22. lemma OAI.SKGapCutoff.halfDiff_zero_of_dirichlet_zero line 231
  23. lemma OAI.SKGapCutoff.constant_of_generator_zero line 245
  24. lemma OAI.SKGapCutoff.spinSpectralCoefficient_zero_eigenvalue line 253
  25. theorem OAI.SKGapCutoff.spinSpectralMeasure_nonpositive line 268