Theorems · Theorem · order theory

holley

∀ {α : 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 μ →
          ∑ a, f a = ∑ a, g a → (∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)) → ∑ a, μ a * f a ≤ ∑ a, μ a * g a

The Holley Inequality.

Defined in

Mathlib.Combinatorics.SetFamily.FourFunctions

Cited by

0 results in Mathlib

Foundations

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

Assumes

DistribLatticeCommSemiringLinearOrderIsStrictOrderedRingExistsAddOfLEFintype