Submodular Set Functions and Marginal Gains

This module defines submodular set functions on Finset α and proves their fundamental algebraic properties ([NWF78], Section 2, Proposition 2.1):

1. Subtraction-free submodularity f (A ∪ B) + f (A ∩ B) ≤ f A + f B over any ordered commutative additive monoid (IsSubmodular).
2. Exact characterization via diminishing marginal returns (isSubmodular_iff_insert_add_le over cancellative ordered monoids such as ℕ, ℤ, ℚ, ℝ, and isSubmodular_iff_marginalGain_le over ordered additive groups).
3. Subadditivity of marginal gains across set differences and unions (IsSubmodular.sub_le_sum_marginalGain_sdiff and IsSubmodular.sub_le_sum_marginalGain_of_monotone), which drives the Nemhauser–Wolsey–Fisher (1 - 1/e) greedy analysis.
4. Closure under constants, addition, finite sums, natural scalar multiplication, and upper truncation min (f S) c (for monotone submodular f), together with modular sums and weighted set-coverage constructors.

Monotonicity reuses Mathlib's Monotone (A ⊆ B → f A ≤ f B) directly on Finset α.

Main definitions

• Cslib.Algorithms.Lean.Submodular.IsSubmodular: ∀ A B, f (A ∪ B) + f (A ∩ B) ≤ f A + f B.
• Cslib.Algorithms.Lean.Submodular.marginalGain: f (insert x S) - f S.
• Cslib.Algorithms.Lean.Submodular.modularSum: additive set function ∑ x ∈ S, w x.
• Cslib.Algorithms.Lean.Submodular.weightedCoverage: coverage function ∑ u ∈ S.biUnion cover, w u.

Main results

• isSubmodular_iff_insert_add_le, isSubmodular_iff_marginalGain_le: diminishing-returns characterizations of IsSubmodular.
• IsSubmodular.sub_le_sum_marginalGain_sdiff, IsSubmodular.sub_le_sum_marginalGain_of_monotone: upper bounds on f (S ∪ T) - f S and f T - f S via single-element marginal gains at S.
• IsSubmodular.add, isSubmodular_sum, IsSubmodular.nsmul, IsSubmodular.min_const: closure properties.
• isSubmodular_modularSum, isSubmodular_weightedCoverage: canonical submodular constructors.

References

• [NWF78] George L. Nemhauser, Laurence A. Wolsey, and Marshall L. Fisher, An Analysis of Approximations for Maximizing Submodular Set Functions—I, 1978.

Core definitions

def Cslib.Algorithms.Lean.Submodular.IsSubmodular {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [Preorder β] (f : Finset α → β) : Prop

A function f : Finset α → β is submodular if f (A ∪ B) + f (A ∩ B) ≤ f A + f B for all finite sets A, B. Stated without subtraction so it applies directly to ℕ-, ℚ-, and ℝ-valued functions alike.

def Cslib.Algorithms.Lean.Submodular.marginalGain {α : Type u_1} {β : Type u_2} [DecidableEq α] [Sub β] (f : Finset α → β) (S : Finset α) (x : α) : β

Marginal gain f (insert x S) - f S of adding x to S.

@[simp]

theorem Cslib.Algorithms.Lean.Submodular.marginalGain_empty_of_map_empty {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup β] {f : Finset α → β} (hf : f ∅ = 0) (x : α) : marginalGain f ∅ x = f {x}

@[simp]

theorem Cslib.Algorithms.Lean.Submodular.marginalGain_of_mem {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup β] {f : Finset α → β} {S : Finset α} {x : α} (hx : x ∈ S) : marginalGain f S x = 0

theorem Cslib.Algorithms.Lean.Submodular.marginalGain_nonneg_of_monotone {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : Finset α → β} (hmono : Monotone f) (S : Finset α) (x : α) : 0 ≤ marginalGain f S x

theorem Cslib.Algorithms.Lean.Submodular.nonneg_of_empty_nonneg_of_monotone {α : Type u_1} {β : Type u_2} [Preorder β] [Zero β] {f : Finset α → β} (hf0 : 0 ≤ f ∅) (hmono : Monotone f) (S : Finset α) : 0 ≤ f S

Diminishing marginal returns characterization

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.insert_add_le {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [Preorder β] {f : Finset α → β} (hf : IsSubmodular f) ⦃A B : Finset α⦄ (x : α) (hAB : A ⊆ B) (hx : x ∉ B) : f (insert x B) + f A ≤ f B + f (insert x A)

Forward diminishing returns (subtraction-free): if f is submodular, A ⊆ B, and x ∉ B, then f (insert x B) + f A ≤ f B + f (insert x A).

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.insert_add_le_of_monotone {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [Preorder β] [AddLeftMono β] {f : Finset α → β} (hf : IsSubmodular f) (hmono : Monotone f) ⦃A B : Finset α⦄ (x : α) (hAB : A ⊆ B) : f (insert x B) + f A ≤ f B + f (insert x A)

When f is also monotone, f (insert x B) + f A ≤ f B + f (insert x A) holds for every x without needing x ∉ B.

theorem Cslib.Algorithms.Lean.Submodular.isSubmodular_of_insert_add_le {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] {f : Finset α → β} (hdim : ∀ ⦃A B : Finset α⦄ (x : α), A ⊆ B → x ∉ B → f (insert x B) + f A ≤ f B + f (insert x A)) : IsSubmodular f

Converse of diminishing returns: if adding an element x ∉ B has smaller incremental effect on B than on any subset A ⊆ B, then f is submodular.

theorem Cslib.Algorithms.Lean.Submodular.isSubmodular_iff_insert_add_le {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] {f : Finset α → β} : IsSubmodular f ↔ ∀ ⦃A B : Finset α⦄ (x : α), A ⊆ B → x ∉ B → f (insert x B) + f A ≤ f B + f (insert x A)

Diminishing-Returns Characterization of Submodularity ([NWF78], Proposition 2.1), subtraction-free form valid over ℕ, ℤ, ℚ, and ℝ.

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.marginalGain_le {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : Finset α → β} (hf : IsSubmodular f) ⦃A B : Finset α⦄ (x : α) (hAB : A ⊆ B) (hx : x ∉ B) : marginalGain f B x ≤ marginalGain f A x

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.marginalGain_le_of_monotone {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : Finset α → β} (hf : IsSubmodular f) (hmono : Monotone f) ⦃A B : Finset α⦄ (x : α) (hAB : A ⊆ B) : marginalGain f B x ≤ marginalGain f A x

theorem Cslib.Algorithms.Lean.Submodular.isSubmodular_iff_marginalGain_le {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : Finset α → β} : IsSubmodular f ↔ ∀ ⦃A B : Finset α⦄ (x : α), A ⊆ B → x ∉ B → marginalGain f B x ≤ marginalGain f A x

Diminishing-Returns Characterization of Submodularity in terms of marginalGain over an ordered commutative group ([NWF78], Proposition 2.1).

Subadditivity of marginal gains over finite unions

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.sub_le_sum_marginalGain_sdiff {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : Finset α → β} (hf : IsSubmodular f) (S T : Finset α) : f (S ∪ T) - f S ≤ ∑ x ∈ T \ S, marginalGain f S x

For any submodular function f (not necessarily monotone) and finite sets S, T, f (S ∪ T) - f S ≤ ∑ x ∈ T \ S, marginalGain f S x ([NWF78], Proposition 2.1(v)).

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.sub_le_sum_marginalGain_of_monotone {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : Finset α → β} (hf : IsSubmodular f) (hmono : Monotone f) (S T : Finset α) : f T - f S ≤ ∑ x ∈ T \ S, marginalGain f S x

Monotone Submodular Marginal-Gain Bound ([NWF78], Section 2, Proposition 2.2(iv')): for monotone submodular f and any S, T : Finset α, f T - f S ≤ ∑ x ∈ T \ S, marginalGain f S x.

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.sub_le_sum_marginalGain_full_of_monotone {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : Finset α → β} (hf : IsSubmodular f) (hmono : Monotone f) (S T : Finset α) : f T - f S ≤ ∑ x ∈ T, marginalGain f S x

Variant summing over all of T (elements in T ∩ S contribute 0).

Closure properties and canonical constructors

theorem Cslib.Algorithms.Lean.Submodular.isSubmodular_const {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [Preorder β] (c : β) : IsSubmodular fun (x : Finset α) => c

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.add {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] {f g : Finset α → β} (hf : IsSubmodular f) (hg : IsSubmodular g) : IsSubmodular fun (S : Finset α) => f S + g S

theorem Cslib.Algorithms.Lean.Submodular.isSubmodular_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (s : Finset ι) {g : ι → Finset α → β} (hg : ∀ i ∈ s, IsSubmodular (g i)) : IsSubmodular fun (S : Finset α) => ∑ i ∈ s, g i S

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.nsmul {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] {f : Finset α → β} (hf : IsSubmodular f) (n : ℕ) : IsSubmodular fun (S : Finset α) => n • f S

theorem Cslib.Algorithms.Lean.Submodular.monotone_min_const {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : Finset α → β} (hmono : Monotone f) (c : β) : Monotone fun (S : Finset α) => min (f S) c

Truncating a monotone function above at a constant c (fun S => min (f S) c) preserves monotonicity.

theorem Cslib.Algorithms.Lean.Submodular.IsSubmodular.min_const {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] {f : Finset α → β} (hf : IsSubmodular f) (hmono : Monotone f) (c : β) : IsSubmodular fun (S : Finset α) => min (f S) c

Truncating a monotone submodular function above at a constant c (fun S => min (f S) c) preserves submodularity.

def Cslib.Algorithms.Lean.Submodular.modularSum {α : Type u_1} {β : Type u_2} [AddCommMonoid β] (w : α → β) (S : Finset α) : β

Modular (additive) set function ∑ x ∈ S, w x.

@[simp]

theorem Cslib.Algorithms.Lean.Submodular.modularSum_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid β] (w : α → β) : modularSum w ∅ = 0

theorem Cslib.Algorithms.Lean.Submodular.modularSum_union_add_inter {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] (w : α → β) (A B : Finset α) : modularSum w (A ∪ B) + modularSum w (A ∩ B) = modularSum w A + modularSum w B

theorem Cslib.Algorithms.Lean.Submodular.isSubmodular_modularSum {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommMonoid β] [Preorder β] (w : α → β) : IsSubmodular (modularSum w)

theorem Cslib.Algorithms.Lean.Submodular.monotone_modularSum {α : Type u_1} {β : Type u_2} [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {w : α → β} (hw : ∀ (x : α), 0 ≤ w x) : Monotone (modularSum w)

def Cslib.Algorithms.Lean.Submodular.weightedCoverage {α : Type u_1} {U : Type u_2} {β : Type u_3} [DecidableEq U] [AddCommMonoid β] (cover : α → Finset U) (w : U → β) (S : Finset α) : β

Weighted set-coverage function ∑ u ∈ S.biUnion cover, w u.

@[simp]

theorem Cslib.Algorithms.Lean.Submodular.weightedCoverage_empty {α : Type u_1} {U : Type u_2} {β : Type u_3} [DecidableEq U] [AddCommMonoid β] (cover : α → Finset U) (w : U → β) : weightedCoverage cover w ∅ = 0

theorem Cslib.Algorithms.Lean.Submodular.monotone_weightedCoverage {α : Type u_1} {U : Type u_2} {β : Type u_3} [DecidableEq U] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] (cover : α → Finset U) {w : U → β} (hw : ∀ (u : U), 0 ≤ w u) : Monotone (weightedCoverage cover w)

theorem Cslib.Algorithms.Lean.Submodular.isSubmodular_weightedCoverage {α : Type u_1} {U : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq U] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] (cover : α → Finset U) {w : U → β} (hw : ∀ (u : U), 0 ≤ w u) : IsSubmodular (weightedCoverage cover w)

Nonnegative weighted set coverage is submodular.