OAI/Probability/SKRatio/Variational/ScalarReduction.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Scalar.multiplier_strict_pos line 11
2. lemma OAI.SKRatio.Scalar.abs_inv_multiplier_le line 14
3. lemma OAI.SKRatio.Scalar.continuous_inv_multiplier line 18
4. lemma OAI.SKRatio.Scalar.abs_v_sum_le line 21
5. lemma OAI.SKRatio.Scalar.v_sum_sq_le line 25
6. lemma OAI.SKRatio.Scalar.abs_diagonal_kernel_le line 28
7. lemma OAI.SKRatio.Scalar.continuous_diagonal_kernel line 35
8. def OAI.SKRatio.Scalar.diagonal line 45
9. def OAI.SKRatio.Scalar.cost line 48
10. lemma OAI.SKRatio.Scalar.integrable_multiplier line 51
11. lemma OAI.SKRatio.Scalar.mean_multiplier_pos line 56
12. lemma OAI.SKRatio.Scalar.continuous_diagonal line 62
13. lemma OAI.SKRatio.Scalar.abs_diagonal_le line 75
14. lemma OAI.SKRatio.Scalar.abs_cost_integrand_le line 87
15. lemma OAI.SKRatio.Scalar.continuous_cost_integrand line 98
16. lemma OAI.SKRatio.Scalar.continuous_cost line 103
17. lemma OAI.SKRatio.Scalar.abs_cost_le line 114
18. lemma OAI.SKRatio.Scalar.memLp_v_sum_mul line 127
19. lemma OAI.SKRatio.Scalar.integral_v_sum_mul line 136
20. def OAI.SKRatio.Scalar.radicand line 143
21. lemma OAI.SKRatio.Scalar.radicand_nonneg line 148
22. lemma OAI.SKRatio.Scalar.integral_centered_sq line 152
23. lemma OAI.SKRatio.Scalar.v_sum_square_integrable line 167
24. lemma OAI.SKRatio.Scalar.radicand_expansion line 174
25. lemma OAI.SKRatio.Scalar.radicand_le line 184
26. lemma OAI.SKRatio.Scalar.continuous_radicand line 193
27. lemma OAI.SKRatio.Scalar.memLp_sqrt_radicand line 212
28. lemma OAI.SKRatio.Scalar.integrable_radical line 220
29. lemma OAI.SKRatio.Scalar.memLp_multiplier line 224
30. lemma OAI.SKRatio.Scalar.integral_weighted_square line 229
31. lemma OAI.SKRatio.Scalar.young_radical_pointwise line 258
32. lemma OAI.SKRatio.Scalar.cost_product_integrable line 268
33. lemma OAI.SKRatio.Scalar.cost_fubini line 275
34. lemma OAI.SKRatio.Scalar.integrable_cost_quadratic line 289
35. lemma OAI.SKRatio.Scalar.integrable_multiplier_square line 297
36. lemma OAI.SKRatio.Scalar.memLp_linear_v line 303
37. lemma OAI.SKRatio.Scalar.integral_linear_v line 306
38. lemma OAI.SKRatio.Scalar.integrable_linear_v_cost line 312
39. lemma OAI.SKRatio.Scalar.radical_young line 319
40. def OAI.SKRatio.Scalar.variational line 371
41. def OAI.SKRatio.Scalar.coherent line 380
42. lemma OAI.SKRatio.Scalar.coherent_paired_integrable line 387
43. lemma OAI.SKRatio.Scalar.coherent_paired_expansion line 398
44. lemma OAI.SKRatio.Scalar.integrable_diagonal_quadratic line 413
45. theorem OAI.SKRatio.Scalar.variational_young line 420
46. lemma OAI.SKRatio.Scalar.integrable_total_coefficient line 437
47. theorem OAI.SKRatio.Scalar.variational_bound_of_two_estimates line 445