OAI/Probability/DilutedSpin/TopologyDecay.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.FiniteLaw.map line 13
2. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_map line 21
3. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_pi_map line 31
4. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_bool line 61
5. lemma OAI.DilutedSpinGlass.FiniteLaw.map_spin_weight line 72
6. def OAI.DilutedSpinGlass.FiniteLaw.spinLog line 83
7. lemma OAI.DilutedSpinGlass.FiniteLaw.logMean_pi_spin line 86
8. lemma OAI.DilutedSpinGlass.PrescribedTree.ceil_boundary_bound line 113
9. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_subtree_eta_bound line 122
10. theorem OAI.DilutedSpinGlass.PrescribedTree.qSubtree_limsup_tendsto line 138