OAI/Analysis/MutuallyUnbiased/MixedSemantics/PairAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.familyPairVector line 12

   Source documentation

   The pair certificate coordinates averaged over ordered pairs of bases.

   def familyPairVector (B : Fin 7 → Basis) : Fin 909 → ℝ :=
   …

   Mentions: OAI.MUB6.Basis

2. theorem OAI.MUB6.Certificate.MixedSemantics.familyPairVector_abs_le_one line 15
3. theorem OAI.MUB6.Certificate.MixedSemantics.eval_familyPairVector line 23
4. theorem OAI.MUB6.Certificate.MixedSemantics.familyPairMoment_of_pointwise line 32