OAI/Probability/InvariantIsing/Spectral/CompactSpectralPartition.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite positive-mass spectral partitions for the compact-support approximation.

  1. def OAI.InvariantIsing.spectralBallWeight line 14
  2. def OAI.InvariantIsing.spectralBallValue line 18
  3. structure OAI.InvariantIsing.CompactSpectralPartition line 21
  4. theorem OAI.InvariantIsing.exists_compact_spectral_partition line 36
  5. def OAI.InvariantIsing.CompactSpectralPartition.cells line 62
  6. def OAI.InvariantIsing.CompactSpectralPartition.weight line 65
  7. def OAI.InvariantIsing.CompactSpectralPartition.value line 67
  8. abbrev OAI.InvariantIsing.CompactSpectralPartition.Positive line 69
  9. lemma OAI.InvariantIsing.CompactSpectralPartition.weight_sum line 71
  10. def OAI.InvariantIsing.CompactSpectralPartition.law line 76
  11. def OAI.InvariantIsing.CompactSpectralPartition.edge line 80
  12. lemma OAI.InvariantIsing.CompactSpectralPartition.value_mem line 82
  13. lemma OAI.InvariantIsing.CompactSpectralPartition.residual_zero line 87
  14. lemma OAI.InvariantIsing.CompactSpectralPartition.law_eq_map line 91
  15. lemma OAI.InvariantIsing.CompactSpectralPartition.quantizer_close line 99
  16. lemma OAI.InvariantIsing.CompactSpectralPartition.endpoint_bounds line 104
  17. lemma OAI.InvariantIsing.CompactSpectralPartition.law_support line 109