Families of objects

Families of objects (Section 1.5 of the FEU paper): a common framework for spanning trees, paths, cuts, etc., each identified with its usage vector.

Everything here is stated over ℝ≥0: Density E := E → ℝ≥0 has no subtraction, only the semiring/convexity/(intrinsic ℝ≥0-Pi) topological structure needed for Adm, Equivalent, and FulkersonDual. The companion coercion into E → ℝ (needed to bring in real-analysis machinery like Krein-Milman) lives in LeanModulus.Common.ToReal; anything that actually needs that coercion belongs there instead of here.

@[reducible, inline]

abbrev FamilyOfObjects (E : Type u_1) : Type u_1

A family of objects on an edge type E: a set of usage vectors γ : E → ℝ≥0, one for each object (spanning tree, path, cut, etc.) in the family.

Equations

• FamilyOfObjects E = Set (E → NNReal)

def FamilyOfObjects.NoZeroObject {E : Type u_1} (Γ : FamilyOfObjects E) : Prop

Every object in Γ has positive usage on at least one edge. This rules out the trivial all-zero object, against which no density could ever be admissible.

Equations

• Γ.NoZeroObject = ∀ γ ∈ Γ, γ ≠ 0

@[reducible, inline]

abbrev Density (E : Type u_1) : Type u_1

A density on the edge type E assigns a nonnegative cost to each edge.

Equations

• Density E = (E → NNReal)

noncomputable def Density.length {E : Type u_1} (ρ : Density E) (γ : E → NNReal) : NNReal

The length of an object γ with respect to a density ρ is the total cost it incurs: ∑ e, γ e * ρ e. We use finsum (rather than Finset.sum over Finset.univ) so that this doesn't need a Fintype E instance, only Finite E.

Equations

• ρ.length γ = ∑ᶠ (e : E), γ e * ρ e

theorem Density.length_add {E : Type u_1} [Finite E] (ρ₁ ρ₂ : Density E) (γ : E → NNReal) : (ρ₁ + ρ₂).length γ = ρ₁.length γ + ρ₂.length γ

The length with respect to the sum of two densities is the sum of the lengths.

theorem Density.length_smul {E : Type u_1} (ρ : Density E) (c : NNReal) (γ : E → NNReal) : (c • ρ).length γ = c * ρ.length γ

The length with respect to a scalar multiple of a density is the scalar multiple of the length.

def Density.IsAdmissible {E : Type u_1} (ρ : Density E) (Γ : FamilyOfObjects E) : Prop

A density ρ is admissible for a family Γ if every object in Γ has length at least 1 with respect to ρ.

Equations

• ρ.IsAdmissible Γ = ∀ γ ∈ Γ, 1 ≤ ρ.length γ

theorem Density.continuous_length {E : Type u_1} [Finite E] (γ : E → NNReal) : Continuous fun (ρ : Density E) => ρ.length γ

The length function is continuous (in the topology of densities).

def FamilyOfObjects.Adm {E : Type u_1} (Γ : FamilyOfObjects E) : Set (Density E)

The admissible set of a family Γ: all densities admissible for it.

Equations

• Γ.Adm = {ρ : Density E | ρ.IsAdmissible Γ}

theorem FamilyOfObjects.convex_adm {E : Type u_1} [Finite E] (Γ : FamilyOfObjects E) : Convex NNReal Γ.Adm

The admissible set Adm(Γ)of a family Γ is convex.

theorem FamilyOfObjects.isClosed_adm {E : Type u_1} [Finite E] (Γ : FamilyOfObjects E) : IsClosed Γ.Adm

The admissible set Adm(Γ)of a family Γ is closed.

def FamilyOfObjects.Equivalent {E : Type u_1} (Γ Γ' : FamilyOfObjects E) : Prop

Two families of objects are equivalent if they have the same admissible set, i.e. they impose exactly the same constraints on densities. This avoids over-distinguishing one family from another obtained by adding or removing redundant objects (objects whose admissibility constraint is implied by the others).

Equations

• Γ.Equivalent Γ' = (Γ.Adm = Γ'.Adm)

@[implicit_reducible]

instance FamilyOfObjects.instSetoid {E : Type u_1} : Setoid (FamilyOfObjects E)

Equations

• FamilyOfObjects.instSetoid = { r := FamilyOfObjects.Equivalent, iseqv := ⋯ }

def FamilyOfObjects.FulkersonDual {E : Type u_1} (Γ : FamilyOfObjects E) : FamilyOfObjects E

The Fulkerson dual family of Γ: the extreme points of its admissible set. Set.extremePoints only needs a Semiring/SMul structure (not a full vector space with subtraction), so this is stated directly over ℝ≥0.

Equations

• Γ.FulkersonDual = Set.extremePoints NNReal Γ.Adm