OAI/Analysis/MutuallyUnbiased/Moments/PartitionExpansion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.groupedColumns line 13
2. def OAI.MUB6.rawMonomial line 17
3. def OAI.MUB6.rowFourier line 21
4. theorem OAI.MUB6.prod_zpow_eq_zpow_sum line 24
5. theorem OAI.MUB6.product_grouped line 32
6. theorem OAI.MUB6.rawMonomial_grouped line 43
7. theorem OAI.MUB6.rowFourier_product_expand line 54
8. theorem OAI.MUB6.rowFourier_partition_expand line 68

   Source documentation

   The unnormalized equality-partition identity. The factor (6)_k in the manuscript is exactly the cardinality of the inner injection type.

   theorem rowFourier_partition_expand {p n : ℕ} {P : Type*} [Fintype P]
       {H : CMatrix} (hH : IsHadamard H) (A : Matrix (Fin p) (Fin n) ℤ)
       (ρ : Fin p ↪ Coord) (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) :
       (∏ j, rowFourier H ρ (fun i => A i j)) =
         (6 : ℂ)⁻¹ ^ n * ∑ s, ∑ κ : Fin (F.blocks s) ↪ Coord,
           exponentMonomial H (groupedColumns A (F.label s)) ρ κ := by
   …

   Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.Coord, OAI.MUB6.EqualityPatterns.Family, OAI.MUB6.rowFourier, OAI.MUB6.exponentMonomial, OAI.MUB6.groupedColumns