OAI/Probability/SwitchChain/TransitiveAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.TransitiveAverage.sum_smul_eq line 14
2. theorem OAI.Problem315.TransitiveAverage.card_mul_sum_smul line 22
3. theorem OAI.Problem315.TransitiveAverage.average_smul_eq line 39
4. theorem OAI.Problem315.TransitiveAverage.average_sum_sq_difference line 48