Concatenating coordinates: ℝᵐ × ℝⁿ and ℝᵐ⁺ⁿ

EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin (m + n)) are different types, and a text written in ℝⁿ moves between them without comment. This module is that move: the concatenation (x, y) ↦ (x₁, …, x_m, y₁, …, y_n), together with the transport along it of the operations a convexity statement is made of — conj, subgradient, ri, the polar and the pointed-cone hull.

Everything turns on inner_euclideanProdEquiv: concatenation adds the two inner products, so the form prodPairing that a product is paired with is the inner product of ℝᵐ⁺ⁿ read through the concatenation. isAdjointPair_euclideanProdEquiv packages that as an adjointness datum, and each transport lemma is one application of a general substitution rule to it.

Main definitions

• euclideanProdIsometry m n — the concatenation as a linear isometry WithLp 2 (ℝᵐ × ℝⁿ) ≃ₗᵢ[ℝ] ℝᵐ⁺ⁿ.
• euclideanProdEquiv m n — the same map out of the plain product, ℝᵐ × ℝⁿ ≃L[ℝ] ℝᵐ⁺ⁿ.
• euclideanOne — ℝ ≃L[ℝ] ℝ¹, the scalar read as a one-dimensional Euclidean space.
• euclideanTripleEquiv n — ℝ × ℝⁿ × ℝ ≃L[ℝ] ℝⁿ⁺², what a text means by (λ, x, μ) ∈ ℝⁿ⁺².

Main results

• inner_euclideanProdEquiv, isAdjointPair_euclideanProdEquiv — the pairing and its adjointness datum; euclideanProdEquiv_apply_castAdd and friends give the coordinates.
• conj_comp_euclideanProdEquiv, subgradient_comp_euclideanProdEquiv, relint_image_euclideanProdEquiv — conjugate, subdifferential and relative interior transport.
• polarCone_image_of_pairing_eq, coe_hull_image — the same for the polar of a set and for the pointed-cone hull, which is what a statement about cones is made of.
• inner_euclideanTripleEquiv, closure_image_euclideanTripleEquiv — the triple concatenation carries the inner product of ℝⁿ⁺² to λ λ* + ⟨x, y⟩ + μ μ* and commutes with the closure. That is all a consumer needs: which Fin (n + 2) index carries λ is an artefact of the assembly.

Implementation notes

The isometry is out of WithLp 2 (ℝᵐ × ℝⁿ) because Mathlib's norm on a product is the supremum norm. Everything else is stated for the plain product, whose linear structure and topology are all that conj, subgradient and ri need, so that no consumer has to move a Convex or an IsClosed across a type synonym; euclideanProdEquiv_eq_isometry records that the two agree.

The concatenation

noncomputable def Tdaf.ConvexAnalysis.euclideanProdIsometry (m n : ℕ) : WithLp 2 (EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n)) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (m + n))

Concatenation of coordinates, (x, y) ↦ (x₁, …, x_m, y₁, …, y_n), as a linear isometry out of WithLp 2 (ℝᵐ × ℝⁿ): Mathlib's product norm is the supremum norm, and concatenation is an isometry only for the Euclidean one.

Equations

• Tdaf.ConvexAnalysis.euclideanProdIsometry m n = (PiLp.sumPiLpEquivProdLpPiLp 2 fun (x : Fin m ⊕ Fin n) => ℝ).symm.trans (LinearIsometryEquiv.piLpCongrLeft 2 ℝ ℝ finSumFinEquiv)

noncomputable def Tdaf.ConvexAnalysis.euclideanProdEquiv (m n : ℕ) : (EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n)) ≃L[ℝ] EuclideanSpace ℝ (Fin (m + n))

Concatenation of coordinates out of the plain product, which carries the supremum norm. No longer an isometry, but still a linear homeomorphism, which is all the transports below need.

Equations

• One or more equations did not get rendered due to their size.

theorem Tdaf.ConvexAnalysis.euclideanProdEquiv_eq_isometry {m n : ℕ} (p : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n)) : (euclideanProdEquiv m n) p = (euclideanProdIsometry m n) (WithLp.toLp 2 p)

The two concatenations are the same map.

@[simp]

theorem Tdaf.ConvexAnalysis.euclideanProdEquiv_apply_castAdd {m n : ℕ} (p : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n)) (i : Fin m) : ((euclideanProdEquiv m n) p).ofLp (Fin.castAdd n i) = p.1.ofLp i

@[simp]

theorem Tdaf.ConvexAnalysis.euclideanProdEquiv_apply_natAdd {m n : ℕ} (p : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n)) (i : Fin n) : ((euclideanProdEquiv m n) p).ofLp (Fin.natAdd m i) = p.2.ofLp i

theorem Tdaf.ConvexAnalysis.euclideanProdEquiv_symm_apply {m n : ℕ} (z : EuclideanSpace ℝ (Fin (m + n))) : (euclideanProdEquiv m n).symm z = (WithLp.toLp 2 fun (i : Fin m) => z.ofLp (Fin.castAdd n i), WithLp.toLp 2 fun (i : Fin n) => z.ofLp (Fin.natAdd m i))

@[simp]

theorem Tdaf.ConvexAnalysis.euclideanProdEquiv_symm_apply_fst {m n : ℕ} (z : EuclideanSpace ℝ (Fin (m + n))) (i : Fin m) : ((euclideanProdEquiv m n).symm z).1.ofLp i = z.ofLp (Fin.castAdd n i)

@[simp]

theorem Tdaf.ConvexAnalysis.euclideanProdEquiv_symm_apply_snd {m n : ℕ} (z : EuclideanSpace ℝ (Fin (m + n))) (i : Fin n) : ((euclideanProdEquiv m n).symm z).2.ofLp i = z.ofLp (Fin.natAdd m i)

theorem Tdaf.ConvexAnalysis.inner_euclideanProdEquiv {m n : ℕ} (p q : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n)) : inner ℝ ((euclideanProdEquiv m n) p) ((euclideanProdEquiv m n) q) = inner ℝ p.1 q.1 + inner ℝ p.2 q.2

Concatenation adds the two inner products. So prodPairing, the form a product is paired with, is the inner product of ℝᵐ⁺ⁿ read through the concatenation.

The adjointness datum

theorem Tdaf.ConvexAnalysis.prodPairing_euclideanProdEquiv_symm {m n : ℕ} (z : EuclideanSpace ℝ (Fin (m + n))) (q : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n)) : ((prodPairing (innerₗ (EuclideanSpace ℝ (Fin m))) (innerₗ (EuclideanSpace ℝ (Fin n)))) ((euclideanProdEquiv m n).symm z)) q = ((innerₗ (EuclideanSpace ℝ (Fin (m + n)))) z) ((euclideanProdEquiv m n) q)

The inner product of ℝᵐ⁺ⁿ pulled back along the concatenation is prodPairing.

theorem Tdaf.ConvexAnalysis.isAdjointPair_euclideanProdEquiv {m n : ℕ} : IsAdjointPair (innerₗ (EuclideanSpace ℝ (Fin (m + n)))) (prodPairing (innerₗ (EuclideanSpace ℝ (Fin m))) (innerₗ (EuclideanSpace ℝ (Fin n)))) ↑↑(euclideanProdEquiv m n).symm ↑↑(euclideanProdEquiv m n)

Concatenation is an adjoint pair for the two pairings. This is the hypothesis conj_comp_linearEquiv and subgradient_comp_linearEquiv take, and the only mathematical input the transport has.

Transporting the subdifferential along a linear isomorphism

conj_comp_linearEquiv is the substitution rule for the conjugate. The subdifferential obeys the same rule, in the generality of an arbitrary adjoint pair of isomorphisms.

theorem Tdaf.ConvexAnalysis.subgradient_comp_linearEquiv {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [AddCommGroup H] [Module ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} (A : E ≃ₗ[ℝ] G) (A' : H ≃ₗ[ℝ] F) (hA : IsAdjointPair B B' ↑A ↑A') (g : G → EReal) (x : E) : subgradient B (fun (u : E) => g (A u)) x = ⇑A' '' subgradient B' g (A x)

Precomposing with a linear isomorphism moves the subdifferential along the transpose. The companion of conj_comp_linearEquiv for ∂f: if A and A' are adjoint isomorphisms, then ∂(g ∘ A)(x) = A' (∂g (A x)).

The transport

theorem Tdaf.ConvexAnalysis.conj_comp_euclideanProdEquiv {m n : ℕ} (f : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n) → EReal) (z : EuclideanSpace ℝ (Fin (m + n))) : conj (innerₗ (EuclideanSpace ℝ (Fin (m + n)))) (fun (w : EuclideanSpace ℝ (Fin (m + n))) => f ((euclideanProdEquiv m n).symm w)) z = conj (prodPairing (innerₗ (EuclideanSpace ℝ (Fin m))) (innerₗ (EuclideanSpace ℝ (Fin n)))) f ((euclideanProdEquiv m n).symm z)

The conjugate transports along the concatenation. A function f on ℝᵐ × ℝⁿ read as a function on ℝᵐ⁺ⁿ has, as its conjugate for the inner product of ℝᵐ⁺ⁿ, the conjugate of f for prodPairing read the same way.

theorem Tdaf.ConvexAnalysis.subgradient_comp_euclideanProdEquiv {m n : ℕ} (f : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n) → EReal) (z : EuclideanSpace ℝ (Fin (m + n))) : subgradient (innerₗ (EuclideanSpace ℝ (Fin (m + n)))) (fun (w : EuclideanSpace ℝ (Fin (m + n))) => f ((euclideanProdEquiv m n).symm w)) z = ⇑(euclideanProdEquiv m n) '' subgradient (prodPairing (innerₗ (EuclideanSpace ℝ (Fin m))) (innerₗ (EuclideanSpace ℝ (Fin n)))) f ((euclideanProdEquiv m n).symm z)

The subdifferential transports along the concatenation.

theorem Tdaf.ConvexAnalysis.relint_image_euclideanProdEquiv {m n : ℕ} {C : Set (EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n))} (hC : Convex ℝ C) : intrinsicInterior ℝ (⇑(euclideanProdEquiv m n) '' C) = ⇑(euclideanProdEquiv m n) '' intrinsicInterior ℝ C

The relative interior transports along the concatenation.

theorem Tdaf.ConvexAnalysis.relint_image_euclideanProdEquiv_symm {m n : ℕ} {D : Set (EuclideanSpace ℝ (Fin (m + n)))} (hD : Convex ℝ D) : intrinsicInterior ℝ (⇑(euclideanProdEquiv m n).symm '' D) = ⇑(euclideanProdEquiv m n).symm '' intrinsicInterior ℝ D

The relative interior transports along the concatenation, read the other way.

theorem Tdaf.ConvexAnalysis.closure_image_euclideanProdEquiv {m n : ℕ} (C : Set (EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin n))) : closure (⇑(euclideanProdEquiv m n) '' C) = ⇑(euclideanProdEquiv m n) '' closure C

The closure transports along the concatenation, because it is a homeomorphism.

Transporting polarity and cone hulls

Both are needed wherever a cone in a product is read in ℝᵏ: the polar consumes the adjointness datum, the pointed-cone hull needs only linearity.

theorem Tdaf.ConvexAnalysis.polarCone_image_of_pairing_eq {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [AddCommGroup H] [Module ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} (A : E ≃ₗ[ℝ] G) (A' : F ≃ₗ[ℝ] H) (hA : ∀ (p : E) (q : F), (B' (A p)) (A' q) = (B p) q) (S : Set E) : polarCone B' (⇑A '' S) = ⇑A' '' polarCone B S

Polarity transports along an adjoint pair of isomorphisms. If A and A' carry B' back to B, the polar of A '' S for B' is the image under A' of the polar of S for B.

theorem Tdaf.ConvexAnalysis.coe_hull_image {E : Type u_1} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (A : E →ₗ[ℝ] G) (S : Set E) : ↑(PointedCone.hull ℝ (⇑A '' S)) = ⇑A '' ↑(PointedCone.hull ℝ S)

The pointed-cone hull transports along a linear map: hull (A '' S) = A '' hull S. This is Submodule.map_span over the semiring of non-negative reals, restated on the underlying sets.

The one-dimensional factor, and ℝ × ℝⁿ × ℝ as ℝⁿ⁺²

ℝ is not EuclideanSpace ℝ (Fin 1), so a concatenation with a scalar factor at each end needs one more transport prepended and one appended.

noncomputable def Tdaf.ConvexAnalysis.euclideanOne : ℝ ≃L[ℝ] EuclideanSpace ℝ (Fin 1)

ℝ as a one-dimensional Euclidean space, a ↦ (a).

Equations

• Tdaf.ConvexAnalysis.euclideanOne = (PiLp.equivOfUnique 2 ℝ fun (x : Fin 1) => ℝ).symm

@[simp]

theorem Tdaf.ConvexAnalysis.euclideanOne_apply (a : ℝ) (i : Fin 1) : (euclideanOne a).ofLp i = a

theorem Tdaf.ConvexAnalysis.inner_euclideanOne (a b : ℝ) : inner ℝ (euclideanOne a) (euclideanOne b) = a * b

The one-dimensional transport multiplies: it is an isometry of ℝ onto ℝ¹.

noncomputable def Tdaf.ConvexAnalysis.euclideanTripleEquiv (n : ℕ) : ((ℝ × EuclideanSpace ℝ (Fin n)) × ℝ) ≃L[ℝ] EuclideanSpace ℝ (Fin (n + 2))

Concatenation of ℝ × ℝⁿ × ℝ into ℝⁿ⁺²: (λ, x, μ) ↦ (λ, x₁, …, xₙ, μ), a linear homeomorphism. Its effect on the inner product is inner_euclideanTripleEquiv.

Equations

• One or more equations did not get rendered due to their size.

theorem Tdaf.ConvexAnalysis.inner_euclideanTripleEquiv {n : ℕ} (p q : (ℝ × EuclideanSpace ℝ (Fin n)) × ℝ) : inner ℝ ((euclideanTripleEquiv n) p) ((euclideanTripleEquiv n) q) = p.1.1 * q.1.1 + inner ℝ p.1.2 q.1.2 + p.2 * q.2

The triple concatenation adds the three inner products.

theorem Tdaf.ConvexAnalysis.closure_image_euclideanTripleEquiv {n : ℕ} (S : Set ((ℝ × EuclideanSpace ℝ (Fin n)) × ℝ)) : closure (⇑(euclideanTripleEquiv n) '' S) = ⇑(euclideanTripleEquiv n) '' closure S

The closure transports along the triple concatenation, because it is a homeomorphism.