OAI/Probability/SKValue/GroundState/TreeProductLaw.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValueG.measurePreserving_finite_curry line 13
  2. lemma OAI.SKValueG.measurePreserving_nodeBlocks line 23
  3. lemma OAI.SKValueG.measurePreserving_midSwap line 35
  4. def OAI.SKValueG.gaussianAddLaw line 45
  5. instance OAI.SKValueG.gaussianAddLaw_probability line 48
  6. lemma OAI.SKValueG.gaussianAddLaw_integrable line 53
  7. lemma OAI.SKValueG.gaussianAddLaw_exp_integrable line 59
  8. lemma OAI.SKValueG.gaussianAddLaw_exp line 72
  9. def OAI.SKValueG.edgeNoiseLaw line 94
  10. instance OAI.SKValueG.edgeNoiseLaw_probability line 95
  11. def OAI.SKValueG.scalarTreeLaw line 98
  12. instance OAI.SKValueG.scalarTreeLaw_probability line 102
  13. def OAI.SKValueG.scalarTreeEval line 111
  14. lemma OAI.SKValueG.finiteMaximum_const line 115
  15. lemma OAI.SKValueG.scalarTreeEval_nil line 120
  16. lemma OAI.SKValueG.continuous_scalarTreeEval line 126
  17. lemma OAI.SKValueG.marked_gaussianAddLaw line 135
  18. lemma OAI.SKValueG.scalarTreeEval_step line 146
  19. theorem OAI.SKValueG.scalarTreeEval_law line 166
  20. lemma OAI.SKValueG.scalarTreeLaw_integrable line 192