OAI/Probability/InvariantIsing/Spectral/SpectralBallQuantizer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual finite quantizer attached to the null-boundary ball cover.

  1. def OAI.InvariantIsing.spectralBallQuantizer line 13
  2. lemma OAI.InvariantIsing.measurable_spectralBallQuantizer line 17
  3. lemma OAI.InvariantIsing.spectralBallQuantizer_close line 24
  4. lemma OAI.InvariantIsing.spectralBallQuantizer_mem line 44