Theorems · Theorem · order theory

fkg

∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] [ExistsAddOfLE β] (f g μ : α → β) [inst_5 : Fintype α],
  0 ≤ μ →
    0 ≤ f →
      0 ≤ g →
        Monotone f →
          Monotone g →
            (∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)) →
              (∑ a, μ a * f a) * ∑ a, μ a * g a ≤ (∑ a, μ a) * ∑ a, μ a * (f a * g a)

The Fortuin-Kasteleyn-Ginibre Inequality.

Defined in

Mathlib.Combinatorics.SetFamily.FourFunctions

Cited by

0 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DistribLatticeCommSemiringLinearOrderIsStrictOrderedRingExistsAddOfLEFintype