OAI/Probability/InvariantIsing/Spectral/SpectralOverlapPaths.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The reconstructed finite-alphabet overlap paths in manuscript rot:full-paths. The formulas and their positivity and sum constraints are proved here; identification with limiting Gibbs overlaps is separate.

  1. def OAI.InvariantIsing.spectralPathDensity line 19
  2. def OAI.InvariantIsing.spectralGroupPath line 23
  3. def OAI.InvariantIsing.spectralGroupDiagonal line 27
  4. theorem OAI.InvariantIsing.spectralPathDensity_nonneg line 31
  5. theorem OAI.InvariantIsing.spectralPathDensity_continuousOn line 36
  6. theorem OAI.InvariantIsing.spectralPathDensity_intervalIntegrable line 42
  7. theorem OAI.InvariantIsing.spectralGroupPath_nonneg line 49
  8. theorem OAI.InvariantIsing.spectralGroupDiagonal_nonneg line 55
  9. theorem OAI.InvariantIsing.spectralGroupPath_monotone line 61
  10. theorem OAI.InvariantIsing.sum_spectralGroupPath line 69
  11. theorem OAI.InvariantIsing.sum_spectralGroupDiagonal line 79
  12. theorem OAI.InvariantIsing.spectralGroupPath_le_diagonal line 89
  13. theorem OAI.InvariantIsing.spectralGroup_diagonalExcess_nonneg line 96
  14. theorem OAI.InvariantIsing.spectralGroup_diagonalExcess_eq_integral line 101
  15. theorem OAI.InvariantIsing.spectralGroup_diagonalExcess_zero_of_top_one line 114
  16. theorem OAI.InvariantIsing.spectralGroupDiagonal_le_one line 120
  17. theorem OAI.InvariantIsing.spectralGroupPath_constant line 127
  18. theorem OAI.InvariantIsing.spectralGroupDiagonal_constant line 133