@[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

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 γ

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 Γ}