OAI/Probability/SKValue/GroundState/QuadraticSK.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValueG.spinVector line 14
  2. lemma OAI.SKValueG.spinVector_inner line 17
  3. lemma OAI.SKValueG.spinVector_sqNorm line 20
  4. lemma OAI.SKValueG.spinVector_norm line 24
  5. lemma OAI.SKValueG.finiteMaximum_mul_nonneg line 27
  6. lemma OAI.SKValueG.scaled_linearProcess line 38
  7. lemma OAI.SKValueG.quadratic_spin_distance line 42
  8. theorem OAI.SKValueG.quadraticValue_spin line 59
  9. theorem OAI.SKValueG.finite_adaptive_SK_lower line 74
  10. lemma OAI.SKValueG.orthogonalRemainder_smul line 100
  11. lemma OAI.SKValueG.columnVector_smul line 105
  12. lemma OAI.SKValueG.empiricalVector_scale line 110
  13. lemma OAI.SKValueG.predictableResidual_rows line 120
  14. lemma OAI.SKValueG.predictableOffset_rows line 138
  15. def OAI.SKValueG.empiricalColumnEnergy line 163
  16. lemma OAI.SKValueG.normalizedOffset_rows line 170