OAI/Probability/SwitchChain/FiniteKernelAlgebra.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.FiniteKernel.energy_eq_pairwise line 12
2. theorem OAI.Problem315.FiniteKernel.energy_nonneg line 47
3. theorem OAI.Problem315.FiniteKernel.energy_eq_zero_iff line 58
4. theorem OAI.Problem315.FiniteKernel.eq_of_energy_eq_zero_of_reachable line 90
5. theorem OAI.Problem315.FiniteKernel.weighted_sq_sum_le line 105
6. theorem OAI.Problem315.FiniteKernel.sq_sum_apply_le line 130
7. theorem OAI.Problem315.FiniteKernel.lazy_sq_sum_apply_le_inner line 150
8. theorem OAI.Problem315.FiniteKernel.lazy_inner_nonneg line 192