OAI/Probability/SKValue/Equations/SumStepsSub.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.sum_steps_sub line 18
2. lemma OAI.SKValue.sum_local_residual line 23
3. lemma OAI.SKValue.sum_local_residual_bound line 27
4. lemma OAI.SKValue.finite_envelope_memLp line 37
5. lemma OAI.SKValue.integral_square_add_le line 50
6. lemma OAI.SKValue.discrete_gradient_residual_L2 line 63