OAI/Probability/SwitchChain/PairFiberEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.PairResampling.sum_expectation line 13
2. theorem OAI.Problem315.PairResampling.sum_fiber_average line 23
3. theorem OAI.Problem315.PairResampling.inner_fluctuation_eq_sum_fiber_variance line 29
4. theorem OAI.Problem315.PairResampling.inner_fluctuation_le_of_fiber_variance_bound line 59
5. theorem OAI.Problem315.PairFiber.assignment_average_eq_fiber_average line 78
6. theorem OAI.Problem315.PairFiber.inner_fluctuation_le_of_assignment_variance_bound line 89
7. theorem OAI.Problem315.PairFiber.inner_fluctuation_le_of_assignment_sum_bound line 107