ShapeMarginal.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.SplitMap.pullSample line 14
Source documentation
Delete all unselected branches of an actual history. Unary vertices and all ancestor coordinates are retained.
```
def pullSample : {n : ℕ} → {T S : PrescribedTree n} →
    SplitMap T S → Sample Ω S → Sample Ω T
  | 0, .leaf, .leaf, _, _ => ()
  | _+1, .node _ _, .node _ _, f, x =>
    fun i => ((x (f.childIndex i)).1,pullSample (f.child i) (x (f.childIndex i)).2)
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.SplitMap, OAI.DilutedSpinGlass.PrescribedTree.Sample
lemma OAI.DilutedSpinGlass.PrescribedTree.SplitMap.pathAt_pullSample line 20
theorem OAI.DilutedSpinGlass.PrescribedTree.SplitMap.expect_pullSample line 38
Source documentation
Every exact prescribed splitting matrix has the same sampling law in EVERY actual extension, jointly over its entire selected leaf family.
```
theorem expect_pullSample {n : ℕ} {T S : PrescribedTree n} (f : SplitMap T S)
    (K : KernelTower Ω n) (F : Sample Ω T → ℝ) :
    (S.sampleLaw K).expect (fun x => F (f.pullSample x)) = (T.sampleLaw K).expect F := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.SplitMap, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Sample
theorem OAI.DilutedSpinGlass.PrescribedTree.SplitMap.expect_paths line 70
Source documentation
Same joint marginal expressed directly in leaf paths, so terminal overlap and projection-error observables can use it without any sample relabeling.
```
theorem expect_paths {n : ℕ} {T S : PrescribedTree n} (f : SplitMap T S)
    (K : KernelTower Ω n) (F : (T.Leaf → FinitePath Ω n) → ℝ) :
    (S.sampleLaw K).expect (fun x => F (fun a => S.pathAt (f.leaf a) x)) =
      (T.sampleLaw K).expect (fun x => F (fun a => T.pathAt a x)) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.SplitMap, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath