OAI/Probability/DilutedSpin/SubsetTree.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.SplitMap.ofChildren line 12
2. lemma OAI.DilutedSpinGlass.PrescribedTree.SplitMap.leaves_le line 23
3. theorem OAI.DilutedSpinGlass.PrescribedTree.exists_subset_tree line 30

   Source documentation

   Every nonempty set of leaf positions has its literal induced leveled tree. Singleton unary stretches are kept; a SplitMap retains the exact pair splits.

   theorem exists_subset_tree {n : ℕ} (T : PrescribedTree n) (A : Finset T.Leaf) (hA : A.Nonempty) :
       ∃ (U : PrescribedTree n) (f : SplitMap U T), ∀ b, (∃ a, f.leaf a=b) ↔ b∈A := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.SplitMap