OAI/Probability/BinarySweep/FiniteLaws/IndependentOperator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.independent_reverse_product line 14
2. lemma OAI.BinaryCoordinateSweeps.weighted_reverse_product line 32
3. lemma OAI.BinaryCoordinateSweeps.independent_average_product line 43
4. lemma OAI.BinaryCoordinateSweeps.reverse_product_norm_le_one line 52
5. lemma OAI.BinaryCoordinateSweeps.pi_single_reverse line 70
6. def OAI.BinaryCoordinateSweeps.continuousRep line 97
7. lemma OAI.BinaryCoordinateSweeps.complexAverage_sum line 102
8. theorem OAI.BinaryCoordinateSweeps.pi_average_norm_le_one line 107
9. lemma OAI.BinaryCoordinateSweeps.pi_comp_average_norm_le_one line 134