OAI/Probability/SwitchChain/CountCovering.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.CountCoupling.prefixMass line 10
2. theorem OAI.Problem315.CountCoupling.adjacent_transport_identity line 12
3. theorem OAI.Problem315.CountCoupling.adjacent_two_coordinate_expectation_bound line 41
4. def OAI.Problem315.CountCoupling.coveredPairProbability line 100
5. theorem OAI.Problem315.CountCoupling.pairWeight_mass_pos line 104
6. theorem OAI.Problem315.CountCoupling.coveredPairProbability_mass line 111
7. theorem OAI.Problem315.CountCoupling.pairExpectation_eq_probability_sum line 125
8. theorem OAI.Problem315.CountCoupling.probability_prefix_eq_expectation line 136
9. theorem OAI.Problem315.CountCoupling.covered_pairExpectation_shift_le_succ_of_antitone line 149
10. theorem OAI.Problem315.CountCoupling.coveredPairProbability_interlace line 157
11. theorem OAI.Problem315.CountCoupling.pairExpectation_adjacent_sum_bound line 182