OAI/Probability/DilutedSpin/PhysicalScheduledMultileaf.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.ReducedTopology.physical_scheduled_root_multileaf line 24

   Source documentation

   Actual physical-root multileaf induction, with ALL ordinary integrability premises discharged for finite alphabets and countably many marker types. The signed root covariance remains a single centered term, not a pointwise absolute value. This is a dependency of decorrelation, not the main formula.

   theorem physical_scheduled_root_multileaf (μ : 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