OAI/Probability/SKValue/GroundState/GaussianColumn.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValueG.columnResidual line 14
  2. def OAI.SKValueG.columnVector line 17
  3. def OAI.SKValueG.quadraticCoeff line 20
  4. def OAI.SKValueG.columnSplitCoeff line 23
  5. lemma OAI.SKValueG.euclidean_inner_sum line 26
  6. lemma OAI.SKValueG.columnResidual_inner line 30
  7. lemma OAI.SKValueG.columnResidual_orthogonal line 38
  8. lemma OAI.SKValueG.quadraticCoeff_inner line 42
  9. lemma OAI.SKValueG.columnVector_inner line 54
  10. lemma OAI.SKValueG.columnSplitCoeff_inner line 70
  11. lemma OAI.SKValueG.columnSplitCoeff_distance line 82
  12. theorem OAI.SKValueG.expected_max_column_split line 90
  13. def OAI.SKValueG.quadraticValue line 112
  14. lemma OAI.SKValueG.linearProcess_integral_zero line 117
  15. lemma OAI.SKValueG.quadraticValue_ge_offset line 129
  16. lemma OAI.SKValueG.column_product_integrable line 140
  17. theorem OAI.SKValueG.quadraticValue_column line 158
  18. lemma OAI.SKValueG.column_integral_integrable line 183