OAI/Probability/DilutedSpin/MarkerRootIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.PrescribedTree.marker_root_covariance line 16

   Source documentation

   A marker identity controls the covariance of two whole overlaps, not just a selected coordinate or a conditional covariance. All constants and both actual finite-tree marginals are explicitly retained.

   theorem marker_root_covariance (μ : Measure Z) (Ω : Z → Type) [∀ z, Fintype (Ω z)]
       (S T Q : PrescribedTree n) (a : S.Leaf) (e : C ≃ S.Leaf)
       (q : Option C → T.Leaf) (hq : Function.Bijective q)
       (qold : S.Leaf → Q.Leaf) (qfresh : C → Q.Leaf)
       (hqQ : Function.Bijective (Sum.elim qold qfresh))
       (hold : ∀ d b, splitDepth S d b=splitDepth Q (qold d) (qold b))
       (hfresh : ∀ c d, splitDepth S (e c) (e d)=splitDepth Q (qfresh c) (qfresh d))
       (hmarker : ∀ x y, splitDepth T (q x) (q y)=
         splitDepth Q (Option.elim' (qold a) qfresh x) (Option.elim' (qold a) qfresh y))
       (hsep : ∀ c d, splitDepth Q (qfresh c) (qold a)<splitDepth Q (qold a) (qold d))
       (K : (z : Z) → KernelTower (Ω z) n) (m : Fin (n+1) → ℝ)
       (hm : StrictMono m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last n)=1)
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.KernelTower