OAI/Probability/DilutedSpin/RootMultileafMatrix.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DilutedSpinGlass.UniversalDictionary.Labels line 16
  2. def OAI.DilutedSpinGlass.UniversalDictionary.rootHistory line 18
  3. lemma OAI.DilutedSpinGlass.UniversalDictionary.rootHistory_polarization line 30
  4. def OAI.DilutedSpinGlass.UniversalDictionary.historyAverage line 59
  5. def OAI.DilutedSpinGlass.UniversalDictionary.historyCovariance line 64
  6. lemma OAI.DilutedSpinGlass.UniversalDictionary.historyAverage_polarization line 76
  7. lemma OAI.DilutedSpinGlass.UniversalDictionary.historyCovariance_polarization line 107
  8. lemma OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError_treeOverlap line 136

    Source documentation

    Exact conversion of the color-indexed matrix projection to the old all-leaf projection error in the SAME sampled tree.

    lemma matrixProjectionError_treeOverlap (S : PrescribedTree n)
    (q : I → S.Leaf) (hq : Function.Bijective q) (T : KernelTower Ω n)
    (a c : I) (f X : FinitePath Ω n → Fin N → ℝ) :
    matrixProjectionError S q T a c (spatialProduct (fun _ : I => f)) X=
      oldProjectionError S T (q a) (q c) (treeOverlap S f) X := by
…

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError, OAI.DilutedSpinGlass.PrescribedTree.spatialProduct, OAI.DilutedSpinGlass.PrescribedTree.oldProjectionError, OAI.DilutedSpinGlass.PrescribedTree.treeOverlap

  9. theorem OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError_prefixed_le line 154

    Source documentation

    The target's actual own-projector error, for arbitrary initial prefix and later first split, is controlled only by genuine proper children.

    theorem matrixProjectionError_prefixed_le (k : ℕ+) (C : Fin k → PrescribedTree n)
    (b : (PrescribedTree.node k C).Leaf) (r d : ℕ)
    (q : I → (splitFrame (.node k C) r d).Leaf) (hq : Function.Bijective q)
    (T : KernelTower Ω (n+1+r+1+d)) (a c : I)
    (ha : q a=splitFrameLeaf (.node k C) r d 0 b)
    (hc : q c=splitFrameLeaf (.node k C) r d 1 b)
    (f : FinitePath Ω (n+1+r+1+d) → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
    matrixProjectionError (splitFrame (.node k C) r d) q T a c
      (spatialProduct (fun _ : I => f))
      (fun x i => splitProjector (.node k C) r d T (fun y => f y i) x) ≤
       2*Real.sqrt ((k:ℝ)*∑ i, Real.sqrt (descendantEnergyAt (C i) r d T f)) := by
…

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.splitFrame, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.splitFrameLeaf, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError, OAI.DilutedSpinGlass.PrescribedTree.spatialProduct, OAI.DilutedSpinGlass.PrescribedTree.splitProjector, OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt

  10. theorem OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError_prefixed_change_le line 172

    Source documentation

    The actual target-side shifted projection error splits into proper-child covariances and a single-path squared-norm comparison. This includes every prefix and never asks for independent target leaves after marginalizing.

    theorem matrixProjectionError_prefixed_change_le (k : ℕ+) (C : Fin k → PrescribedTree n)
    (b : (PrescribedTree.node k C).Leaf) (r d : ℕ)
    (q : I → (splitFrame (.node k C) r d).Leaf) (hq : Function.Bijective q)
    (T : KernelTower Ω (n+1+r+1+d)) (a c : I)
    (ha : q a=splitFrameLeaf (.node k C) r d 0 b)
    (hc : q c=splitFrameLeaf (.node k C) r d 1 b)
    (f X : FinitePath Ω (n+1+r+1+d) → Fin N → ℝ)
    (hf : ∀ x i, |f x i|≤1) (hX : ∀ x i, |X x i|≤1) :
    matrixProjectionError (splitFrame (.node k C) r d) q T a c
      (spatialProduct (fun _ : I => f)) X ≤
       2*Real.sqrt ((k:ℝ)*∑ i, Real.sqrt (descendantEnergyAt (C i) r d T f))+
       2*Real.sqrt ((KernelTower.law (n+1+r+1+d) T).expect (fun x => FiniteLaw.spatialSq (fun i =>
…

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.splitFrame, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.splitFrameLeaf, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError, OAI.DilutedSpinGlass.PrescribedTree.spatialProduct, OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt, OAI.DilutedSpinGlass.KernelTower.law, OAI.DilutedSpinGlass.FiniteLaw.spatialSq

  11. theorem OAI.DilutedSpinGlass.PrescribedTree.root_multileaf_matrix line 206

    Source documentation

    The entire multileaf covariance, after averaging the genuine root law, is controlled by the SAME signed centered matrix history and the literal proper-child covariances. No conditional concentration is assumed.

    theorem root_multileaf_matrix {Z : Type} [MeasurableSpace Z] (μ : Measure Z)
    [IsProbabilityMeasure μ] (Ω : Z → Type) [∀ z, Fintype (Ω z)]
    (k : ℕ+) (C : Fin k → PrescribedTree n) (b : (PrescribedTree.node k C).Leaf) (r d : ℕ)
    (Target : PrescribedTree (n+1+r+1+d)) (q : I → Target.Leaf) (hq : Function.Bijective q)
    (Q : Finset ℕ) (hS : branchingCount (splitFrame (.node k C) r d) (· ∈ Q)=0)
    (K : (z : Z) → KernelTower (Ω z) (n+1+r+1+d)) (a c : I) (hac : a≠c)
    (cs : List I) (hcs : cs.Nodup) (hdis : ∀ j ∈ cs, j ∉ insert c ({a}:Finset I))
    (hfull : insert c ({a}:Finset I) ∪ cs.toFinset=Finset.univ)
    (hqd : splitDepth Target (q a) (q c)=d)
    (f : (z : Z) → FinitePath (Ω z) (n+1+r+1+d) → Fin N → ℝ) (hf : ∀ z x i, |f z x i| ≤ 1) :
    let L := n+1+r+1+d
…

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.splitFrame, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.FinitePath