OAI/Probability/SKValue/GroundState/GramSchmidtLimit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValueG.inner_approx_tendsto line 13
  2. lemma OAI.SKValueG.norm_approx_tendsto line 25
  3. theorem OAI.SKValueG.gramSchmidt_approx line 33
  4. theorem OAI.SKValueG.gramSchmidtNormed_approx line 69
  5. def OAI.SKValueG.orthogonalRemainder line 104
  6. lemma OAI.SKValueG.inner_orthogonalRemainder line 107
  7. lemma OAI.SKValueG.orthogonalRemainder_succ line 117
  8. lemma OAI.SKValueG.columnResidual_orthogonalRemainder line 122
  9. lemma OAI.SKValueG.column_revealed_energy line 128
  10. lemma OAI.SKValueG.orthogonalRemainder_inner_tendsto line 140
  11. theorem OAI.SKValueG.normalized_column_energy_tendsto line 153