Convex analysis on a finite product

A finite product ι → E carries a pairing, a notion of product set, and — once E is finite-dimensional — a relative interior, and all three are computed coordinatewise. This file establishes that dictionary and then reads one theorem through it: a finite family of convex sets has a common relative-interior point exactly when a certain family of dual vectors summing to zero does not exist.

Main definitions

• piPairing B — the pairing of ι → E with ι → F given by ⟨x, y⟩ = ∑ i, ⟨xᵢ, yᵢ⟩, together with the four pairing classes as instances. It is to Set.pi what prodPairing is to ×ˢ.

Main results

• supportFn_univ_pi — the support function of a product set is the sum of the support functions of the factors.
• conj_piFn — the conjugate of a separable sum of proper functions is the separable sum of the conjugates, (∑ i, fᵢ ∘ prᵢ)* = ∑ i, fᵢ* ∘ prᵢ.
• iInter_relint_nonempty_iff_supportFn, iInter_relint_dom_nonempty_iff — a finite family of convex sets (resp. of effective domains) has a common relative-interior point exactly when there is no family y with ∑ i, yᵢ = 0, ∑ i, δ*(yᵢ ∣ Cᵢ) ≤ 0 and ∑ i, δ*(-yᵢ ∣ Cᵢ) > 0 (Corollary 16.2.2 in [^1]). The diagonal {x ∣ x₁ = ⋯ = xₘ} is a subspace of ι → E whose annihilator under the product pairing is the family of y summing to zero, so this is the subspace criterion of Duality/RelintSeparation.lean read at a product set.

Implementation notes

piPairing sums over Finset.univ, so the index has to be a Fintype. The product is non-dependent because the diagonal subspace needs all the factors to be the same space; the Set.pi results would hold verbatim for a dependent product.

⊥ absorbs, so supportFn_univ_pi needs no nonemptiness hypothesis — but its two sides are ⊥ for different reasons when a factor is empty, and the proof splits. The nonempty branch is an induction over the index Finset whose step decouples one coordinate with Function.update.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §16, §6 and §13.

The pairing of a finite product

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

The pairing of ι → E with ι → F, ⟨x, y⟩ = ∑ i, ⟨xᵢ, yᵢ⟩: prodPairing for a finite family, and the pairing under which a product of sets has a separable support function.

Equations

• Tdaf.ConvexAnalysis.piPairing B = LinearMap.mk₂ ℝ (fun (x : ι → E) (y : ι → F) => ∑ i : ι, (B (x i)) (y i)) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Tdaf.ConvexAnalysis.piPairing_apply {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (x : ι → E) (y : ι → F) : ((piPairing B) x) y = ∑ i : ι, (B (x i)) (y i)

theorem Tdaf.ConvexAnalysis.piPairing_flip {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : (piPairing B).flip = piPairing B.flip

Flipping the product pairing flips the pairing of the factors.

instance Tdaf.ConvexAnalysis.instIsContinuousPairingPi {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsContinuousPairing B] : IsContinuousPairing (piPairing B)

A finite product of copies of a continuous pairing is continuous.

instance Tdaf.ConvexAnalysis.instIsCompatiblePairingPi {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsCompatiblePairing B] : IsCompatiblePairing (piPairing B)

A finite product of copies of a compatible pairing is compatible.

instance Tdaf.ConvexAnalysis.isInnerPairing_piPairing {ι : Type u_1} {E : Type u_2} [Fintype ι] [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] : IsInnerPairing (piPairing B)

A finite product of copies of an inner pairing is an inner pairing. The product carries no inner-product structure of its own, but the pairing does not care.

instance Tdaf.ConvexAnalysis.isContinuousInnerPairing_piPairing {ι : Type u_1} {E : Type u_2} [Fintype ι] [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [TopologicalSpace E] [IsContinuousInnerPairing B] : IsContinuousInnerPairing (piPairing B)

The quadratic form of a finite product of inner pairings is continuous.

The relative interior of a product set

The support function of a product set

The supremum of a separable sum over a product of sets is the sum of the suprema.

theorem Tdaf.ConvexAnalysis.supportFn_univ_pi {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (C : ι → Set E) (y : ι → F) : supportFn (piPairing B) (Set.univ.pi C) y = ∑ i : ι, supportFn B (C i) (y i)

The support function of a product set is the sum of the support functions of its factors, with no hypothesis. If some factor is empty both sides are ⊥.

The conjugate of a separable sum

The other half of the finite-product dictionary. ⟨x, y⟩ - ∑ fᵢ (xᵢ) splits as ∑ (⟨xᵢ, yᵢ⟩ - fᵢ (xᵢ)) only once the ⊤ case is disposed of, which ⊥ absorbing does.

theorem Tdaf.ConvexAnalysis.conj_piFn {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : ι → E → EReal) (hf : ∀ (i : ι), Proper (f i)) (y : ι → F) : conj (piPairing B) (fun (x : ι → E) => ∑ i : ι, f i (x i)) y = ∑ i : ι, conj B (f i) (y i)

The conjugate of a separable sum is the separable sum of the conjugates. For a finite family of proper functions, (∑ i, fᵢ ∘ prᵢ)* = ∑ i, fᵢ* ∘ prᵢ against piPairing B.

Properness keeps the two sides from colliding at ∞ - ∞: it lets the supremum defining fᵢ* be taken over dom fᵢ, and it keeps fᵢ* yᵢ off ⊥, so no summand on the right can absorb.

A common relative interior point of a finite family

The diagonal {x | x₁ = ⋯ = xₘ} is a subspace of ι → E whose annihilator, under the product pairing, is the family of y summing to zero.

theorem Tdaf.ConvexAnalysis.iInter_relint_nonempty_iff_supportFn {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] (hB : B.SeparatingRight) (C : ι → Set E) (hC : ∀ (i : ι), Convex ℝ (C i)) (hne : ∀ (i : ι), (C i).Nonempty) : (⋂ (i : ι), intrinsicInterior ℝ (C i)).Nonempty ↔ ¬∃ (y : ι → F), ∑ i : ι, y i = 0 ∧ ∑ i : ι, supportFn B (C i) (y i) ≤ 0 ∧ 0 < ∑ i : ι, supportFn B (C i) (-y i)

A finite family of convex sets has a common relative interior point exactly when there is no family y of dual vectors summing to zero with ∑ i, δ*(yᵢ | Cᵢ) ≤ 0 < ∑ i, δ*(-yᵢ | Cᵢ).

This is submodule_inter_relint_nonempty_iff_supportFn in ι → E at the diagonal subspace and the product set ∏ Cᵢ. Separation on the right of the pairing is what turns the annihilator of the diagonal into ∑ i, yᵢ = 0.

theorem Tdaf.ConvexAnalysis.iInter_relint_dom_nonempty_iff {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] (hB : B.SeparatingRight) (f : ι → E → EReal) (hf : ∀ (i : ι), ConvexFn (f i)) (hp : ∀ (i : ι), Proper (f i)) (hc : ∀ (i : ι), Proper (conj B (f i))) : (⋂ (i : ι), intrinsicInterior ℝ (dom (f i))).Nonempty ↔ ¬∃ (y : ι → F), ∑ i : ι, y i = 0 ∧ ∑ i : ι, recessionFn (conj B (f i)) (y i) ≤ 0 ∧ 0 < ∑ i : ι, recessionFn (conj B (f i)) (-y i)

A finite family of proper convex functions has a common relative interior point of their effective domains exactly when there is no family y summing to zero with ∑ i, (fᵢ* 0⁺)(yᵢ) ≤ 0 < ∑ i, (fᵢ* 0⁺)(-yᵢ): the previous statement at Cᵢ = dom fᵢ, whose support function is the recession function of fᵢ*.