OAI/Probability/DilutedSpin/MatrixNormalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PrescribedTree.splitOn_pick_old line 15
2. lemma OAI.DilutedSpinGlass.PrescribedTree.splitOn_pick_fresh line 35
3. theorem OAI.DilutedSpinGlass.PrescribedTree.matrixHistory_normalization line 61

   Source documentation

   Exact normalization of the ACTUAL complete-matrix protected history, retaining an arbitrary old test. This bridges the analytic history to the unordered kappa product, without assuming a reference-history identity.

   theorem matrixHistory_normalization (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)
       (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 → ℝ) :
       matrixHistory T q K m cs S U loc pos f =
         (partialKappa T m (Finset.univ.image q) / partialKappa T m (P.image q)) *
   …

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

4. def OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory line 144

   Source documentation

   A complete-matrix history with a general terminal observable. The full ordered old-erase/fresh-grow history remains literal.

   noncomputable def weightedMatrixHistory (T : PrescribedTree n) (q : C → T.Leaf)
       (V : (R : PrescribedTree n) → (C → R.Leaf) → (Sample Ω R → ℝ) → ℝ)
       (m : Fin (n+1) → ℝ) (cs : List C)
       (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf)
       (pos : C → S.Leaf) (f : Sample Ω S → ℝ) : ℝ :=
   …

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

5. lemma OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory_mismatch line 156

   Source documentation

   Once two assigned colors have the wrong split, no future legal extension can repair it. This justifies enforcing the matrix constraints successively.

   lemma weightedMatrixHistory_mismatch (T : PrescribedTree n) (q : C → T.Leaf)
       (V : (R : PrescribedTree n) → (C → R.Leaf) → (Sample Ω R → ℝ) → ℝ) (m : Fin (n+1) → ℝ) (cs : List C)
       (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf)
       (pos : C → S.Leaf) (f : Sample Ω S → ℝ)
       (a b : C) (ha : a ∉ cs) (hb : b ∉ cs)
       (he : splitDepth S (pos a) (pos b) ≠ splitDepth T (q a) (q b)) :
       weightedMatrixHistory T q V m cs S U loc pos f = 0 := by
   …

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

6. theorem OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory_step line 193

   Source documentation

   Exact sequential enforcement of the full split matrix inside the protected signed history. Impossible branches vanish, rather than being silently dropped or replaced by a reference law.

   theorem weightedMatrixHistory_step (T : PrescribedTree n) (q : C → T.Leaf)
       (V : (R : PrescribedTree n) → (C → R.Leaf) → (Sample Ω R → ℝ) → ℝ) (m : Fin (n+1) → ℝ) (c : C) (cs : List C)
       (P : Finset C) (hc : c ∉ P) (hdis : ∀ d ∈ cs, d ∉ insert c P)
       (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf)
       (pos : C → S.Leaf) (f : Sample Ω S → ℝ) :
       weightedMatrixHistory T q V m (c::cs) S U loc pos f =
       (∑ i ∈ U, if ∀ d ∈ P, splitDepth S (loc i) (pos d) = splitDepth T (q c) (q d)
         then weightedMatrixHistory T q V m cs S (U.erase i) loc (Function.update pos c (loc i)) f else 0) +
       ∑ v : S.Internal, if ∀ d ∈ P, freshSplitDepth S v (pos d) = splitDepth T (q c) (q d)
         then gamma S m v * weightedMatrixHistory T q V m cs (grow S v) U
           (fun i => oldLeaf S v (loc i))
           (Function.update (fun d => oldLeaf S v (pos d)) c (newLeaf S v))
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldLeaf, OAI.DilutedSpinGlass.PrescribedTree.newLeaf