OAI/Probability/SKRatio/Variational/ScalarHilbert.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Scalar.l2Norm line 14
2. lemma OAI.SKRatio.Scalar.l2Norm_nonneg line 16
3. lemma OAI.SKRatio.Scalar.l2Norm_sq line 17
4. lemma OAI.SKRatio.Scalar.abs_integral_mul_le line 20
5. lemma OAI.SKRatio.Scalar.integral_mul_sq_le line 29
6. lemma OAI.SKRatio.Scalar.integral_pairing_add line 35
7. lemma OAI.SKRatio.Scalar.integral_square_add line 45
8. theorem OAI.SKRatio.Scalar.rank_two_bound line 58
9. def OAI.SKRatio.Scalar.centered line 105
10. def OAI.SKRatio.Scalar.sd line 106
11. lemma OAI.SKRatio.Scalar.sd_nonneg line 109
12. lemma OAI.SKRatio.Scalar.memLp_centered line 111
13. lemma OAI.SKRatio.Scalar.integral_centered line 114
14. lemma OAI.SKRatio.Scalar.pairing_centered line 120
15. lemma OAI.SKRatio.Scalar.abs_pairing_centered_le line 131
16. lemma OAI.SKRatio.Scalar.pairing_centered_sq_le line 137
17. lemma OAI.SKRatio.Scalar.l2_decomposition line 145
18. lemma OAI.SKRatio.Scalar.integral_mul_decomposition line 151