Topologies from matrix norms

This file exposes the topology underlying Mathlib's L∞ operator norm on finite matrices. Since matrix norms are scoped, consumers can select this topology locally without reconstructing the instance projection chain.

Mathlib's ContinuousStar instance for matrices is stated for the entrywise topology, which is the same topology but not the same instance, so continuity of the conjugate transpose has to be restated for the topology selected here.

Main definitions

• Matrix.linftyOpTopologicalSpace: the topology induced by the L∞ operator norm.
• Matrix.linftyOpContinuousStar: conjugate transposition is continuous for that topology.

@[reducible, inline]

noncomputable abbrev Matrix.linftyOpTopologicalSpace (m : Type u_1) (n : Type u_2) [Fintype m] [Fintype n] (α : Type u_3) [NormedAddCommGroup α] : TopologicalSpace (Matrix m n α)

The topology underlying the L∞ operator norm on finite matrices.

Equations

• Matrix.linftyOpTopologicalSpace m n α = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

@[reducible, inline]

abbrev Matrix.linftyOpContinuousStar (n : Type u_1) [Fintype n] (α : Type u_2) [NormedAddCommGroup α] [Star α] [ContinuousStar α] : ContinuousStar (Matrix n n α)

Conjugate transposition is continuous for the topology of the L∞ operator norm.

Equations

• ⋯ = ⋯