OAI/Probability/DilutedSpin/TreeSampleProjection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.firstLeaf line 10
2. lemma OAI.DilutedSpinGlass.PrescribedTree.sample_ext line 15

   Source documentation

   The paths at all leaf positions determine the entire sample.

   lemma sample_ext {n : ℕ} (S : PrescribedTree n) {x y : Sample Ω S}
       (h : ∀ a : S.Leaf, S.pathAt a x = S.pathAt a y) : x = y := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample

3. lemma OAI.DilutedSpinGlass.PrescribedTree.sampleFst_oldSample line 27
4. lemma OAI.DilutedSpinGlass.PrescribedTree.sampleSnd_oldSample line 38