OAI/Probability/SKValue/GroundState/GaussianTranspose.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValueG.uncurryGaussian line 14
  2. lemma OAI.SKValueG.uncurryGaussian_preserving line 26
  3. def OAI.SKValueG.transposeGaussian line 42
  4. lemma OAI.SKValueG.transposeGaussian_apply line 48
  5. lemma OAI.SKValueG.transposeGaussian_preserving line 51
  6. lemma OAI.SKValueG.iid_gaussian_columns_law line 58
  7. lemma OAI.SKValueG.measurable_finite_eval line 75
  8. def OAI.SKValueG.rowSpin line 88
  9. lemma OAI.SKValueG.rowSpin_measurable line 92
  10. lemma OAI.SKValueG.rowSpin_rows line 98
  11. lemma OAI.SKValueG.rowHistory_full line 107
  12. theorem OAI.SKValueG.empirical_finite_spin_lower line 112