OAI/Probability/SKValue/GroundState/ColumnBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValueG.unitOrZero_norm_le_one line 13
2. lemma OAI.SKValueG.columnResidual_norm_le line 20
3. lemma OAI.SKValueG.columnVector_norm_le line 29
4. lemma OAI.SKValueG.columnLinear_bound line 42
5. lemma OAI.SKValueG.quadraticCoeff_coord_bound line 51
6. lemma OAI.SKValueG.measurable_columnResidual line 63
7. lemma OAI.SKValueG.measurable_columnVector line 69
8. lemma OAI.SKValueG.gramSchmidt_eq_sub_sum_nat line 77
9. lemma OAI.SKValueG.measurable_gramSchmidt line 85
10. lemma OAI.SKValueG.measurable_gramSchmidtNormed line 101
11. lemma OAI.SKValueG.gramSchmidtNormed_unitOrZero line 109
12. lemma OAI.SKValueG.gramSchmidtNormed_pairwise_orthogonal line 118