MarkerHistory.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory_drop_available line 16

Source documentation

If every requested new color has a different split from a protected marker than every available old leaf, the old choices vanish in the literal signed history. Fresh extensions retain this exclusion.

theorem weightedMatrixHistory_drop_available (T : PrescribedTree n) (q : C → T.Leaf)
    (V : (R : PrescribedTree n) → (C → R.Leaf) → (Sample Ω R → ℝ) → ℝ)
    (m : Fin (n+1) → ℝ) (a : C) (cs : List C) (hcs : cs.Nodup) (ha : a ∉ cs)
    (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf) (pos : C → S.Leaf)
    (hsep : ∀ c ∈ cs, ∀ i ∈ U,
      splitDepth S (loc i) (pos a) ≠ splitDepth T (q c) (q a))
    (f : Sample Ω S → ℝ) :
    weightedMatrixHistory T q V m cs S U loc pos f =
      weightedMatrixHistory T q V m cs S ∅ loc pos f := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory

theorem OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory_protected_one line 56

Source documentation

General complete-matrix normalization with a whole protected old tree. All paths, including those used by an old observable, are jointly retained.

theorem weightedMatrixHistory_protected_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)
    (cs : List C) (hcs : cs.Nodup) (P : Finset C) (hP : P.Nonempty)
    (hdis : ∀ c ∈ cs, c ∉ P) (hfull : P ∪ cs.toFinset=Finset.univ)
    (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))
    (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)))
…

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

theorem OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_congr_protected_split line 96

Source documentation

Split relations among colors which are never reassigned survive all old and fresh extensions. This transports an exact terminal identity through the actual signed expansion.

theorem labeledHistory_congr_protected_split (m : Fin (n+1) → ℝ)
    (V W : (R : PrescribedTree n) → (C → R.Leaf) → (Sample Ω R → ℝ) → ℝ)
    (P : Finset C) (B : C → C → ℕ)
    (h : ∀ R pos, (∀ a ∈ P, ∀ b ∈ P, splitDepth R (pos a) (pos b)=B a b) →
      ∀ g, V R pos g=W R pos g)
    (cs : List C) (hdis : ∀ c ∈ cs, c ∉ P)
    (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf) (pos : C → S.Leaf)
    (hsplit : ∀ a ∈ P, ∀ b ∈ P, splitDepth S (pos a) (pos b)=B a b)
    (f : Sample Ω S → ℝ) :
    labeledHistory m V cs S U loc pos f=labeledHistory m W cs S U loc pos f := by
…

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