OAI/Analysis/MutuallyUnbiased/Moments/NormalizedPartitions.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.averagedRowProducts line 13

   Source documentation

   Row sampling in an arbitrary number of retained nonzero coordinates.

   def averagedRowProducts {p n : ℕ} (H : CMatrix) (A : Matrix (Fin p) (Fin n) ℤ) : ℝ :=
   …

   Mentions: OAI.MUB6.CMatrix

2. theorem OAI.MUB6.inverse_six_pow_real line 18
3. theorem OAI.MUB6.partition_integrand line 22
4. theorem OAI.MUB6.average_injection_sum line 39
5. theorem OAI.MUB6.averagedRowProducts_partition line 54

   Source documentation

   The normalized equality-pattern expansion. For k blocks the coefficient is card (Fin k ↪ Fin 6) / 6^n, exactly (6)_k / 6^n in the source.

   theorem averagedRowProducts_partition {p n : ℕ} {P : Type*} [Fintype P]
       {H : CMatrix} (hH : IsHadamard H) (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) :
       averagedRowProducts H A =
         ∑ s, ((Fintype.card (Fin (F.blocks s) ↪ Coord) : ℝ) / 6 ^ n) *
           injectiveMoment H (groupedColumns A (F.label s)) := by
   …

   Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.EqualityPatterns.Family, OAI.MUB6.Coord, OAI.MUB6.averagedRowProducts, OAI.MUB6.injectiveMoment, OAI.MUB6.groupedColumns