OAI/Analysis/MutuallyUnbiased/Moments/OrderedPairs.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.reversePair line 11
2. theorem OAI.MUB6.reversePair_involutive line 14
3. def OAI.MUB6.reversePairEquiv line 20
4. def OAI.MUB6.familyAverage line 23
5. def OAI.MUB6.familyPairMoment line 26
6. theorem OAI.MUB6.familyPairMoment_abs_le_one line 29
7. theorem OAI.MUB6.familyAverage_add line 37
8. theorem OAI.MUB6.familyAverage_mul line 41
9. theorem OAI.MUB6.relativeMatrix_reverse line 45
10. theorem OAI.MUB6.familyAverage_transpose line 51
11. def OAI.MUB6.unorientedRowProducts line 66
12. theorem OAI.MUB6.rowFourier_conjugate line 69
13. theorem OAI.MUB6.unorientedRowProducts_conjugate line 73
14. theorem OAI.MUB6.averagedRowProducts_split line 80
15. theorem OAI.MUB6.familyAverage_averagedRowProducts line 92
16. def OAI.MUB6.singletonEmbeddingEquiv line 101
17. theorem OAI.MUB6.mixedMoment_single_label line 110
18. theorem OAI.MUB6.mixedMoment_single_label_partition line 127

    Source documentation

    Single-label mixed moments expand into the manuscript's transpose-averaged pair moments with the exact falling-factorial weights.

    theorem mixedMoment_single_label_partition {p n : ℕ} {P : Type*} [Fintype P]
        (B : Fin 7 → Basis) (hB : IsMUBFamily B) (A : Matrix (Fin p) (Fin n) ℤ)
        (F : EqualityPatterns.Family (Fin n) P)
        (cover : ∀ f : Fin n → Coord, ∃ s, ∀ i j,
          F.label s i = F.label s j ↔ f i = f j) :
        mixedMoment B A (fun _ => (0 : Fin 1)) =
          ∑ s, ((Fintype.card (Fin (F.blocks s) ↪ Coord) : ℝ) / 6 ^ n) *
            familyPairMoment B (groupedColumns A (F.label s)) := by
    …

    Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.EqualityPatterns.Family, OAI.MUB6.Coord, OAI.MUB6.mixedMoment, OAI.MUB6.familyPairMoment, OAI.MUB6.groupedColumns