OAI/Probability/InvariantIsing/Haar/HaarPolynomialSpace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite polynomial spaces, padded by the constant atom, for the rotation semigroup.

  1. def OAI.InvariantIsing.haarPolynomialAtom line 11
  2. def OAI.InvariantIsing.haarPolynomialWord line 15
  3. def OAI.InvariantIsing.haarPolynomialSpace line 18
  4. instance OAI.InvariantIsing.haarPolynomialSpace_finite line 21
  5. lemma OAI.InvariantIsing.haarPolynomialWord_mem line 24
  6. lemma OAI.InvariantIsing.haarPolynomialWord_cons line 28
  7. lemma OAI.InvariantIsing.haarPolynomialSpace_atom_mul line 33
  8. lemma OAI.InvariantIsing.haarPolynomialSpace_le_succ line 50
  9. lemma OAI.InvariantIsing.haarPolynomialSpace_mono line 56
  10. lemma OAI.InvariantIsing.one_mem_haarPolynomialSpace line 59
  11. theorem OAI.InvariantIsing.exists_mem_haarPolynomialSpace line 65

    Source documentation

    Every multivariate polynomial belongs to one of the finite spaces.

    theorem exists_mem_haarPolynomialSpace {N : ℕ} (p : MatrixPolynomial N) :
    ∃ d : ℕ, p ∈ haarPolynomialSpace N d := by
…

    Mentions: OAI.InvariantIsing.MatrixPolynomial, OAI.InvariantIsing.haarPolynomialSpace