OAI/Analysis/MutuallyUnbiased/MixedMoments/MixedReduction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.rowFourier_zero_first line 10
2. theorem OAI.MUB6.mixedMoment_zero_first_row line 16
3. theorem OAI.MUB6.mixedMoment_unused_first_label line 33
4. theorem OAI.MUB6.mixedMoment_zero_first_factor line 45
5. theorem OAI.MUB6.mixedMoment_singleton_first line 62

   Source documentation

   The source singleton-label contraction, before dividing by its positive integer coefficient. The first factor has order two and its own label.

   theorem mixedMoment_singleton_first {p n l : ℕ} (hl : l < 6)
       (B : Fin 7 → Basis) (hB : IsMUBFamily B)
       (A : Matrix (Fin p) (Fin (n + 1)) ℤ) (label : Fin n → Fin l)
       (ha : ∑ i, A i 0 = 0) (ho : ∑ i, (A i 0).toNat = 2) :
       ((6 - l : ℕ) : ℝ) * mixedMoment B A (Fin.cases 0 (Fin.succ ∘ label)) +
         (∑ j : Fin l, mixedMoment B A (Fin.cases j label)) = 0 := by
   …

   Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.mixedMoment