MatrixConstant.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_congr_one line 15

theorem OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory_one line 29

Source documentation

The anchor-alone complete matrix history is its exact signed kappa times the single-target marginal observable. In fact the same identity holds with any unused old tree, as long as its test is one.

theorem weightedMatrixHistory_one (T : PrescribedTree n) (q : C → T.Leaf)
    (hq : Function.Bijective q) (K : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (hm : StrictMono m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last n) = 1)
    (a : C) (cs : List C) (hcs : cs.Nodup) (hdis : ∀ c ∈ cs, c ≠ a)
    (hfull : ({a} : Finset C) ∪ cs.toFinset = Finset.univ)
    (S : PrescribedTree n) (x : S.Leaf) (A : (C → FinitePath Ω n) → ℝ) :
    weightedMatrixHistory T q
      (fun D pos g => (D.sampleLaw K).expect (fun z => g z*A (fun c => D.pathAt (pos c) z)))
      m cs S (Finset.univ.erase x) id (fun _ => x) (fun _ => 1) =
    partialKappa T m (Finset.univ.image q) *
      (T.sampleLaw K).expect (fun z => A (fun c => T.pathAt (q c) z)) := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory, OAI.DilutedSpinGlass.PrescribedTree.partialKappa

lemma OAI.DilutedSpinGlass.PrescribedTree.partialKappa_pair line 79