OAI/Probability/SKRatio/Variational/ScalarKernel.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Scalar.m line 11
2. def OAI.SKRatio.Scalar.v line 12
3. def OAI.SKRatio.Scalar.w line 13
4. def OAI.SKRatio.Scalar.kernel line 14
5. def OAI.SKRatio.Scalar.g line 15
6. def OAI.SKRatio.Scalar.q line 16
7. def OAI.SKRatio.Scalar.rho line 17
8. lemma OAI.SKRatio.Scalar.m_bounds line 19
9. lemma OAI.SKRatio.Scalar.v_pos line 21
10. lemma OAI.SKRatio.Scalar.v_le_one line 22
11. lemma OAI.SKRatio.Scalar.w_pos line 23
12. lemma OAI.SKRatio.Scalar.v_factor line 24
13. lemma OAI.SKRatio.Scalar.kernel_nonneg line 25
14. lemma OAI.SKRatio.Scalar.kernel_diag line 27
15. lemma OAI.SKRatio.Scalar.kernel_diag_le_one line 34
16. lemma OAI.SKRatio.Scalar.kernel_square_le line 41
17. lemma OAI.SKRatio.Scalar.abs_kernel_le_one line 51
18. lemma OAI.SKRatio.Scalar.residual_identity line 58
19. lemma OAI.SKRatio.Scalar.rho_eq line 69
20. lemma OAI.SKRatio.Scalar.rho_nonneg line 76
21. lemma OAI.SKRatio.Scalar.rho_le_one line 80
22. lemma OAI.SKRatio.Scalar.abs_g_le_one line 86
23. lemma OAI.SKRatio.Scalar.abs_residual_le line 94
24. lemma OAI.SKRatio.Scalar.continuous_m line 106
25. lemma OAI.SKRatio.Scalar.continuous_v line 110
26. lemma OAI.SKRatio.Scalar.continuous_w line 111
27. lemma OAI.SKRatio.Scalar.continuous_g line 112
28. lemma OAI.SKRatio.Scalar.continuous_kernel line 117
29. lemma OAI.SKRatio.Scalar.continuous_rho line 122
30. lemma OAI.SKRatio.Scalar.memLp_g line 129
31. lemma OAI.SKRatio.Scalar.memLp_sqrt_rho line 134
32. lemma OAI.SKRatio.Scalar.integrable_rho line 142
33. lemma OAI.SKRatio.Scalar.integral_abs_mul_sq_le line 147
34. lemma OAI.SKRatio.Scalar.kernel_pair_integrable line 158
35. theorem OAI.SKRatio.Scalar.kernel_bound line 174
36. lemma OAI.SKRatio.Scalar.integral_rho_nonneg line 201