Duality between packings and rows: the three sets

• massSet ι K — the polytope P = {a ≥ 0, ∑ a ≤ K} in ι → ℝ (compact, convex);
• slack t — the affine map a ↦ (S ↦ a(S) - t S) into Finset ι → ℝ;
• orthant ι — the closed convex cone V₊ = {v ≥ 0} in Finset ι → ℝ.

They are used in the proof of the duality statement (Proposition 6.7 of the paper), which is Dual.exists_cover in Dual/Cover.lean. The image of P under the slack map is the set C of the proof in the paper.

def AaronsonAmbainis.Dual.massSet (ι : Type u_2) [Fintype ι] (K : ℝ) : Set (ι → ℝ)

P = {a : a ≥ 0, ∑ a ≤ K}.

Equations

• AaronsonAmbainis.Dual.massSet ι K = {a : ι → ℝ | (∀ (i : ι), 0 ≤ a i) ∧ ∑ i : ι, a i ≤ K}

def AaronsonAmbainis.Dual.slack {ι : Type u_1} (t : Finset ι → ℝ) (a : ι → ℝ) : Finset ι → ℝ

The slack of a against the demands t: S ↦ a(S) - t S.

Equations

• AaronsonAmbainis.Dual.slack t a S = ∑ i ∈ S, a i - t S

def AaronsonAmbainis.Dual.orthant (ι : Type u_2) : Set (Finset ι → ℝ)

The nonnegative orthant of Finset ι → ℝ.

Equations

• AaronsonAmbainis.Dual.orthant ι = {v : Finset ι → ℝ | ∀ (S : Finset ι), 0 ≤ v S}

theorem AaronsonAmbainis.Dual.massSet_convex {ι : Type u_1} [Fintype ι] (K : ℝ) : Convex ℝ (massSet ι K)

theorem AaronsonAmbainis.Dual.massSet_isClosed {ι : Type u_1} [Fintype ι] (K : ℝ) : IsClosed (massSet ι K)

theorem AaronsonAmbainis.Dual.massSet_isCompact {ι : Type u_1} [Fintype ι] (K : ℝ) : IsCompact (massSet ι K)

theorem AaronsonAmbainis.Dual.slack_continuous {ι : Type u_1} (t : Finset ι → ℝ) : Continuous (slack t)

theorem AaronsonAmbainis.Dual.slackImage_convex {ι : Type u_1} [Fintype ι] (t : Finset ι → ℝ) (K : ℝ) : Convex ℝ (slack t '' massSet ι K)

theorem AaronsonAmbainis.Dual.slackImage_isCompact {ι : Type u_1} [Fintype ι] (t : Finset ι → ℝ) (K : ℝ) : IsCompact (slack t '' massSet ι K)

theorem AaronsonAmbainis.Dual.orthant_convex {ι : Type u_1} : Convex ℝ (orthant ι)

theorem AaronsonAmbainis.Dual.orthant_isClosed {ι : Type u_1} : IsClosed (orthant ι)