OAI/Probability/BinarySweep/FiniteLaws/FiniteLawAverage.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.finiteLaw_complex_expectation line 14
  2. lemma OAI.BinaryCoordinateSweeps.uniform_average_product line 24
  3. lemma OAI.BinaryCoordinateSweeps.complexAverage_finiteLaw line 35
  4. lemma OAI.BinaryCoordinateSweeps.binary_average_product line 42
  5. lemma OAI.BinaryCoordinateSweeps.finiteLaw_pi line 51
  6. lemma OAI.BinaryCoordinateSweeps.finiteLaw_equiv line 69
  7. lemma OAI.BinaryCoordinateSweeps.finiteLaw_complex_comp_expectation line 76
  8. def OAI.BinaryCoordinateSweeps.pushLaw line 89
  9. lemma OAI.BinaryCoordinateSweeps.finiteLaw_pushLaw line 92
  10. lemma OAI.BinaryCoordinateSweeps.pushLaw_expectation line 95
  11. lemma OAI.BinaryCoordinateSweeps.pushLaw_comp line 103
  12. lemma OAI.BinaryCoordinateSweeps.pushLaw_equiv line 110
  13. lemma OAI.BinaryCoordinateSweeps.pushLaw_equiv_apply line 116
  14. lemma OAI.BinaryCoordinateSweeps.pushLaw_id line 121
  15. lemma OAI.BinaryCoordinateSweeps.pushLaw_prod line 124
  16. lemma OAI.BinaryCoordinateSweeps.pushLaw_pi line 139
  17. lemma OAI.BinaryCoordinateSweeps.uniformLaw_prod line 157
  18. lemma OAI.BinaryCoordinateSweeps.uniformLaw_pi line 162
  19. lemma OAI.BinaryCoordinateSweeps.uniformLaw_equiv line 167