OAI/Probability/SignedSweeps/FiniteSampling.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.finiteMean line 14
  2. lemma OAI.SignedSweeps.finiteMean_congr line 16
  3. lemma OAI.SignedSweeps.finiteMean_equiv line 19
  4. lemma OAI.SignedSweeps.finiteMean_const line 23
  5. lemma OAI.SignedSweeps.finiteMean_prod line 28
  6. lemma OAI.SignedSweeps.linearMap_finiteMean line 33
  7. lemma OAI.SignedSweeps.finiteMean_reverse_prod line 49
  8. abbrev OAI.SignedSweeps.SweepSettings line 93
  9. def OAI.SignedSweeps.sampleSweep line 95
  10. lemma OAI.SignedSweeps.representation_sampleSweep_average line 98
  11. lemma OAI.SignedSweeps.sweepOperator_eq_sampleMean line 109
  12. lemma OAI.SignedSweeps.tupleSweep_eq_sampleMean line 113
  13. lemma OAI.SignedSweeps.subsetSweep_eq_sampleMean line 117