OAI/Probability/SKValue/GroundState/EmpiricalVectors.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValueG.empiricalVector line 13
  2. lemma OAI.SKValueG.empiricalVector_inner line 16
  3. lemma OAI.SKValueG.iid_sample_law line 31
  4. lemma OAI.SKValueG.iid_prefix_law line 35
  5. lemma OAI.SKValueG.iid_average_tendsto line 42
  6. lemma OAI.SKValueG.empirical_inner_tendsto line 56
  7. lemma OAI.SKValueG.empirical_norm_tendsto_one line 64
  8. lemma OAI.SKValueG.gramSchmidt_congr_prefix line 87
  9. lemma OAI.SKValueG.gramSchmidtNormed_congr_prefix line 99
  10. def OAI.SKValueG.paddedRow line 106
  11. lemma OAI.SKValueG.paddedRow_measurable line 109
  12. def OAI.SKValueG.rawHistory line 116
  13. lemma OAI.SKValueG.rawHistory_measurable line 120
  14. def OAI.SKValueG.predictableDirection line 131
  15. lemma OAI.SKValueG.predictableDirection_measurable line 136
  16. lemma OAI.SKValueG.predictableDirection_unitOrZero line 142
  17. def OAI.SKValueG.rowColumn line 150
  18. def OAI.SKValueG.rowHistory line 153
  19. lemma OAI.SKValueG.rowHistory_init line 156
  20. lemma OAI.SKValueG.rawHistory_rows line 159
  21. lemma OAI.SKValueG.predictableDirection_rows line 173