OAI/Probability/DilutedSpin/CavityAllocation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.cavityJoin line 15

   Source documentation

   Duplicate every block at every site before selecting its actual allocation. The unused duplicates disappear by prior-law projection, not by independence of tilted physical sites.

   def cavityJoin : (l : ℕ) → RootPath ι l →
       (ι → CavityState Ω Λ p l) → CavityState (ι → Ω) Λ p l
     | 0,_,z => z
     | l+1,c,z => (cavityJoin l c.2 (fun i => (z i).1),(z c.1).2)
   
   omit [Fintype R] in

   Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.PrescribedTree.CavityState

2. lemma OAI.DilutedSpinGlass.PrescribedTree.cavityJoin_projects line 21
3. lemma OAI.DilutedSpinGlass.PrescribedTree.pathMap_cavityJoin_zero line 36
4. lemma OAI.DilutedSpinGlass.PrescribedTree.pathFst_cavityJoin line 41
5. lemma OAI.DilutedSpinGlass.PrescribedTree.pathSnd_cavityJoin line 50
6. lemma OAI.DilutedSpinGlass.PrescribedTree.cavityProject_join line 59
7. lemma OAI.DilutedSpinGlass.PrescribedTree.cavityProject_pathJoin line 67