OAI/Probability/DilutedSpin/ProductComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_pi_comparison line 11

   Source documentation

   Replacing each independent coordinate with a law that decreases every conditional expectation decreases the full product expectation.

   lemma expect_pi_comparison {α : Type} [Fintype α] [Nonempty α] (k : ℕ)
       (P Q : Fin k → FiniteLaw α) (F : (Fin k → α) → ℝ)
       (h : ∀ (i : Fin k) (x : Fin k → α),
         (P i).expect (fun a => F (Function.update x i a)) ≤
           (Q i).expect (fun a => F (Function.update x i a))) :
       (pi P).expect F ≤ (pi Q).expect F := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.expect, OAI.DilutedSpinGlass.FiniteLaw.pi