OAI/Probability/SwitchChain/Energy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.FiniteEnergy.column_sum_of_symmetric line 12
2. theorem OAI.Problem315.FiniteEnergy.sum_sq_sub line 20
3. theorem OAI.Problem315.FiniteEnergy.dirichlet_eq_half_sum line 51
4. theorem OAI.Problem315.FiniteEnergy.uniform_dirichlet_eq line 71
5. theorem OAI.Problem315.FiniteEnergy.dirichlet_nonneg line 81
6. theorem OAI.Problem315.FiniteEnergy.dirichlet_add_const line 96
7. theorem OAI.Problem315.FiniteEnergy.dirichlet_eq_zero_iff line 107
8. theorem OAI.Problem315.FiniteEnergy.row_square_le line 142
9. theorem OAI.Problem315.FiniteEnergy.l2_contraction line 156
10. theorem OAI.Problem315.FiniteEnergy.sum_apply line 172
11. theorem OAI.Problem315.FiniteEnergy.quadratic_lower_bound line 182