English
As part of the Four Functions framework, a higher-level theorem is stated: Finset.four_functions_theorem provides the finite distributive lattice generalization of the inequality, with a corollary that the standard finite Four Functions theorem holds in the powerset algebra.
Русский
В рамках теоремы Four Functions дано обобщение в конечной решётке; выводы включают частные случаи в алгебре степеней \(P(X)\).
LaTeX
$$FourFunctions theorem$$
Lean4
/-- The **Four Functions Theorem** on a powerset algebra. See `four_functions_theorem` for the
finite distributive lattice generalisation. -/
protected theorem four_functions_theorem (u : Finset α) (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
(h : ∀ ⦃s⦄, s ⊆ u → ∀ ⦃t⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) {𝒜 ℬ : Finset (Finset α)}
(h𝒜 : 𝒜 ⊆ u.powerset) (hℬ : ℬ ⊆ u.powerset) :
(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s := by
induction u using Finset.induction generalizing f₁ f₂ f₃ f₄ 𝒜 ℬ with
| empty =>
simp only [Finset.powerset_empty, Finset.subset_singleton_iff] at h𝒜 hℬ
obtain rfl | rfl := h𝒜 <;> obtain rfl | rfl := hℬ <;> simp; exact h (subset_refl ∅) subset_rfl
| insert a u hu
ih =>
specialize
ih (collapse_nonneg h₁) (collapse_nonneg h₂) (collapse_nonneg h₃) (collapse_nonneg h₄)
(collapse_modular hu h₁ h₂ h₃ h₄ h 𝒜 ℬ) Subset.rfl Subset.rfl
have : 𝒜 ⊼ ℬ ⊆ powerset (insert a u) := by simpa using infs_subset h𝒜 hℬ
have : 𝒜 ⊻ ℬ ⊆ powerset (insert a u) := by simpa using sups_subset h𝒜 hℬ
simpa only [powerset_sups_powerset_self, powerset_infs_powerset_self, sum_collapse, not_false_eq_true, *] using ih
