OAI/Probability/SKValue/GroundState/GaussianTree.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SKValueG.TreeLevel line 12
  2. abbrev OAI.SKValueG.GaussianTree line 17
  3. abbrev OAI.SKValueG.TreeLeaves line 19
  4. abbrev OAI.SKValueG.TreeEdges line 23
  5. instance OAI.SKValueG.treeLeavesFintype line 27
  6. instance OAI.SKValueG.treeLeavesNonempty line 31
  7. instance OAI.SKValueG.treeEdgesFintype line 35
  8. def OAI.SKValueG.treePathCoeff line 40
  9. def OAI.SKValueG.treeOverlap line 47
  10. def OAI.SKValueG.ValidTreeGrid line 51
  11. lemma OAI.SKValueG.treePath_inner_node line 55
  12. def OAI.SKValueG.treeFieldVector line 77
  13. def OAI.SKValueG.treeAuxVector line 80
  14. lemma OAI.SKValueG.treeField_inner line 83
  15. lemma OAI.SKValueG.treeAux_inner line 101
  16. lemma OAI.SKValueG.treeOverlap_self line 121
  17. lemma OAI.SKValueG.treeField_unit line 127
  18. lemma OAI.SKValueG.treeAux_distance line 133