OAI/Probability/DilutedSpin/TerminalMarginal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.FiniteLaw.expMoment_bind_one line 10
2. lemma OAI.DilutedSpinGlass.FiniteLaw.logMean_bind_one_congr line 24
3. lemma OAI.DilutedSpinGlass.KernelTower.terminal_marginal_congr line 39

   Source documentation

   Equality of the genuine final-spin marginal propagates through every auxiliary conditional power mean. The only required endpoint is m_L=1.

   lemma terminal_marginal_congr (L : ℕ) (a : Ω) (b : Λ) (P : FiniteLaw Ω) (R : FiniteLaw Λ)
       (U : KernelTower A (L+1)) (m : Fin (L+1) → ℝ) (hm : m (Fin.last L)=1)
       (F : Ω → FinitePath A (L+1) → ℝ) (G : Λ → FinitePath A (L+1) → ℝ)
       (h : ∀ y, P.expMoment 1 (fun s => F s y) = R.expMoment 1 (fun s => G s y)) :
       backwardLog (L+1) (prod (L+1) (terminalTower a P L) U) m
         (fun y => F (terminalState L (pathFst (L+1) y)) (pathSnd (L+1) y)) =
       backwardLog (L+1) (prod (L+1) (terminalTower b R L) U) m
         (fun y => G (terminalState L (pathFst (L+1) y)) (pathSnd (L+1) y)) := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.backwardLog, OAI.DilutedSpinGlass.KernelTower.prod, OAI.DilutedSpinGlass.KernelTower.terminalTower, OAI.DilutedSpinGlass.KernelTower.terminalState, OAI.DilutedSpinGlass.KernelTower.pathFst, OAI.DilutedSpinGlass.KernelTower.pathSnd