OAI/Probability/DilutedSpin/ActualTreeSelector.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_pi_comm line 11
2. def OAI.DilutedSpinGlass.MarkSelector.pathColor line 28
3. lemma OAI.DilutedSpinGlass.MarkSelector.abs_pathColor line 33
4. theorem OAI.DilutedSpinGlass.PrescribedTree.actual_tree_selector line 51
5. theorem OAI.DilutedSpinGlass.PrescribedTree.actual_tree_selector_prod line 78

   Source documentation

   The same selector after adjoining the fresh mark prior to ANY previous physical reservoir, including its complete existing mark alphabet and tilt.

   theorem actual_tree_selector_prod {Ω C R : Type} [Fintype Ω]
       [Fintype C] [DecidableEq C] [Fintype R] [DecidableEq R]
       {n : ℕ} (S : PrescribedTree n) (T : KernelTower Ω n)
       (a b : R → C) (d : R → Fin n) (pos : C → S.Leaf) (f : Sample Ω S → ℝ) :
       (S.sampleLaw (KernelTower.prod n T
         (markPrior n (fun _ => FiniteLaw.pi (fun _ : R => rademacher))))).expect
         (fun x => f (sampleFst S x) * ∏ c, pathColor a b d c
           (KernelTower.pathSnd n (S.pathAt (pos c) x))) =
         (S.sampleLaw T).expect f *
           ∏ r, if (d r).val+1 ≤ splitDepth S (pos (a r)) (pos (b r)) then (1:ℝ) else 0 := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.KernelTower.prod, OAI.DilutedSpinGlass.markPrior, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.PrescribedTree.sampleFst, OAI.DilutedSpinGlass.KernelTower.pathSnd, OAI.DilutedSpinGlass.PrescribedTree.splitDepth