OAI/Probability/DilutedSpin/ForkTree.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.fork line 13

   Source documentation

   k paths with a common d-coordinate prefix, no contracted unary levels.

   def fork (h : ℕ) (k : ℕ+) : (d : ℕ) → PrescribedTree (h+1+d)
     | 0 => .node k (fun _ => single h)
     | d+1 => .node 1 (fun _ => fork h k d)

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.single

2. def OAI.DilutedSpinGlass.PrescribedTree.forkLeaf line 17
3. def OAI.DilutedSpinGlass.PrescribedTree.forkVertex line 21
4. lemma OAI.DilutedSpinGlass.PrescribedTree.leaf_single_unique line 25
5. lemma OAI.DilutedSpinGlass.PrescribedTree.forkLeaf_surjective line 34
6. lemma OAI.DilutedSpinGlass.PrescribedTree.forkLeaf_injective line 48
7. lemma OAI.DilutedSpinGlass.PrescribedTree.fork_split line 56
8. lemma OAI.DilutedSpinGlass.PrescribedTree.fork_gamma line 64
9. lemma OAI.DilutedSpinGlass.PrescribedTree.fork_fresh_split line 71
10. lemma OAI.DilutedSpinGlass.PrescribedTree.fork_zero_expect line 81

    Source documentation

    At the actual branching vertex every child is a full independent kernel path. Proves the full joint law, not just product moments.

    lemma fork_zero_expect (h : ℕ) (k : ℕ+) (T : KernelTower Ω (h+1))
        (F : (Fin k → FinitePath Ω (h+1)) → ℝ) :
        ((fork h k 0).sampleLaw T).expect
          (fun x => F (fun i => (fork h k 0).pathAt (forkLeaf h k 0 i) x)) =
          (FiniteLaw.pi (fun _ : Fin k => KernelTower.law (h+1) T)).expect F := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.fork, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.forkLeaf, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.KernelTower.law