OAI/Probability/InvariantIsing/Spectral/SpectralPartition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Total spin overlap and self normalization for a genuine spectral partition.

  1. lemma OAI.InvariantIsing.projectedOverlap_partition line 14
  2. lemma OAI.InvariantIsing.projectedOverlap_partition_self line 28
  3. def OAI.InvariantIsing.spectralSpinArray line 38
  4. lemma OAI.InvariantIsing.continuous_spectralSpinArray line 41
  5. def OAI.InvariantIsing.SpectralPartitionGeometry line 45
  6. lemma OAI.InvariantIsing.isClosed_spectralPartitionGeometry line 48
  7. lemma OAI.InvariantIsing.spectralReplicaArray_partition line 60
  8. lemma OAI.InvariantIsing.spectralArrayLaw_partition line 78
  9. lemma OAI.InvariantIsing.spectralArray_limit_partition line 93
  10. lemma OAI.InvariantIsing.tensorPerturbedArrayLaw_partition line 100
  11. lemma OAI.InvariantIsing.spectralPartition_diagonal_sum line 111
  12. lemma OAI.InvariantIsing.spectralPartition_spin_unit line 119
  13. def OAI.InvariantIsing.spectralSpinWeight line 126
  14. lemma OAI.InvariantIsing.spectralSpinWeight_nonneg line 128
  15. lemma OAI.InvariantIsing.spectralLinearArray_spinWeight line 131
  16. lemma OAI.InvariantIsing.spectralLinearArray_single line 138