OAI/Probability/ProjectionMoments/CapDuality.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ProjectionMoments.measurable_radialLabel line 18
2. lemma OAI.ProjectionMoments.rowMap_mixRows line 30
3. lemma OAI.ProjectionMoments.polar_label_identity line 35
4. lemma OAI.ProjectionMoments.normalizedDensity_unitBall line 44
5. lemma OAI.ProjectionMoments.measurable_capReferenceLabel line 61
6. lemma OAI.ProjectionMoments.measurable_capKernelValue line 67
7. lemma OAI.ProjectionMoments.capReference_le_one line 73
8. lemma OAI.ProjectionMoments.capKernelValue_le_one line 81
9. lemma OAI.ProjectionMoments.cap_kernel_test_identity line 88
10. lemma OAI.ProjectionMoments.holder_bounded_kernel line 128
11. lemma OAI.ProjectionMoments.cap_exp_root line 143
12. lemma OAI.ProjectionMoments.cap_dual_estimate line 149