Submodular functions on lattices

This file defines submodularity for functions on lattices and establishes its elementary closure properties. It also proves that the minimizers of a submodular function over a sublattice form a sublattice, and that symmetric submodular functions are posimodular. These are the order-theoretic inputs for lattices of minimum cuts and for uncrossing them, independently of any particular graph or network representation.

Main declarations

• TauCeti.IsSubmodular: the submodular inequality on a lattice.
• TauCeti.IsSymmSubmodular: a symmetric submodular function on a Boolean algebra.
• TauCeti.IsSubmodular.add: sums of submodular functions are submodular.
• TauCeti.IsSubmodular.comp_latticeHom: precomposition by a lattice homomorphism preserves submodularity.
• TauCeti.isSubmodular_finsetSum: summing fixed vertex weights over a finite set is submodular.
• TauCeti.IsSubmodular.isMinOn_sup_inf: uncrossing two minimizers by join and meet.
• TauCeti.IsSubmodular.isSublattice_minimizers: minimizers over a sublattice form a sublattice.
• TauCeti.IsSymmSubmodular.sdiff_add_sdiff_le: the posimodular inequality.

def TauCeti.IsSubmodular {K : Type u_1} {L : Type u_2} [Add K] [LE K] [Lattice L] (f : L → K) : Prop

A function on a lattice is submodular if its values at a join and a meet sum to at most the sum of its values at the original pair.

structure TauCeti.IsSymmSubmodular {K : Type u_1} {L : Type u_2} [Add K] [LE K] [BooleanAlgebra L] (f : L → K) : Prop

A function on a Boolean algebra is symmetric submodular if it is invariant under taking complements and is submodular. Symmetry is additional data: the submodular theory itself does not require it.

• symm (a : L) : f aᶜ = f a

  An element and its complement have the same value.

• submodular : IsSubmodular f

  The set function satisfies the submodular inequality.

theorem TauCeti.isSubmodular_def {K : Type u_1} {L : Type u_2} [Add K] [LE K] [Lattice L] (f : L → K) : IsSubmodular f ↔ ∀ (a b : L), f (a ⊔ b) + f (a ⊓ b) ≤ f a + f b

A function is submodular exactly when it satisfies the submodular inequality at every pair.

theorem TauCeti.isSubmodular_const {K : Type u_1} {L : Type u_2} [Add K] [Preorder K] [Lattice L] (c : K) : IsSubmodular fun (x : L) => c

A constant function on a lattice is submodular.

theorem TauCeti.isSubmodular_finsetSum {K : Type u_1} {V : Type u_4} [DecidableEq V] [AddCommMonoid K] [Preorder K] (f : V → K) : IsSubmodular fun (S : Finset V) => ∑ v ∈ S, f v

The sum of fixed weights over a finite set is submodular. In fact, its submodular inequality is always an equality.

theorem TauCeti.IsSubmodular.apply {K : Type u_1} {L : Type u_2} [Add K] [LE K] [Lattice L] {f : L → K} (hf : IsSubmodular f) (a b : L) : f (a ⊔ b) + f (a ⊓ b) ≤ f a + f b

Extract the submodular inequality at a pair of lattice elements.

theorem TauCeti.IsSubmodular.add {K : Type u_1} {L : Type u_2} [AddCommMonoid K] [Preorder K] [IsOrderedAddMonoid K] [Lattice L] {f g : L → K} (hf : IsSubmodular f) (hg : IsSubmodular g) : IsSubmodular fun (a : L) => f a + g a

The pointwise sum of two submodular functions is submodular.

theorem TauCeti.IsSubmodular.comp_latticeHom {K : Type u_1} {L : Type u_2} {M : Type u_3} [Add K] [LE K] [Lattice L] [Lattice M] {f : L → K} (hf : IsSubmodular f) (g : LatticeHom M L) : IsSubmodular (f ∘ ⇑g)

Precomposition with a lattice homomorphism preserves submodularity.

theorem TauCeti.IsSubmodular.isMinOn_sup_inf {K : Type u_1} {L : Type u_2} [AddCommMonoid K] [Preorder K] [IsOrderedCancelAddMonoid K] [Lattice L] {f : L → K} (hf : IsSubmodular f) {s t : Set L} {a b : L} (hamin : IsMinOn f s a) (hbmin : IsMinOn f t b) (hsup : a ⊔ b ∈ t) (hinf : a ⊓ b ∈ s) : IsMinOn f t (a ⊔ b) ∧ IsMinOn f s (a ⊓ b)

Let a minimize a submodular function over s and b minimize it over t. If the meet lies in s and the join lies in t, then the join minimizes over t and the meet minimizes over s.

theorem TauCeti.IsSubmodular.isSublattice_minimizers {K : Type u_1} {L : Type u_2} [AddCommMonoid K] [Preorder K] [IsOrderedCancelAddMonoid K] [Lattice L] {f : L → K} (hf : IsSubmodular f) {s : Set L} (hs : IsSublattice s) : IsSublattice {a : L | a ∈ s ∧ IsMinOn f s a}

The minimizers of a submodular function over a sublattice form a sublattice. Membership in this set records both membership in the original domain and minimality there.

theorem TauCeti.IsSymmSubmodular.sdiff_add_sdiff_le {K : Type u_1} {L : Type u_2} [AddCommSemigroup K] [LE K] [BooleanAlgebra L] {f : L → K} (hf : IsSymmSubmodular f) (a b : L) : f (a \ b) + f (b \ a) ≤ f a + f b

The posimodular inequality: a symmetric submodular function also satisfies the submodular inequality with the two differences in place of the join and meet.