Images and inverse images of convex functions under a linear map

A linear map A : E → G transports convex functions in both directions. The inverse image g A = g ∘ A is the easy one — its epigraph is a preimage — while the image (A f) y = inf {f x | A x = y} is the interesting one: the infimum need not be attained, so A f is read off epi f not as a set image but as the function that image determines. Accordingly epi (A f) = (A × id) '' epi f is false in general (exists_epi_mapLin_ne_image); epi_mapLin recovers it from IsEpiLike, exactly the missing attainment.

Main definitions

• mapLin A f — the image A f of f under A.
• compLin g A — the inverse image g A of g under A.

Main results

• convexFn_compLin, convexFn_mapLin — both directions preserve convexity.
• gc_compLin_mapLin — g ≤ A f ↔ g A ≤ f, a monotone Galois connection (no OrderDual, unlike gc_ofEpi_epi), giving the monotonicity lemmas, the unit and counit, and — for surjective A, where it is a GaloisCoinsertion — the identity A (g A) = g.
• mapLin_eq_ofEpi — the image is the function determined by the image of the epigraph under (x, μ) ↦ (A x, μ), which is how convexity of the image is proved.
• convexFn_iInf_right — partial minimisation y ↦ ⨅ z, h (y, z) of a jointly convex function is convex: the projection case, and the form the perturbation function of a convex program takes.
• ConvexFn.comp_affine, ConvexFn.slice_left, ConvexFn.slice_right — precomposition with an affine map, and fixing one variable of a function of two.

References

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

The two operations

noncomputable def Tdaf.ConvexAnalysis.mapLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) (f : E → EReal) : G → EReal

The image of f under a linear map A: (A f) y = inf {f x | A x = y} over the fibre of A above y, hence ⊤ off its range. The infimum is generally not attained.

Equations

• Tdaf.ConvexAnalysis.mapLin A f y = ⨅ x ∈ {x : E | A x = y}, f x

def Tdaf.ConvexAnalysis.compLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (g : G → EReal) (A : E →ₗ[ℝ] G) : E → EReal

The inverse image of g under a linear map A: (g A) x = g (A x).

Equations

• Tdaf.ConvexAnalysis.compLin g A = g ∘ ⇑A

@[reducible, inline]

abbrev Tdaf.ConvexAnalysis.prodMapId {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) : E × ℝ →ₗ[ℝ] G × ℝ

The map (x, μ) ↦ (A x, μ), along which epi (g A) is the pullback of epi g.

Equations

• Tdaf.ConvexAnalysis.prodMapId A = A.prodMap LinearMap.id

@[simp]

theorem Tdaf.ConvexAnalysis.compLin_apply {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (g : G → EReal) (A : E →ₗ[ℝ] G) (x : E) : compLin g A x = g (A x)

The infimum defining the image

theorem Tdaf.ConvexAnalysis.mapLin_le {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} {f : E → EReal} {x : E} {y : G} (h : A x = y) : mapLin A f y ≤ f x

theorem Tdaf.ConvexAnalysis.le_mapLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} {f : E → EReal} {y : G} {z : EReal} (h : ∀ (x : E), A x = y → z ≤ f x) : z ≤ mapLin A f y

theorem Tdaf.ConvexAnalysis.mapLin_lt_iff {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} {f : E → EReal} {y : G} {z : EReal} : mapLin A f y < z ↔ ∃ (x : E), A x = y ∧ f x < z

The witness extractor: as for ofEpi, arguments go through a strict inequality.

theorem Tdaf.ConvexAnalysis.mapLin_of_notMem_range {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} {f : E → EReal} {y : G} (hy : y ∉ Set.range ⇑A) : mapLin A f y = ⊤

Off the range of A the image is ⊤: there is nothing to take an infimum over.

The adjunction g ≤ A f ↔ g A ≤ f

theorem Tdaf.ConvexAnalysis.gc_compLin_mapLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) : GaloisConnection (fun (g : G → EReal) => compLin g A) fun (f : E → EReal) => mapLin A f

The universal property of the image. f ↦ A f is right adjoint to g ↦ g A.

theorem Tdaf.ConvexAnalysis.le_mapLin_iff {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} {f : E → EReal} {g : G → EReal} : g ≤ mapLin A f ↔ compLin g A ≤ f

theorem Tdaf.ConvexAnalysis.mapLin_mono {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} {f₁ f₂ : E → EReal} (h : f₁ ≤ f₂) : mapLin A f₁ ≤ mapLin A f₂

theorem Tdaf.ConvexAnalysis.compLin_mono {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} {g₁ g₂ : G → EReal} (h : g₁ ≤ g₂) : compLin g₁ A ≤ compLin g₂ A

theorem Tdaf.ConvexAnalysis.compLin_mapLin_le {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) (f : E → EReal) : compLin (mapLin A f) A ≤ f

The counit of the adjunction: (A f) (A x) ≤ f x.

theorem Tdaf.ConvexAnalysis.le_mapLin_compLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) (g : G → EReal) : g ≤ mapLin A (compLin g A)

The unit of the adjunction: g ≤ A (g A), with equality exactly on the range of A.

theorem Tdaf.ConvexAnalysis.mapLin_compLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} (hA : Function.Surjective ⇑A) (g : G → EReal) : mapLin A (compLin g A) = g

noncomputable def Tdaf.ConvexAnalysis.gci_compLin_mapLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} (hA : Function.Surjective ⇑A) : GaloisCoinsertion (fun (g : G → EReal) => compLin g A) fun (f : E → EReal) => mapLin A f

For surjective A the adjunction is a GaloisCoinsertion.

Equations

• Tdaf.ConvexAnalysis.gci_compLin_mapLin hA = ⋯.toGaloisCoinsertion ⋯

Effective domains

theorem Tdaf.ConvexAnalysis.dom_compLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (g : G → EReal) (A : E →ₗ[ℝ] G) : dom (compLin g A) = ⇑A ⁻¹' dom g

theorem Tdaf.ConvexAnalysis.proper_compLin_of_surjective {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} {g : G → EReal} (hA : Function.Surjective ⇑A) : Proper (compLin g A) ↔ Proper g

Properness survives a surjective substitution, both ways. Surjectivity is needed for both halves: g A can be proper while g is ⊥ off the range, and g proper while A misses all of its finite values.

theorem Tdaf.ConvexAnalysis.dom_mapLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) (f : E → EReal) : dom (mapLin A f) = ⇑A '' dom f

The effective domain of an image is the image of the effective domain; no convexity needed.

Epigraphs, and convexity in both directions

theorem Tdaf.ConvexAnalysis.epi_compLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (g : G → EReal) (A : E →ₗ[ℝ] G) : epi (compLin g A) = ⇑(prodMapId A) ⁻¹' epi g

epi g pulled back along (x, μ) ↦ (A x, μ): the whole proof of the inverse-image half.

theorem Tdaf.ConvexAnalysis.convexFn_compLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {g : G → EReal} (A : E →ₗ[ℝ] G) (hg : ConvexFn g) : ConvexFn (compLin g A)

The inverse image of a convex function under a linear map is convex.

theorem Tdaf.ConvexAnalysis.ConvexFn.comp_affine {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {g : G → EReal} (hg : ConvexFn g) (A : E →ₗ[ℝ] G) (b : G) : ConvexFn fun (x : E) => g (A x + b)

Precomposition with an affine map preserves convexity, in the form applications want.

theorem Tdaf.ConvexAnalysis.mapLin_eq_ofEpi {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) (f : E → EReal) : mapLin A f = ofEpi (⇑(A.prodMap LinearMap.id) '' epi f)

The image of f under A is the function determined by the image of epi f under (x, μ) ↦ (A x, μ). This is an equality of functions; the corresponding equality of sets, epi_mapLin, needs a hypothesis.

theorem Tdaf.ConvexAnalysis.convexFn_mapLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {f : E → EReal} (A : E →ₗ[ℝ] G) (hf : ConvexFn f) : ConvexFn (mapLin A f)

The image of a convex function under a linear map is convex: a linear image of a convex set is convex, and the function it determines is then convex too.

theorem Tdaf.ConvexAnalysis.epi_mapLin {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] {A : E →ₗ[ℝ] G} {f : E → EReal} (h : IsEpiLike (⇑(A.prodMap LinearMap.id) '' epi f)) : epi (mapLin A f) = ⇑(A.prodMap LinearMap.id) '' epi f

The epigraph of the image is the image of the epigraph, under the hypothesis that makes it true: the infimum defining A f must be attained wherever it is finite.

Indicator functions

theorem Tdaf.ConvexAnalysis.mapLin_indicatorFn {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) (s : Set E) : mapLin A (indicatorFn s) = indicatorFn (⇑A '' s)

theorem Tdaf.ConvexAnalysis.compLin_indicatorFn {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) (s : Set G) : compLin (indicatorFn s) A = indicatorFn (⇑A ⁻¹' s)

The hypothesis of epi_mapLin is not removable

theorem Tdaf.ConvexAnalysis.exists_epi_mapLin_ne_image : ∃ (f : ℝ → EReal) (A : ℝ →ₗ[ℝ] ℝ), ConvexFn f ∧ epi (mapLin A f) ≠ ⇑(A.prodMap LinearMap.id) '' epi f

The image of an epigraph need not be an epigraph. With A = 0 on ℝ and f the (convex) function equal to x on (0, ∞) and ⊤ elsewhere, (A f) 0 = inf {x | x > 0} = 0 is not attained: (0, 0) belongs to epi (A f) but not to the image of epi f, which is {0} × (0, ∞).

Partial minimisation: the projection case

theorem Tdaf.ConvexAnalysis.ConvexFn.slice_left {Y : Type u_1} {Z : Type u_2} [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] {h : Y × Z → EReal} (hh : ConvexFn h) (c : Y) : ConvexFn fun (z : Z) => h (c, z)

Fixing one variable of a jointly convex function: the slice map z ↦ (c, z) is affine.

theorem Tdaf.ConvexAnalysis.ConvexFn.slice_right {Y : Type u_1} {Z : Type u_2} [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] {h : Y × Z → EReal} (hh : ConvexFn h) (c : Z) : ConvexFn fun (y : Y) => h (y, c)

theorem Tdaf.ConvexAnalysis.mapLin_fst_apply {Y : Type u_1} {Z : Type u_2} [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] (h : Y × Z → EReal) (y : Y) : mapLin (LinearMap.fst ℝ Y Z) h y = ⨅ (z : Z), h (y, z)

The image under the projection (y, z) ↦ y is minimisation over z.

theorem Tdaf.ConvexAnalysis.mapLin_fst {Y : Type u_1} {Z : Type u_2} [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] (h : Y × Z → EReal) : mapLin (LinearMap.fst ℝ Y Z) h = fun (y : Y) => ⨅ (z : Z), h (y, z)

theorem Tdaf.ConvexAnalysis.convexFn_iInf_right {Y : Type u_1} {Z : Type u_2} [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] {h : Y × Z → EReal} (hh : ConvexFn h) : ConvexFn fun (y : Y) => ⨅ (z : Z), h (y, z)

Partial minimisation preserves convexity: the image case with A a projection. This is the form used to build the perturbation function of a convex program.

theorem Tdaf.ConvexAnalysis.dom_iInf_right {Y : Type u_1} {Z : Type u_2} [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] (h : Y × Z → EReal) : (dom fun (y : Y) => ⨅ (z : Z), h (y, z)) = Prod.fst '' dom h