Sums of finitely many convex sets

A sum C₁ + ⋯ + Cₘ of subsets of E is the image of the product set ∏ Cᵢ ⊆ ι → E under the sum map (xᵢ) ↦ ∑ xᵢ, so every question about the closure and the recession cone of a finite sum becomes a question about a linear image, which the recession calculus of a linear map answers. Convex.isClosed_sum, Convex.closure_sum_eq and Convex.recessionCone_sum are the m-ary statements: closure and recession cone both distribute over a finite sum of convex sets.

The cancellation hypothesis is genuinely m-ary: a sum of m directions of recession can vanish without any two of them cancelling, so it is stated on the family, and the two-set results of Recession/Closedness.lean are kept separately rather than derived from these.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §9.

def Tdaf.ConvexAnalysis.piSum {ι : Type u_1} {E : Type u_2} [Fintype ι] [AddCommGroup E] [Module ℝ E] : (ι → E) →ₗ[ℝ] E

The sum map (x₁, …, xₘ) ↦ x₁ + ⋯ + xₘ of a finite product, as a linear map: the m-ary codiagonal.

Equations

• Tdaf.ConvexAnalysis.piSum = { toFun := fun (x : ι → E) => ∑ i : ι, x i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.piSum_apply {ι : Type u_1} {E : Type u_2} [Fintype ι] [AddCommGroup E] [Module ℝ E] (x : ι → E) : piSum x = ∑ i : ι, x i

theorem Tdaf.ConvexAnalysis.image_piSum_univ_pi {ι : Type u_1} {E : Type u_2} [Fintype ι] [AddCommGroup E] [Module ℝ E] (C : ι → Set E) : ⇑piSum '' Set.univ.pi C = ∑ i : ι, C i

A sum of finitely many sets is the image of their product under the sum map: what turns a question about a finite sum into a question about a linear image.

theorem Tdaf.ConvexAnalysis.forall_mem_linealitySpace_pi {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {C : ι → Set E} (hne : ∀ (i : ι), (C i).Nonempty) (h : ∀ (z : ι → E), (∀ (i : ι), z i ∈ recessionCone (closure (C i))) → ∑ i : ι, z i = 0 → ∀ (i : ι), z i ∈ linealitySpace (closure (C i))) (p : ι → E) : p ∈ recessionCone (closure (Set.univ.pi C)) → piSum p = 0 → p ∈ linealitySpace (closure (Set.univ.pi C))

The cancellation hypothesis for a family, transported to the product set.

theorem Tdaf.ConvexAnalysis.Convex.isClosed_sum {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : ι → Set E} (hC : ∀ (i : ι), Convex ℝ (C i)) (hCc : ∀ (i : ι), IsClosed (C i)) (hne : ∀ (i : ι), (C i).Nonempty) (h : ∀ (z : ι → E), (∀ (i : ι), z i ∈ recessionCone (C i)) → ∑ i : ι, z i = 0 → ∀ (i : ι), z i ∈ linealitySpace (C i)) : IsClosed (∑ i : ι, C i)

Closedness of a finite sum: a finite sum of closed convex sets is closed as soon as the only way finitely many directions of recession can sum to zero is inside the lineality spaces.

theorem Tdaf.ConvexAnalysis.Convex.closure_sum_eq {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : ι → Set E} (hC : ∀ (i : ι), Convex ℝ (C i)) (hne : ∀ (i : ι), (C i).Nonempty) (h : ∀ (z : ι → E), (∀ (i : ι), z i ∈ recessionCone (closure (C i))) → ∑ i : ι, z i = 0 → ∀ (i : ι), z i ∈ linealitySpace (closure (C i))) : closure (∑ i : ι, C i) = ∑ i : ι, closure (C i)

Closure distributes over a finite sum: cl (C₁ + ⋯ + Cₘ) = cl C₁ + ⋯ + cl Cₘ.

theorem Tdaf.ConvexAnalysis.Convex.recessionCone_sum {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : ι → Set E} (hC : ∀ (i : ι), Convex ℝ (C i)) (hne : ∀ (i : ι), (C i).Nonempty) (h : ∀ (z : ι → E), (∀ (i : ι), z i ∈ recessionCone (closure (C i))) → ∑ i : ι, z i = 0 → ∀ (i : ι), z i ∈ linealitySpace (closure (C i))) : recessionCone (∑ i : ι, closure (C i)) = ∑ i : ι, recessionCone (closure (C i))

The recession cone of a finite sum of closed convex sets: 0⁺(cl C₁ + ⋯ + cl Cₘ) = 0⁺(cl C₁) + ⋯ + 0⁺(cl Cₘ).