OAI/Analysis/MutuallyUnbiased/Cubic/CubicSymmetric.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Elementary symmetric sums for the six-entry cubic classification.

  1. def OAI.MUB6.elementarySum line 18
  2. theorem OAI.MUB6.unit_product_complement line 21
  3. theorem OAI.MUB6.elementarySum_reciprocal line 32
  4. theorem OAI.MUB6.elementarySum_zero line 52
  5. theorem OAI.MUB6.elementarySum_six line 55
  6. theorem OAI.MUB6.elementarySum_one line 60
  7. theorem OAI.MUB6.coordinate_pairs line 63
  8. theorem OAI.MUB6.elementarySum_two_identity line 71

    Source documentation

    Newton's identity at degree two, specialized to exactly six entries.

    theorem elementarySum_two_identity (v : (Fin 6) → ℂ) :
    (∑ i, v i) ^ 2 = (∑ i, v i ^ 2) + 2 * elementarySum v 2 := by
…

    Mentions: OAI.MUB6.elementarySum

  9. theorem OAI.MUB6.elementarySum_one_two_zero line 76
  10. theorem OAI.MUB6.elementarySum_four_five_zero line 84