OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleRules.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSemantics.single_label_two line 13

   Source documentation

   The two equality patterns for the sampled column indices.

   theorem single_label_two {p : ℕ} (B : Fin 7 → Basis) (hB : IsMUBFamily B)
       (A : Matrix (Fin p) (Fin 2) ℤ) :
       mixedMoment B A (fun _ => (0 : Fin 1)) =
         (1 / 6 : ℝ) * familyPairMoment B (groupedColumns A (EqualityPatterns.family2.label 0)) +
         (5 / 6 : ℝ) * familyPairMoment B (groupedColumns A (EqualityPatterns.family2.label 1)) := by
   …

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

2. theorem OAI.MUB6.Certificate.MixedSemantics.single_label_three line 26

   Source documentation

   The five equality patterns for three sampled column indices.

   theorem single_label_three {p : ℕ} (B : Fin 7 → Basis) (hB : IsMUBFamily B)
       (A : Matrix (Fin p) (Fin 3) ℤ) :
       mixedMoment B A (fun _ => (0 : Fin 1)) =
         (1 / 36 : ℝ) * familyPairMoment B (groupedColumns A (EqualityPatterns.family3.label 0)) +
         (5 / 36 : ℝ) * familyPairMoment B (groupedColumns A (EqualityPatterns.family3.label 1)) +
         (5 / 36 : ℝ) * familyPairMoment B (groupedColumns A (EqualityPatterns.family3.label 2)) +
         (5 / 36 : ℝ) * familyPairMoment B (groupedColumns A (EqualityPatterns.family3.label 3)) +
         (5 / 9 : ℝ) * familyPairMoment B (groupedColumns A (EqualityPatterns.family3.label 4)) := by
   …

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