Self-pairings of inner-product type

A pairing of a space with itself that is symmetric and positive definite behaves like an inner product in every way the theory needs, without carrying a NormedAddCommGroup structure of its own. That matters because Moreau's theorem gets applied on U × X, which carries the supremum norm and so has no InnerProductSpace ℝ instance, even though prodPairing (innerₗ U) (innerₗ X) is a perfectly good inner product on it. Moving to WithLp 2 (U × X) instead would replace the topology instance, so ClosedFn, Continuous and IsClosed would stop transferring definitionally; generalising the pairing costs one class and leaves the topology alone.

Main definitions

• IsInnerPairing B — B is symmetric, positive semidefinite, and definite.
• IsContinuousInnerPairing B — an inner pairing whose quadratic form x ↦ B x x is continuous. This is the only topological fact Moreau's theorem needs, and it holds for innerₗ E on any real inner-product space, with no finite-dimensionality.
• pairingNorm B x — the induced norm √(B x x).

Main results

• self_pairing_add, self_pairing_sub, self_pairing_combo_le — the quadratic expansions, and convexity of ½ B z z with its defect visible. These replace norm_add_sq_real and friends.
• pairing_sq_le_mul — Cauchy–Schwarz for a positive semidefinite symmetric form. Only self_nonneg is used, not definiteness: the proof splits on B y y = 0, and semidefiniteness alone forces B x y = 0 in that branch.
• pairingNorm_add_le — the triangle inequality, so pairingNorm is a genuine norm.
• exists_pairingNorm_le_and_le_pairingNorm — in finite dimensions the induced norm is equivalent to the ambient one, so nothing stated through pairingNorm says anything new about the topology.

Implementation notes

IsInnerPairing is a Prop-class rather than a structure carrying data: the form B is already a LinearMap, and the class only records the three properties, so an inner-product space's own innerₗ E picks the instance up automatically. Definiteness is stated as B x x = 0 → x = 0, which is the form proofs apply; self_pos supplies the other.

No InnerProductSpace instance is manufactured from IsInnerPairing: doing so through InnerProductSpace.ofCore would produce a second NormedAddCommGroup on E, which is the clash this module exists to avoid.

class Tdaf.ConvexAnalysis.IsInnerPairing {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : Prop

A pairing of E with itself that is symmetric and positive definite — an inner product in all but the NormedAddCommGroup structure.

• pairing_comm (x y : E) : (B x) y = (B y) x

  The pairing is symmetric.

• self_nonneg (x : E) : 0 ≤ (B x) x

  The pairing is positive semidefinite.

• eq_zero_of_self_eq_zero (x : E) : (B x) x = 0 → x = 0

  The pairing is definite.

theorem Tdaf.ConvexAnalysis.pairing_comm {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] (x y : E) : (B x) y = (B y) x

theorem Tdaf.ConvexAnalysis.self_pairing_nonneg {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] (x : E) : 0 ≤ (B x) x

@[simp]

theorem Tdaf.ConvexAnalysis.flip_eq_self {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] : B.flip = B

A symmetric pairing is its own flip. This is what lets closedFn_conj — which asks for IsContinuousPairing B.flip — be applied to an inner pairing without a detour.

@[simp]

theorem Tdaf.ConvexAnalysis.self_pairing_eq_zero_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] {x : E} : (B x) x = 0 ↔ x = 0

theorem Tdaf.ConvexAnalysis.self_pairing_pos {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] {x : E} (hx : x ≠ 0) : 0 < (B x) x

Positive definiteness in the form the analysis uses.

theorem Tdaf.ConvexAnalysis.self_pairing_add_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] (t : ℝ) (x y : E) : (B (x + t • y)) (x + t • y) = (B x) x + 2 * t * (B x) y + t ^ 2 * (B y) y

The quadratic expansion the discriminant argument runs on.

Expansions

The quadratic identities ‖x ± y‖² = ‖x‖² ± 2⟪x, y⟫ + ‖y‖² and their companions.

theorem Tdaf.ConvexAnalysis.self_pairing_add {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] (x y : E) : (B (x + y)) (x + y) = (B x) x + 2 * (B x) y + (B y) y

theorem Tdaf.ConvexAnalysis.self_pairing_sub {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] (x y : E) : (B (x - y)) (x - y) = (B x) x - 2 * (B x) y + (B y) y

@[simp]

theorem Tdaf.ConvexAnalysis.self_pairing_neg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} (x : E) : (B (-x)) (-x) = (B x) x

theorem Tdaf.ConvexAnalysis.self_pairing_sub_rev {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} (x y : E) : (B (x - y)) (x - y) = (B (y - x)) (y - x)

theorem Tdaf.ConvexAnalysis.self_pairing_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} (a : ℝ) (x : E) : (B (a • x)) (a • x) = a ^ 2 * (B x) x

theorem Tdaf.ConvexAnalysis.self_pairing_combo_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] {u v : E} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : (B (a • u + b • v)) (a • u + b • v) / 2 ≤ a * ((B u) u / 2) + b * ((B v) v / 2)

Convexity of the quadratic form, with the defect a b B (u - v) (u - v) ≥ 0 visible. This is the one inequality that makes w z = ½ B z z a convex function.

theorem Tdaf.ConvexAnalysis.pairing_sq_le_mul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] (x y : E) : (B x) y ^ 2 ≤ (B x) x * (B y) y

Cauchy–Schwarz for a symmetric positive semidefinite pairing. Definiteness is not used.

noncomputable def Tdaf.ConvexAnalysis.pairingNorm {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (x : E) : ℝ

The norm induced by the pairing, √(B x x).

Equations

• Tdaf.ConvexAnalysis.pairingNorm B x = √((B x) x)

theorem Tdaf.ConvexAnalysis.pairingNorm_nonneg {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (x : E) : 0 ≤ pairingNorm B x

@[simp]

theorem Tdaf.ConvexAnalysis.pairingNorm_sq {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] (x : E) : pairingNorm B x ^ 2 = (B x) x

@[simp]

theorem Tdaf.ConvexAnalysis.pairingNorm_eq_zero_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] {x : E} : pairingNorm B x = 0 ↔ x = 0

@[simp]

theorem Tdaf.ConvexAnalysis.pairingNorm_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] : pairingNorm B 0 = 0

theorem Tdaf.ConvexAnalysis.pairingNorm_neg {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] (x : E) : pairingNorm B (-x) = pairingNorm B x

theorem Tdaf.ConvexAnalysis.pairing_le_pairingNorm_mul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] (x y : E) : (B x) y ≤ pairingNorm B x * pairingNorm B y

Cauchy–Schwarz in norm form.

theorem Tdaf.ConvexAnalysis.pairingNorm_add_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] (x y : E) : pairingNorm B (x + y) ≤ pairingNorm B x + pairingNorm B y

The triangle inequality: pairingNorm B is a norm.

theorem Tdaf.ConvexAnalysis.pairingNorm_sub_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] (x y z : E) : pairingNorm B (x - z) ≤ pairingNorm B (x - y) + pairingNorm B (y - z)

Inner pairings with a continuous quadratic form

class Tdaf.ConvexAnalysis.IsContinuousInnerPairing {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) extends Tdaf.ConvexAnalysis.IsInnerPairing B : Prop

An inner pairing whose quadratic form is continuous. This does not follow from IsContinuousPairing, which gives continuity only in the first variable with the second held fixed.

• pairing_comm (x y : E) : (B x) y = (B y) x
• self_nonneg (x : E) : 0 ≤ (B x) x
• eq_zero_of_self_eq_zero (x : E) : (B x) x = 0 → x = 0
• continuous_self : Continuous fun (x : E) => (B x) x

  The quadratic form is continuous.

theorem Tdaf.ConvexAnalysis.continuous_self_pairing' {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsContinuousInnerPairing B] : Continuous fun (x : E) => (B x) x

@[instance 100]

instance Tdaf.ConvexAnalysis.isContinuousPairing_of_isContinuousInnerPairing {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsContinuousInnerPairing B] : IsContinuousPairing B

Polarization makes the diagonal do all the work: a symmetric form whose quadratic form is continuous is continuous in each variable separately, so IsContinuousInnerPairing subsumes IsContinuousPairing.

instance Tdaf.ConvexAnalysis.isContinuousPairing_flip_of_isContinuousInnerPairing {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsContinuousInnerPairing B] : IsContinuousPairing B.flip

The flip of an inner pairing is continuous, which instance search cannot see through LinearMap.flip on its own.

instance Tdaf.ConvexAnalysis.isCompatiblePairing_flip_of_isInnerPairing {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] [IsCompatiblePairing B] : IsCompatiblePairing B.flip

The flip of a compatible inner pairing is compatible: for a symmetric pairing the two conditions coincide.

The inner product of an inner-product space

instance Tdaf.ConvexAnalysis.isInnerPairing_innerL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsInnerPairing (innerₗ E)

The inner product of a real inner-product space is an inner pairing.

@[simp]

theorem Tdaf.ConvexAnalysis.pairingNorm_innerL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : pairingNorm (innerₗ E) x = ‖x‖

instance Tdaf.ConvexAnalysis.isContinuousInnerPairing_innerL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsContinuousInnerPairing (innerₗ E)

The inner product of a real inner-product space has a continuous quadratic form, ‖·‖ ^ 2, with no finite-dimensionality needed.

Products

instance Tdaf.ConvexAnalysis.isInnerPairing_prodPairing {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {Bu : U →ₗ[ℝ] U →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] X →ₗ[ℝ] ℝ} [IsInnerPairing Bu] [IsInnerPairing Bx] : IsInnerPairing (prodPairing Bu Bx)

A product of inner pairings is an inner pairing: U × X has no InnerProductSpace structure, but prodPairing (innerₗ U) (innerₗ X) is an inner pairing on it.

instance Tdaf.ConvexAnalysis.isContinuousInnerPairing_prodPairing {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {Bu : U →ₗ[ℝ] U →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] X →ₗ[ℝ] ℝ} [TopologicalSpace U] [TopologicalSpace X] [IsContinuousInnerPairing Bu] [IsContinuousInnerPairing Bx] : IsContinuousInnerPairing (prodPairing Bu Bx)

A product of continuous inner pairings has a continuous quadratic form.

Equivalence with the ambient norm, in finite dimensions

theorem Tdaf.ConvexAnalysis.continuous_self_pairing {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} : Continuous fun (x : E) => (B x) x

x ↦ B x x is continuous, being a continuous bilinear form evaluated on the diagonal. No IsContinuousPairing hypothesis is needed, since in finite dimensions every linear map out of E is continuous.

@[instance 100]

instance Tdaf.ConvexAnalysis.isContinuousInnerPairing_of_finiteDimensional {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] : IsContinuousInnerPairing B

In finite dimensions every inner pairing has a continuous quadratic form.

theorem Tdaf.ConvexAnalysis.continuous_pairingNorm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} : Continuous (pairingNorm B)

pairingNorm B is continuous.

theorem Tdaf.ConvexAnalysis.exists_pairingNorm_le_and_le_pairingNorm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) [IsInnerPairing B] : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ 0 < C ∧ (∀ (x : E), c * ‖x‖ ≤ pairingNorm B x) ∧ ∀ (x : E), pairingNorm B x ≤ C * ‖x‖

The induced norm is equivalent to the ambient one. Positive definiteness makes B x x strictly positive on the unit sphere, which is compact in finite dimensions, so it has a positive minimum and a finite maximum there; homogeneity spreads both bounds over all of E.