OAI/Probability/DilutedSpin/CommonTreeSample.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.KernelTower.Projects.refl line 11
2. lemma OAI.DilutedSpinGlass.KernelTower.Projects.comp line 16
3. lemma OAI.DilutedSpinGlass.KernelTower.Projects.prod line 26
4. lemma OAI.DilutedSpinGlass.KernelTower.pi_prod_projects line 46
5. lemma OAI.DilutedSpinGlass.KernelTower.Projects.pi line 64
6. lemma OAI.DilutedSpinGlass.KernelTower.pathMap_comp line 73
7. lemma OAI.DilutedSpinGlass.PrescribedTree.prod_pi_sample_expect line 90
8. lemma OAI.DilutedSpinGlass.PrescribedTree.common_sample_expect line 107

   Source documentation

   Each new label is independently sampled, including its root, on the same prescribed replica tree as the old system.

   lemma common_sample_expect (S : PrescribedTree n) (T : KernelTower Ω n)
       (Q : FiniteLaw R) (U : R → KernelTower Λ n)
       (g : (ι → R×Sample Λ S) → Sample Ω S → ℝ) :
       (FiniteLaw.pi (fun _ : ι => Q)).expect (fun r =>
         (S.sampleLaw (KernelTower.prod n T (KernelTower.piTower n (fun j : ι => U (r j))))).expect
           (fun w => g (fun j => (r j,sampleMap (fun x : ι → Λ => x j) S (sampleSnd S w)))
             (sampleFst S w))) =
       (S.sampleLaw T).expect (fun old =>
         (FiniteLaw.pi (fun _ : ι => Q.bind (fun r => S.sampleLaw (U r)))).expect
           (fun fresh => g fresh old)) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.KernelTower.prod, OAI.DilutedSpinGlass.KernelTower.piTower, OAI.DilutedSpinGlass.PrescribedTree.sampleMap, OAI.DilutedSpinGlass.PrescribedTree.sampleSnd, OAI.DilutedSpinGlass.PrescribedTree.sampleFst

9. lemma OAI.DilutedSpinGlass.PrescribedTree.leafProduct_eq_fin_prod line 135
10. def OAI.DilutedSpinGlass.PrescribedTree.mixedTreeD line 141
11. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedTree_leafProduct line 148
12. lemma OAI.DilutedSpinGlass.PrescribedTree.common_tree_sample line 160
13. lemma OAI.DilutedSpinGlass.PrescribedTree.common_tree_point line 179