OAI/Probability/SKValue/GroundState/EmpiricalCalculus.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValueG.empiricalVector_measurable line 13
2. lemma OAI.SKValueG.iid_average_integrable line 22
3. lemma OAI.SKValueG.iid_average_integral line 31
4. lemma OAI.SKValueG.empiricalVector_norm_sq line 44
5. lemma OAI.SKValueG.empirical_norm_sq_integrable line 49
6. lemma OAI.SKValueG.empirical_norm_sq_integral line 55
7. lemma OAI.SKValueG.empiricalVector_norm_unit line 62
8. lemma OAI.SKValueG.empiricalVector_norm_le_one line 71
9. lemma OAI.SKValueG.orthogonalRemainder_gramSchmidt_norm_le line 87
10. lemma OAI.SKValueG.measurable_orthogonalRemainder line 97
11. lemma OAI.SKValueG.empiricalColumnEnergy_measurable line 108
12. lemma OAI.SKValueG.empiricalColumnEnergy_bound line 120