-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
/-- The **Holley Inequality**. -/
lemma holley (hμ₀ : 0 ≤ μ) (hf : 0 ≤ f) (hg : 0 ≤ g) (hμ : Monotone μ)
    (hfg : ∑ a, f a = ∑ a, g a) (h : ∀ a b, f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)) :
    ∑ a, μ a * f a ≤ ∑ a, μ a * g a

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hg : 0 ≤ g
hμ : Monotone μ
hf : 0 ≤ 0
hfg : ∑ a : α, 0 a = ∑ a : α, g a
h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)
⊢ ∑ a : α, μ a * 0 a ≤ ∑ a : α, μ a * g a

Tactic:
simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg

Result:
case inl
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hg : 0 ≤ g
hμ : Monotone μ
hf : 0 ≤ 0
h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)
hfg : g = 0
⊢ ∑ a : α, μ a * 0 a ≤ ∑ a : α, μ a * g a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * g a

Tactic:
obtain rfl | hf := hf.eq_or_lt

Result:
case inl
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hg : 0 ≤ g
hμ : Monotone μ
hf : 0 ≤ 0
hfg : ∑ a : α, 0 a = ∑ a : α, g a
h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)
⊢ ∑ a : α, μ a * 0 a ≤ ∑ a : α, μ a * g a

case inr
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * g a

Proof state:
case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : 0 ≤ 0
hfg : ∑ a : α, f a = ∑ a : α, 0 a
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * 0 a

Tactic:
simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg

Result:
case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : 0 ≤ 0
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
hfg : f = 0
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * 0 a

Proof state:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))

Tactic:
rw [sup_comm, inf_comm]

Result:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (b ⊔ a) * (f (b ⊓ a) * g (b ⊔ a))

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hg : 0 ≤ g
hμ : Monotone μ
hf : 0 ≤ 0
h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)
hfg : g = 0
⊢ ∑ a : α, μ a * 0 a ≤ ∑ a : α, μ a * g a

Tactic:
simp [hfg]

Result:
no goals

Proof state:
case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
this : (∑ a : α, g a) * ∑ a : α, (μ * f) a ≤ (∑ a ∈ univ ⊼ univ, f a) * ∑ a ∈ univ ⊻ univ, (μ * g) a
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * g a

Tactic:
simpa [hfg, sum_pos hg] using this

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : 0 ≤ 0
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
hfg : f = 0
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * 0 a

Tactic:
simp [hfg]

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * g a

Tactic:
have := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
  (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_) univ univ

Result:
case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
this : (∑ a : α, g a) * ∑ a : α, (μ * f) a ≤ (∑ a ∈ univ ⊼ univ, f a) * ∑ a ∈ univ ⊻ univ, (μ * g) a
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * g a

case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)

Proof state:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (b ⊔ a) * (f (b ⊓ a) * g (b ⊔ a))

Tactic:
exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _

Result:
no goals

Proof state:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)

Tactic:
simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]

Result:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))