InformationTheory.Polymatroid.Basic

Imports 6

Polymatroid #

A polymatroid is a finite ground set together with a real-valued rank function on its subsets satisfying three axioms (empty, monotone, submodular).

Mathlib does not (yet) carry a set-function Polymatroid / Submodular structure (Matroid rank exists at ℕ∞-value, see Mathlib.Combinatorics.Matroid.Rank.ENat); this file introduces the ℝ-valued set-function version, mirroring the field style of Mathlib.Combinatorics.Matroid.Basic.

The canonical example is the joint entropy of a finite collection of random variables (InformationTheory.Shannon.entropyPolymatroid in InformationTheory/Shannon/Polymatroid.lean).

structure

Combinatorics.Polymatroid

source

(ι : Type u_1) [DecidableEq ι] :

Type u_1

A polymatroid is a finite ground set ι together with a real-valued rank function on Finset ι satisfying:

rank ∅ = 0 — the empty set has rank 0,
Monotone rank — rank is monotone in the subset relation,
submodularity — rank (S ∪ T) + rank (S ∩ T) ≤ rank S + rank T.

The ground set type ι only needs [DecidableEq ι] (for Finset union / intersection); finiteness of ι itself is not required.

rank : Finset ι → ℝ
The real-valued rank function on subsets of the ground set.
rank_empty : self.rank ∅ = 0
The rank of the empty set is zero.
rank_mono : Monotone self.rank
The rank function is monotone in the subset relation.
rank_submodular(S T : Finset ι) : self.rank (S ∪ T) + self.rank (S ∩ T) ≤ self.rank S + self.rank T
The rank function is submodular.

Instances For

Used by

theorem

Combinatorics.Polymatroid.ext_iff

source

realized by @[ext] from Combinatorics.Polymatroid.ext

{ι : Type u_1} {inst✝ : DecidableEq ι} {x y : Polymatroid ι} :

x = y ↔ x.rank = y.rank

Used by

theorem

Combinatorics.Polymatroid.ext

source

realized by @[ext] from Combinatorics.Polymatroid

{ι : Type u_1} {inst✝ : DecidableEq ι} {x y : Polymatroid ι} (rank : x.rank = y.rank) :

x = y

Used by