OAI/Analysis/MutuallyUnbiased/Moments/Sampling.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite sampling identities. The splitting theorem below is the counting step behind contraction of an order-one row; it is independent of the values of the matrix entries and uses no certificate data.

  1. theorem OAI.MUB6.Sampling.sum_split_embedding line 19
  2. def OAI.MUB6.Sampling.dropFirst line 27
  3. theorem OAI.MUB6.Sampling.dropFirst_apply line 31
  4. theorem OAI.MUB6.Sampling.sum_injective_extension line 34
  5. theorem OAI.MUB6.Sampling.sum_samples_split line 42
  6. theorem OAI.MUB6.Sampling.sum_contraction line 55