OAI/Probability/DilutedSpin/HistoryRetained.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_protected_function line 14

   Source documentation

   A function of protected paths is transported jointly with the full old test through EVERY fresh extension. This is an identity of signed histories.

   theorem labeledHistory_protected_function (m : Fin (n+1) → ℝ)
       (V : (S : PrescribedTree n) → (C → S.Leaf) → (Sample Ω S → ℝ) → ℝ)
       (P : Finset C) (G : (C → FinitePath Ω n) → ℝ)
       (hG : ∀ x y, (∀ c ∈ P, x c = y c) → G x = G y)
       (cs : List C) (hdis : ∀ c ∈ cs, c ∉ P)
       (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf)
       (pos : C → S.Leaf) (f : Sample Ω S → ℝ) :
       labeledHistory m (fun R pos g => V R pos (fun x => g x * G (fun c => R.pathAt (pos c) x)))
         cs S U loc pos f =
       labeledHistory m V cs S U loc pos (fun x => f x*G (fun c => S.pathAt (pos c) x)) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.labeledHistory

2. theorem OAI.DilutedSpinGlass.PrescribedTree.matrixHistory_retained line 57

   Source documentation

   Complete-matrix normalization WITH any observable of the already assigned paths. Its joint dependence on the old test and the original samples is kept.

   theorem matrixHistory_retained (T : PrescribedTree n) (q : C → T.Leaf)
       (hq : Function.Injective q) (K : KernelTower Ω n) (m : Fin (n+1) → ℝ)
       (hm : StrictMono m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last n) = 1)
       (cs : List C) (hcs : cs.Nodup) (P : Finset C) (hP : P.Nonempty)
       (hdis : ∀ c ∈ cs, c ∉ P) (hfull : P ∪ cs.toFinset = Finset.univ)
       (G : (C → FinitePath Ω n) → ℝ)
       (hG : ∀ x y, (∀ c ∈ P, x c = y c) → G x = G y)
       (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf) (pos : C → S.Leaf)
       (hcover : HistoryCover S U loc P pos)
       (hsplit : ∀ a ∈ P, ∀ b ∈ P,
         splitDepth S (pos a) (pos b) = splitDepth T (q a) (q b))
       (f : Sample Ω S → ℝ) :
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.HistoryCover, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.Sample