OAI/Probability/SKValue/GroundState/TreeGuerra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValueG.treeAux_tensor_distance line 13
  2. lemma OAI.SKValueG.expected_treeAux_eq_tensor line 22
  3. theorem OAI.SKValueG.finite_tree_guerra_upper line 32
  4. lemma OAI.SKValueG.finiteMaximum_prod_curry_left line 52
  5. lemma OAI.SKValueG.treeLinear_step line 65
  6. def OAI.SKValueG.treeCenter line 76
  7. def OAI.SKValueG.treeOffset line 80
  8. lemma OAI.SKValueG.treePathCoeff_const_q line 83
  9. lemma OAI.SKValueG.treeOffset_step line 89
  10. def OAI.SKValueG.scalarTreeValue line 98
  11. lemma OAI.SKValueG.scalarTreeValue_step line 102
  12. def OAI.SKValueG.fieldTreeValue line 125
  13. lemma OAI.SKValueG.fieldTreeValue_step line 129