theorem dualNormDef_nonneg' {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Module.Dual ℝ E) : 0 ≤ DualNormDef s

DualNormDef is nonnegative.

theorem operatorNormDef_eq_sSup_dualNormDef_of_continuous {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) : have A' := { toFun := fun (x : E1) => ↑(A x), map_add' := ⋯, map_smul' := ⋯ }; OperatorNormDef A' = sSup {r : ℝ | ∃ (x : E1), ‖x‖ = 1 ∧ r = DualNormDef (A' x)}

For the linear map A' induced from A : E1 →L E2*, OperatorNormDef is the supremum of DualNormDef over unit vectors.

theorem operatorNormDef_eq_maxEntry_l1 (n m : ℕ) (A : (PiLp 1 fun (x : Fin n) => ℝ) →L[ℝ] (PiLp 1 fun (x : Fin m) => ℝ) →L[ℝ] ℝ) : have A' := { toFun := fun (x : PiLp 1 fun (x : Fin n) => ℝ) => ↑(A x), map_add' := ⋯, map_smul' := ⋯ }; have AEntry := fun (i : Fin n) (j : Fin m) => (A' ((PiLp.basisFun 1 ℝ (Fin n)) i)) ((PiLp.basisFun 1 ℝ (Fin m)) j); have maxEntry := sSup {r : ℝ | ∃ (i : Fin n) (j : Fin m), r = |AEntry i j|}; OperatorNormDef A' = maxEntry

For a continuous bilinear map A : ℓ¹ → (ℓ¹)* on finite-dimensional coordinate spaces, the operator norm ‖A‖_{1,2} is the maximum absolute entry of the induced matrix.