OAI/Probability/InvariantIsing/Fields/ZeroFieldPopulations.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Vanishing field populations can be relabeled into a positive population.

  1. lemma OAI.InvariantIsing.spectralLabelCount_eq_spinGroupSize line 12
  2. def OAI.InvariantIsing.positiveFieldProjection line 19
  3. lemma OAI.InvariantIsing.positiveFieldProjection_weight line 22
  4. lemma OAI.InvariantIsing.positiveFieldProjection_counts line 36
  5. lemma OAI.InvariantIsing.physical_mean_zero_field_populations line 45