OAI/Probability/SKValue/Equations/MemLpLinearCombination.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.memLp_linearCombination line 14
2. lemma OAI.SKValue.integral_linearCombination_mul line 18
3. lemma OAI.SKValue.orthogonal_linearCombination_coefficient line 29
4. lemma OAI.SKValue.orthogonal_linearCombination_square line 36
5. lemma OAI.SKValue.finite_bessel line 48
6. lemma OAI.SKValue.finite_projection_error line 87