MarkerNormalization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.all_old_history_cover line 13
lemma OAI.DilutedSpinGlass.PrescribedTree.marker_history_joint_ratio line 25

theorem OAI.DilutedSpinGlass.PrescribedTree.marker_history_joint line 78

Source documentation

The exact marker history coefficient is the anchor-alone kappa; this proof obtains the equality by normalization of the same histories, without an independent combinatorial simplification of kappa.

theorem marker_history_joint (S T Q : PrescribedTree n) (a : 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 e, splitDepth S d e=splitDepth Q (qold d) (qold e))
    (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 : 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) (hfull : cs.toFinset=Finset.univ)
    (F : (S.Leaf → FinitePath Ω n) → ℝ) (A : (Option C → FinitePath Ω n) → ℝ) :
…

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