PhysicalMultileafMoments.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.ReducedTopology.physical_scheduled_root_multileaf_moments line 21

Source documentation

Root-moment form of the genuine multileaf induction. Projection costs are now functions of the ROOT conditional covariance of proper children; there are no caller integrability or projection-error hypotheses.

theorem physical_scheduled_root_multileaf_moments (μ : Measure (FullRootState Y X J M))
    [IsProbabilityMeasure μ]
    (H r d : ℕ) (k : ℕ+) (hk : 2≤(k:ℕ)) (a : α) (C : Fin k → ReducedTopology)
    (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
    (Q : α → Fin (H+1+1+r+1+d)) (ha : (Q a).val=r+1+d)
    (hQ : ∀ j v, (Q a).val+1≤(Q (e j v)).val)
    (T : KernelTower Ω (H+1+1+r+1+d)) (P : (j : J) → Fin (H+1+1+r+1+d) → FiniteLaw (Mark j))
    (m : Fin (H+1+1+r+1+d) → ℝ)
    (base : RootPath Y M → (k : ℕ) → RootPath X k → FinitePath Ω (H+1+1+r+1+d) → ℝ)
    (old : (j : J) → FinitePath Ω (H+1+1+r+1+d) → FinitePath (Mark j) (H+1+1+r+1+d) → ℝ)
    (V : FinitePath Ω (H+1+1+r+1+d) → Fin N → ℝ)
    (hb : ∀ k y, Measurable (fun z : RootPath Y M × RootPath X k => base z.1 k z.2 y))
…

Mentions: OAI.DilutedSpinGlass.FullRootState, OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.FinitePath