Symmetric gauges of square specializations

Diagonal evaluation and operator absolute value use endomorphisms. They specialize the rectangular seminorm to identical domain and codomain; there is no square structure.

The symmetric gauge

noncomputable def TauCeti.UnitarilyInvariantSeminorm.gauge {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) (x : Fin n → ℝ) : ℝ

The symmetric gauge of a unitarily invariant norm relative to an orthonormal basis b: the norm of the diagonal operator with diagonal x. Defined on all real vectors, not only sorted nonnegative ones — the T-transform descent exploits its subadditivity, homogeneity, permutation invariance, and single-coordinate sign invariance on arbitrary vectors.

Equations

• N.gauge b x = N (TauCeti.diagOp b x)

theorem TauCeti.UnitarilyInvariantSeminorm.gauge_add_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) (x y : Fin n → ℝ) : N.gauge b (x + y) ≤ N.gauge b x + N.gauge b y

The induced vector gauge is subadditive, inherited from the norm through diagOp_add.

theorem TauCeti.UnitarilyInvariantSeminorm.gauge_real_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) (c : ℝ) (x : Fin n → ℝ) : N.gauge b (c • x) = |c| * N.gauge b x

The induced vector gauge is absolutely homogeneous over ℝ.

theorem TauCeti.UnitarilyInvariantSeminorm.gauge_perm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) (x : Fin n → ℝ) (π : Equiv.Perm (Fin n)) : N.gauge b (x ∘ ⇑π) = N.gauge b x

Permutation invariance of the gauge: conjugating the diagonal operator by the basis-permutation unitary permutes the diagonal.

theorem TauCeti.UnitarilyInvariantSeminorm.gauge_neg_single {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) (x : Fin n → ℝ) (j : Fin n) : N.gauge b (Function.update x j (-x j)) = N.gauge b x

Single-coordinate sign flip invariance of the gauge: flipping the sign of the j-th diagonal entry composes the diagonal operator with the reflection through (𝕜 ∙ b j)ᗮ, a unitary.

theorem TauCeti.UnitarilyInvariantSeminorm.apply_eq_gauge {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (hn : Module.finrank 𝕜 E = n) (b : OrthonormalBasis (Fin n) 𝕜 E) (A : E →ₗ[𝕜] E) : N A = N.gauge b fun (i : Fin n) => A.singularValues ↑i

The gauge representation: a unitarily invariant norm is the gauge of the singular values, via the operator SVD.

Monotonicity of the gauge

noncomputable def TauCeti.UnitarilyInvariantSeminorm.finiteSymmetricGauge {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) : FiniteSymmetricGauge n

The gauge of a unitarily invariant norm, packaged as a FiniteSymmetricGauge. Its four fields are exactly gauge_add_le, gauge_real_smul, gauge_perm and gauge_neg_single, which is what makes the Hardy--Littlewood--Pólya transfer theory (ForTauCeti.Analysis.Convex.Majorization) apply verbatim: everything below is that theory read through this packaging, not a second proof of it.

Equations

• N.finiteSymmetricGauge b = { toFun := N.gauge b, add_le' := ⋯, real_smul' := ⋯, perm' := ⋯, neg_single' := ⋯ }

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.finiteSymmetricGauge_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) (x : Fin n → ℝ) : (N.finiteSymmetricGauge b).toFun x = N.gauge b x

The induced finite symmetric gauge, unfolded.

theorem TauCeti.UnitarilyInvariantSeminorm.gauge_update_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) {y : Fin n → ℝ} {j : Fin n} {t : ℝ} (ht : |t| ≤ y j) : N.gauge b (Function.update y j t) ≤ N.gauge b y

Shrinking one coordinate of y (in absolute value) does not increase the gauge: update y j t with |t| ≤ y j is a convex combination of y and its j-th sign flip.

theorem TauCeti.UnitarilyInvariantSeminorm.gauge_mono {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) {x y : Fin n → ℝ} (hx0 : ∀ (i : Fin n), 0 ≤ x i) (hxy : ∀ (i : Fin n), x i ≤ y i) : N.gauge b x ≤ N.gauge b y

Coordinatewise monotonicity of the gauge on nonnegative vectors.

The T-transform descent

theorem TauCeti.UnitarilyInvariantSeminorm.gauge_le_gauge_of_prefix_sums_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (N : UnitarilyInvariantSeminorm 𝕜 E E) (b : OrthonormalBasis (Fin n) 𝕜 E) {z y : Fin n → ℝ} (hz_anti : Antitone z) (hz0 : ∀ (i : Fin n), 0 ≤ z i) (hy0 : ∀ (i : Fin n), 0 ≤ y i) (hpre : ∀ (m : ℕ), ∑ i : Fin n with ↑i < m, z i ≤ ∑ i : Fin n with ↑i < m, y i) : N.gauge b z ≤ N.gauge b y

The T-transform descent on the gauge — the engine of Fan dominance. If z is antitone and nonnegative, y is nonnegative, and every prefix sum of z is dominated by the corresponding prefix sum of y, then Φ_N(z) ≤ Φ_N(y).

No total-sum equality is assumed, no majorization completion and no separation theorem is used: this is TauCeti.FiniteSymmetricGauge.le_of_prefixSum_le, whose descent averages y with a transposition of itself, at a cost of one triangle inequality, one homogeneity, and one swap invariance of the gauge per step.

The Fan dominance principle

theorem TauCeti.UnitarilyInvariantSeminorm.apply_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (N : UnitarilyInvariantSeminorm 𝕜 E E) (A : E →ₗ[𝕜] E) : N (LinearMap.adjoint A) = N A

A square seminorm is unchanged by taking the adjoint.

theorem TauCeti.UnitarilyInvariantSeminorm.apply_operatorAbs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (N : UnitarilyInvariantSeminorm 𝕜 E E) (A : E →ₗ[𝕜] E) : N (operatorAbs A) = N A

A square seminorm is unchanged by taking the operator absolute value.