OAI/Analysis/MutuallyUnbiased/Moments/Moments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite injective moments of Section 2 of the exact companion. Both orientations are retained with weight 1/2, including when H = Hᵀ.

  1. def OAI.MUB6.exponentMonomial line 15
  2. def OAI.MUB6.injectiveMoment line 19
  3. theorem OAI.MUB6.exponentMonomial_norm line 24
  4. theorem OAI.MUB6.injectiveMoment_abs_le_one line 30
  5. def OAI.MUB6.pairAverage line 45

    Source documentation

    Equation (pair-average), with the two orientations counted separately.

    def pairAverage (H : CMatrix) (F : CMatrix → ℝ) : ℝ :=
…

    Mentions: OAI.MUB6.CMatrix

  6. theorem OAI.MUB6.pairAverage_nonneg line 49
  7. theorem OAI.MUB6.pairAverage_zero_terms line 55