Preservation of essential smoothness

Essential smoothness survives infimal convolution and the image under a linear map, under the usual exactness hypotheses. Both are one argument. Essential smoothness of f is essential strict convexity of f*; the dual operation on the conjugate side is a sum, for □, or composition with the transpose, for the image; the subdifferential calculus puts the domain of the subdifferential of that dual object inside dom ∂f*; and strict convexity there survives adding a convex function or precomposing with an injective linear map. Read backwards, the same duality returns essential smoothness.

Main results

• StrictConvexOnFn.add_convexFn, StrictConvexOnFn.compLin — a strictly convex summand makes a sum strictly convex, and strict convexity pulls back along an injective linear map.
• IsExactSum.essentiallySmooth_infConv — infimal convolution (Corollary 26.3.2 in [^1]).
• IsExactImage.essentiallySmooth_mapLin — linear images (Corollary 26.3.3 in [^1]). Each has an _of_relint variant asking ri (dom f₁*) ∩ ri (dom f₂*) ≠ ∅, resp. ∃ y*, A' y* ∈ ri (dom f*).

Implementation notes

The linear-image result instantiates the exactness interface for the transpose A', because the identity used is A f = (f* A')*; surjectivity of A enters only through injectivity of A'.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §26.

Strict convexity under addition and under precomposition

theorem Tdaf.ConvexAnalysis.StrictConvexOnFn.add_convexFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f g : E → EReal} {C : Set E} (hC : Convex ℝ C) (hsc : StrictConvexOnFn f C) (hg : ConvexFn g) (hpf : Proper f) (hpg : Proper g) (hCf : C ⊆ dom f) (hCg : C ⊆ dom g) : StrictConvexOnFn (f + g) C

A strictly convex summand makes the sum strictly convex. Both functions must be finite on C: the strict inequality for f is vacuous where f x = ⊤, while the one being proved for f + g is not.

theorem Tdaf.ConvexAnalysis.ConvexFn.add_strictConvexOnFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f g : E → EReal} {C : Set E} (hC : Convex ℝ C) (hf : ConvexFn f) (hsc : StrictConvexOnFn g C) (hpf : Proper f) (hpg : Proper g) (hCf : C ⊆ dom f) (hCg : C ⊆ dom g) : StrictConvexOnFn (f + g) C

The same with the summands the other way round.

theorem Tdaf.ConvexAnalysis.StrictConvexOnFn.compLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {f : E → EReal} {A : G →ₗ[ℝ] E} {D : Set G} (h : StrictConvexOnFn f (⇑A '' D)) (hinj : Function.Injective ⇑A) : StrictConvexOnFn (ConvexAnalysis.compLin f A) D

Strict convexity pulls back along an injective linear map.

Infimal convolution

theorem Tdaf.ConvexAnalysis.IsExactSum.essentiallyStrictlyConvex_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g₁ g₂ : E → EReal} (h : IsExactSum (innerₗ E) g₁ g₂) (hg₂ : ConvexFn g₂) (hesc : EssentiallyStrictlyConvex g₁) : EssentiallyStrictlyConvex (g₁ + g₂)

The conjugate-side content: if g₁ is essentially strictly convex and g₁ + g₂ adds exactly, then g₁ + g₂ is essentially strictly convex. The sum rule for subdifferentials puts dom ∂(g₁ + g₂) inside dom ∂g₁.

theorem Tdaf.ConvexAnalysis.IsExactSum.essentiallySmooth_infConv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f₁ f₂ : E → EReal} (h : IsExactSum (innerₗ E) (conj (innerₗ E) f₁) (conj (innerₗ E) f₂)) (h₁ : ClosedProperConvexFn f₁) (h₂ : ClosedProperConvexFn f₂) (hes : EssentiallySmooth f₁) : EssentiallySmooth (infConv f₁ f₂)

If f₁ is essentially smooth and the conjugates f₁* and f₂* add exactly, then f₁ □ f₂ is essentially smooth: it is the conjugate of f₁* + f₂*.

theorem Tdaf.ConvexAnalysis.essentiallySmooth_infConv_of_relint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f₁ f₂ : E → EReal} (h₁ : ClosedProperConvexFn f₁) (h₂ : ClosedProperConvexFn f₂) (hes : EssentiallySmooth f₁) {y₀ : E} (hy₁ : y₀ ∈ intrinsicInterior ℝ (dom (conj (innerₗ E) f₁))) (hy₂ : y₀ ∈ intrinsicInterior ℝ (dom (conj (innerₗ E) f₂))) : EssentiallySmooth (infConv f₁ f₂)

The same under the classical hypothesis: a common relative interior point of dom f₁* and dom f₂* supplies the exactness.

Linear images

theorem Tdaf.ConvexAnalysis.injective_of_isAdjointPair_of_surjective {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] {A : E →ₗ[ℝ] G} {A' : G →ₗ[ℝ] E} (hA : IsAdjointPair (innerₗ G) (innerₗ E) A' A) (hsurj : Function.Surjective ⇑A) : Function.Injective ⇑A'

An onto linear map has an injective transpose.

theorem Tdaf.ConvexAnalysis.IsExactImage.essentiallyStrictlyConvex_compLin {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] {A : E →ₗ[ℝ] G} {A' : G →ₗ[ℝ] E} {g : E → EReal} {hA : IsAdjointPair (innerₗ G) (innerₗ E) A' A} (h : IsExactImage (innerₗ G) (innerₗ E) A' A hA g) (hinj : Function.Injective ⇑A') (hesc : EssentiallyStrictlyConvex g) : EssentiallyStrictlyConvex (compLin g A')

The conjugate-side content: if g is essentially strictly convex, A' is injective and g pulls back exactly along A', then g A' is essentially strictly convex. The chain rule makes dom ∂(g A') the preimage of dom ∂g.

theorem Tdaf.ConvexAnalysis.IsExactImage.essentiallySmooth_mapLin {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [FiniteDimensional ℝ G] {f : E → EReal} {A : E →ₗ[ℝ] G} {A' : G →ₗ[ℝ] E} {hA : IsAdjointPair (innerₗ G) (innerₗ E) A' A} (h : IsExactImage (innerₗ G) (innerₗ E) A' A hA (conj (innerₗ E) f)) (hf : ClosedProperConvexFn f) (hes : EssentiallySmooth f) (hinj : Function.Injective ⇑A') : EssentiallySmooth (mapLin A f)

If f is essentially smooth, A' is injective, and f* pulls back exactly along A', then the image A f is essentially smooth: it is the conjugate of f* A'.

theorem Tdaf.ConvexAnalysis.essentiallySmooth_mapLin_of_relint {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [FiniteDimensional ℝ G] {f : E → EReal} {A : E →ₗ[ℝ] G} {A' : G →ₗ[ℝ] E} (hA : IsAdjointPair (innerₗ G) (innerₗ E) A' A) (hf : ClosedProperConvexFn f) (hes : EssentiallySmooth f) (hsurj : Function.Surjective ⇑A) {y₀ : G} (hy₀ : A' y₀ ∈ intrinsicInterior ℝ (dom (conj (innerₗ E) f))) : EssentiallySmooth (mapLin A f)

The same under the classical hypotheses: A onto and some y₀ with A' y₀ ∈ ri (dom f*). The first gives injectivity of the transpose, the second the exactness.