Linear transformations inside the convex algebra

A linear transformation is a single-valued convex process, and ConvexProcess.ofLinearMap is that embedding. Every operation of the convex algebra restricts along it to the corresponding operation on linear maps: the image of a set is the linear image, composition is composition, the image of a function under the associated bifunction is mapLin, and the adjoint of the process is a transpose of the linear map.

Implementation notes

The adjoints of a convex process, bifunction and function are defined outright from a pair of pairings; none mentions a linear map. A transpose enters only here, as the hypothesis IsAdjointPair Bu Bx T T' — between arbitrarily paired spaces a linear map need not have a transpose at all, and when it does it is unique only if Bu is right-separating.

adjointProcess and coadjointProcess must be kept apart on a general process, but on a linear one the graph is a subspace, so the defining inequality at -u reverses the one at u and both collapse to ⟨T u, y⟩ = ⟨u, v⟩. It is right-separation of Bu, not of Bx, that pins the answer: without it the adjoint process is single-valued only up to the annihilator of U in V.

References

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

The set-level dictionary

theorem Tdaf.ConvexAnalysis.ConvexProcess.image_ofLinearMap {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (T : U →ₗ[ℝ] X) (C : Set U) : (ofLinearMap T).image C = ⇑T '' C

theorem Tdaf.ConvexAnalysis.ConvexProcess.range_ofLinearMap {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (T : U →ₗ[ℝ] X) : (ofLinearMap T).range = Set.range ⇑T

theorem Tdaf.ConvexAnalysis.ConvexProcess.comp_ofLinearMap {U : Type u_1} {X : Type u_2} {Z : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Z] [Module ℝ Z] (S : X →ₗ[ℝ] Z) (T : U →ₗ[ℝ] X) : (ofLinearMap S).comp (ofLinearMap T) = ofLinearMap (S ∘ₗ T)

theorem Tdaf.ConvexAnalysis.ConvexProcess.ofLinearMap_injective {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : Function.Injective ofLinearMap

The image of a function under a linear process

theorem Tdaf.ConvexAnalysis.ConvexProcess.imageBifun_indicatorBifun_ofLinearMap {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (T : U →ₗ[ℝ] X) {f : U → EReal} (hbf : ∀ (u : U), f u ≠ ⊥) : imageBifun (ofLinearMap T).indicatorBifun f = mapLin T f

Ff at the indicator bifunction of a linear T is the image mapLin T f. The hypothesis that f is nowhere ⊥ is not a convenience: off the fibre of T the summand is ⊤, and ⊥ + ⊤ = ⊥ would drag the infimum to ⊥ at every point of X.

The adjoint of a linear process

theorem Tdaf.ConvexAnalysis.ConvexProcess.adjointProcess_ofLinearMap {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {T : U →ₗ[ℝ] X} {T' : Y →ₗ[ℝ] V} (hB : Bu.SeparatingRight) (hA : IsAdjointPair Bu Bx T T') : adjointProcess Bu Bx (ofLinearMap T) = ofLinearMap T'

The adjoint of a linear process is a transpose of the linear map. Bu.SeparatingRight is what makes the answer unique, as it is for the transpose itself.

theorem Tdaf.ConvexAnalysis.ConvexProcess.coadjointProcess_ofLinearMap {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {T : U →ₗ[ℝ] X} {T' : Y →ₗ[ℝ] V} (hB : Bu.SeparatingRight) (hA : IsAdjointPair Bu Bx T T') : coadjointProcess Bu Bx (ofLinearMap T) = ofLinearMap T'

The infimum-oriented adjoint of a linear process is the same transpose, the defining inequality holding in both directions on a subspace.