OAI/Probability/InvariantIsing/Spectral/SpectralArrayGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Gram structure and replica symmetry for spectral arrays retaining common disorder.

  1. def OAI.InvariantIsing.permuteSpectralArray line 15
  2. lemma OAI.InvariantIsing.continuous_permuteSpectralArray line 18
  3. lemma OAI.InvariantIsing.disorderReplicaLaw_map_reindex line 23
  4. lemma OAI.InvariantIsing.spectralArrayLaw_map_reindex line 39
  5. lemma OAI.InvariantIsing.spectralArray_limit_reindex line 55
  6. lemma OAI.InvariantIsing.scalar_of_spectral_exchangeable line 70
  7. def OAI.InvariantIsing.spectralCoordinateArray line 84
  8. lemma OAI.InvariantIsing.continuous_spectralCoordinateArray line 87
  9. def OAI.InvariantIsing.SpectralGram line 92
  10. lemma OAI.InvariantIsing.isClosed_spectralGram line 95
  11. lemma OAI.InvariantIsing.spectralReplicaArray_gram line 101
  12. lemma OAI.InvariantIsing.spectralArrayLaw_gram line 111
  13. lemma OAI.InvariantIsing.spectralArray_limit_gram line 122