OAI/Probability/InvariantIsing/Arrays/MonomialEnumeration.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A concrete complete enumeration of the spectral/tree monomials with linear degree cap.

  1. def OAI.InvariantIsing.multidegreeDecode line 13
  2. def OAI.InvariantIsing.multidegreeEncode line 17
  3. lemma OAI.InvariantIsing.multidegreeDecode_encode line 21
  4. lemma OAI.InvariantIsing.multidegreeDecode_sum_le line 33
  5. def OAI.InvariantIsing.enumeratedSpectralDegree line 44

    Source documentation

    First m coordinates are spectral degrees; the final coordinate is the tree degree. The constant kernel can be retained harmlessly.

    def enumeratedSpectralDegree (m j : ℕ) (a : Fin m) : ℕ :=
…
  6. def OAI.InvariantIsing.enumeratedTreeDegree line 47
  7. lemma OAI.InvariantIsing.enumeratedMonomial_degree_le line 50
  8. lemma OAI.InvariantIsing.enumeratedSpectralDegree_real_sum_le line 55
  9. theorem OAI.InvariantIsing.enumeratedMonomial_surjective line 63

    Source documentation

    Every nonconstant joint spectral/tree monomial occurs at a fixed finite index, hence eventually occurs in the truncation through N.

    theorem enumeratedMonomial_surjective (m : ℕ) (d : Fin m → ℕ) (r : ℕ)
    (h : 1 ≤ (∑ a, d a) + r) :
    ∃ j, (∀ a, enumeratedSpectralDegree m j a = d a) ∧ enumeratedTreeDegree m j = r := by
…

    Mentions: OAI.InvariantIsing.enumeratedSpectralDegree, OAI.InvariantIsing.enumeratedTreeDegree