From c6529053211bed9dd64a3ad40836b30ff1e3eac9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 6 Jan 2024 05:23:43 +0000 Subject: [PATCH] fix(Analysis/NormedSpace/OperatorNorm): muddled norm and nnnorm (#9473) This is a lemma about `nnnorm`, but it seems one of the arguments was forgotten. --- Mathlib/Analysis/NormedSpace/OperatorNorm.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean index 8a2d176302e92..72eae739234a7 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean @@ -370,7 +370,7 @@ theorem op_nnnorm_le_of_lipschitz {f : E →SL[σ₁₂] F} {K : ℝ≥0} (hf : op_norm_le_of_lipschitz hf #align continuous_linear_map.op_nnnorm_le_of_lipschitz ContinuousLinearMap.op_nnnorm_le_of_lipschitz -theorem op_nnnorm_eq_of_bounds {φ : E →SL[σ₁₂] F} (M : ℝ≥0) (h_above : ∀ x, ‖φ x‖ ≤ M * ‖x‖) +theorem op_nnnorm_eq_of_bounds {φ : E →SL[σ₁₂] F} (M : ℝ≥0) (h_above : ∀ x, ‖φ x‖₊ ≤ M * ‖x‖₊) (h_below : ∀ N, (∀ x, ‖φ x‖₊ ≤ N * ‖x‖₊) → M ≤ N) : ‖φ‖₊ = M := Subtype.ext <| op_norm_eq_of_bounds (zero_le M) h_above <| Subtype.forall'.mpr h_below #align continuous_linear_map.op_nnnorm_eq_of_bounds ContinuousLinearMap.op_nnnorm_eq_of_bounds