The Euclidean instantiation shared by every ℝⁿ surface

Rn n is EuclideanSpace ℝ (Fin n) and pairing n is its own inner product read as a bilinear map. Together they instantiate the backbone's duality theory at a stroke, which is why a textbook written in ℝⁿ can state everything without qualification. Nothing here is tied to one book.

Main definitions

• Rn n — the ambient space.
• pairing n — the self-pairing ⟨x, y⟩, as a LinearMap so that the backbone's duality applies.
• pairingProd, pairingAdjoint — the pairing on a product, and its sign-flipped form.
• linFn b — the vector b read as the linear function ⟨·, b⟩.

Main results

• flip_pairing — the pairing is its own flip; conj_flip_pairing and its seven companions rewrite away the .flip a bipolar theorem hands back.
• pairing_comm, forall_pairing_le_comm, forall_pairing_lt_comm — a book writes a linear system as ⟨aᵢ, x⟩ ≤ αᵢ and the backbone puts the variable on the left; these translate.
• exists_linFn, linFn_eq_toDual — the Fréchet–Riesz translation between the book's vector b and the backbone's continuous linear functional.
• pairingProd_euclideanProdEquiv — pairingProd is the inner product of Rn (m + n), read through the concatenation of coordinates.

Implementation notes

A textbook in ℝⁿ identifies a space with its dual, writing x* for a vector of the same space. Both sides of pairing n are Rn n, so the book's * is a naming convention here and not a type distinction. The backbone keeps its two spaces apart precisely so that the general theory cannot use self-duality silently.

References

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

@[reducible, inline]

abbrev TdafSurface.Rn (n : ℕ) : Type

The ambient space of a finite-dimensional real surface: ℝⁿ with its Euclidean structure.

Equations

• TdafSurface.Rn n = EuclideanSpace ℝ (Fin n)

@[reducible, inline]

noncomputable abbrev TdafSurface.pairing (n : ℕ) : Rn n →ₗ[ℝ] Rn n →ₗ[ℝ] ℝ

The standard inner product on Rn n, as a bilinear map, which is the form the backbone's duality theory takes. A book that writes ⟨x, x*⟩ for vectors of one space means this. An abbrev, not a def: instance search does not unfold a plain def, and every pairing class the surface needs is stated about innerₗ.

Equations

• TdafSurface.pairing n = innerₗ (TdafSurface.Rn n)

@[simp]

theorem TdafSurface.pairing_apply {n : ℕ} (x y : Rn n) : ((pairing n) x) y = inner ℝ x y

@[simp]

theorem TdafSurface.flip_pairing (n : ℕ) : (pairing n).flip = pairing n

The pairing is symmetric, hence its own flip: every backbone statement that asks for B.flip is asking for pairing n again.

theorem TdafSurface.pairing_comm {n : ℕ} (x y : Rn n) : ((pairing n) x) y = ((pairing n) y) x

The pairing is symmetric. Rockafellar writes a linear system as ⟨aᵢ, x⟩ ≤ αᵢ, with the data on the left; the backbone's B x y puts the variable there.

theorem TdafSurface.forall_pairing_le_comm {n : ℕ} {ι : Sort u_1} (a : ι → Rn n) (α : ι → ℝ) (x : Rn n) : (∀ (i : ι), ((pairing n) (a i)) x ≤ α i) ↔ ∀ (i : ι), ((pairing n) x) (a i) ≤ α i

A system of weak inequalities read in the book's orientation and in the backbone's.

theorem TdafSurface.forall_pairing_lt_comm {n : ℕ} {ι : Sort u_1} (a : ι → Rn n) (α : ι → ℝ) (x : Rn n) : (∀ (i : ι), ((pairing n) (a i)) x < α i) ↔ ∀ (i : ι), ((pairing n) x) (a i) < α i

A system of strict inequalities read in the book's orientation and in the backbone's.

theorem TdafSurface.pairing_eq_sum {n : ℕ} (u v : Rn n) : ((pairing n) u) v = ∑ i : Fin n, u.ofLp i * v.ofLp i

The pairing in coordinates: ⟨u, v⟩ = ∑ᵢ uᵢ vᵢ.

theorem TdafSurface.pairing_two (u v : Rn 2) : ((pairing 2) u) v = u.ofLp 0 * v.ofLp 0 + u.ofLp 1 * v.ofLp 1

The pairing on ℝ² in coordinates: ⟨u, v⟩ = u₀v₀ + u₁v₁. Rockafellar's counterexamples are two-dimensional almost without exception, and this is the first line of every one of them.

theorem TdafSurface.continuous_coord {n : ℕ} (i : Fin n) : Continuous fun (x : Rn n) => x.ofLp i

Each coordinate of Rn n is continuous, Rn n being a PiLp 2. A counterexample that cuts a region out of Rn n with coordinate inequalities needs this to see the region is open.

theorem TdafSurface.separatingRight_pairing (n : ℕ) : (pairing n).SeparatingRight

pairing n separates on the right, which is the hypothesis the backbone's level-set and recession duality asks for in place of a book's y ≠ 0.

@[reducible, inline]

noncomputable abbrev TdafSurface.pairingProd (m n : ℕ) : Rn m × Rn n →ₗ[ℝ] Rn m × Rn n →ₗ[ℝ] ℝ

The product pairing on Rn m × Rn n, which is what a bifunction from ℝᵐ to ℝⁿ is conjugated against.

Equations

• TdafSurface.pairingProd m n = Tdaf.ConvexAnalysis.prodPairing (TdafSurface.pairing m) (TdafSurface.pairing n)

@[reducible, inline]

noncomputable abbrev TdafSurface.pairingAdjoint (m n : ℕ) : Rn m × Rn n →ₗ[ℝ] Rn m × Rn n →ₗ[ℝ] ℝ

The sign-flipped product pairing of §30: the one Rockafellar's adjoint F* of a convex bifunction is stated against.

Equations

• TdafSurface.pairingAdjoint m n = Tdaf.ConvexAnalysis.negFst (TdafSurface.pairingProd m n)

theorem TdafSurface.pairingProd_euclideanProdEquiv {m n : ℕ} (p q : Rn m × Rn n) : ((pairingProd m n) p) q = ((pairing (m + n)) ((Tdaf.ConvexAnalysis.euclideanProdEquiv m n) p)) ((Tdaf.ConvexAnalysis.euclideanProdEquiv m n) q)

The product pairing is the pairing of Rn (m + n), read through the concatenation of coordinates (euclideanProdEquiv). This is the identification a text in ℝⁿ makes silently whenever it writes a point of ℝᵐ × ℝⁿ as a point of ℝᵐ⁺ⁿ.

Dimension

Module.finrank ℝ (Rn n) = n is finrank_euclideanSpace_fin, which Mathlib does not mark simp; every dimension count the surface states needs it.

Instance discharge

Each example asserts that a class the surface needs is found by instance search with no hypothesis. They are the regression test for the instantiation.

Rewriting .flip away

flip_pairing is a simp lemma, but a .flip inside a conj or a subgradient sits under a binder simp will not always reach.

@[simp]

theorem TdafSurface.conj_flip_pairing {n : ℕ} (f : Rn n → EReal) : Tdaf.ConvexAnalysis.conj (pairing n).flip f = Tdaf.ConvexAnalysis.conj (pairing n) f

@[simp]

theorem TdafSurface.subgradient_flip_pairing {n : ℕ} (f : Rn n → EReal) (x : Rn n) : Tdaf.ConvexAnalysis.subgradient (pairing n).flip f x = Tdaf.ConvexAnalysis.subgradient (pairing n) f x

@[simp]

theorem TdafSurface.supportSet_flip_pairing {n : ℕ} (f : Rn n → EReal) : Tdaf.ConvexAnalysis.supportSet (pairing n).flip f = Tdaf.ConvexAnalysis.supportSet (pairing n) f

@[simp]

theorem TdafSurface.supportFn_flip_pairing {n : ℕ} (s : Set (Rn n)) : Tdaf.ConvexAnalysis.supportFn (pairing n).flip s = Tdaf.ConvexAnalysis.supportFn (pairing n) s

@[simp]

theorem TdafSurface.polarCone_flip_pairing {n : ℕ} (K : Set (Rn n)) : Tdaf.ConvexAnalysis.polarCone (pairing n).flip K = Tdaf.ConvexAnalysis.polarCone (pairing n) K

@[simp]

theorem TdafSurface.polarSet_flip_pairing {n : ℕ} (C : Set (Rn n)) : Tdaf.ConvexAnalysis.polarSet (pairing n).flip C = Tdaf.ConvexAnalysis.polarSet (pairing n) C

@[simp]

theorem TdafSurface.polarGauge_flip_pairing {n : ℕ} (k : Rn n → EReal) : Tdaf.ConvexAnalysis.polarGauge (pairing n).flip k = Tdaf.ConvexAnalysis.polarGauge (pairing n) k

@[simp]

theorem TdafSurface.polarFn_flip_pairing {n : ℕ} (f : Rn n → EReal) : Tdaf.ConvexAnalysis.polarFn (pairing n).flip f = Tdaf.ConvexAnalysis.polarFn (pairing n) f

The vector picture of a linear function

A book writes a linear function on ℝⁿ as ⟨·, b⟩ and quantifies over the vector b; the backbone quantifies over a continuous linear functional, which is what separation produces.

noncomputable def TdafSurface.linFn {n : ℕ} (b : Rn n) : Rn n →L[ℝ] ℝ

The vector b read as the linear function ⟨·, b⟩.

Equations

• TdafSurface.linFn b = (innerSL ℝ) b

@[simp]

theorem TdafSurface.linFn_apply {n : ℕ} (b x : Rn n) : (linFn b) x = ((pairing n) x) b

theorem TdafSurface.linFn_eq_zero_iff {n : ℕ} {b : Rn n} : linFn b = 0 ↔ b = 0

⟨·, b⟩ is the zero function exactly when b is the zero vector: this is what makes b ≠ 0 and "{x | ⟨x, b⟩ = β} is a hyperplane" the same condition.

theorem TdafSurface.exists_linFn {n : ℕ} (f : Rn n →L[ℝ] ℝ) : ∃ (b : Rn n), linFn b = f

Every continuous linear function on ℝⁿ is ⟨·, b⟩. This Fréchet–Riesz identification is what lets a surface statement quantify over vectors while its proof quantifies over functionals.

theorem TdafSurface.linFn_eq_toDual {n : ℕ} (b : Rn n) : linFn b = (InnerProductSpace.toDual ℝ (Rn n)) b

linFn is the Fréchet–Riesz map, so the surface's vector-to-functional translation and the one the backbone's gradient results are stated against are the same map.

theorem TdafSurface.toDual_apply_eq_pairing {n : ℕ} (v x : Rn n) : ((InnerProductSpace.toDual ℝ (Rn n)) v) x = ((pairing n) x) v

The Riesz representative of v evaluated at x is the book's ⟨x, v⟩. Every backbone result about HasGradientAt produces the left-hand side, and every surface statement wants the right.

The canonical adjoint

Between arbitrarily paired spaces a transpose need not exist, so the backbone keeps the adjoint as data. On ℝⁿ it is canonical, and isAdjointPair_adjoint already covers innerₗ (Rn n): a surface section writes A* as LinearMap.adjoint A and discharges the hypothesis with it.