OAI/Probability/DilutedSpin/BranchingEvaluation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.branchingMean line 10
2. def OAI.DilutedSpinGlass.PrescribedTree.branchingProduct line 16
3. lemma OAI.DilutedSpinGlass.PrescribedTree.branchingProduct_eq_prod line 23
4. lemma OAI.DilutedSpinGlass.PrescribedTree.branchingMean_eq_expect line 34
5. lemma OAI.DilutedSpinGlass.PrescribedTree.branchingMean_pi line 56