From b06d228536034fccebd3579653baca3f7bc9c23b Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Mon, 24 Oct 2022 21:05:23 +0000 Subject: [PATCH] feat(analysis/normed_space/operator_norm): characterize the operator norm over a `densely_normed_field` in terms of the supremum (#16963) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This provides a few results pertaining to the operator norm over a `densely_normed_field`. In particular, if `0 ≤ r < ∥f∥` then there exists some `x` with `∥x∥ ≤ 1` such that `r < ∥f x∥`. Consequently, the operator norm is the supremum of the norm of the image of the unit ball under `f`. --- src/analysis/normed_space/operator_norm.lean | 82 ++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean index 44fcf1655e801..fc6a658ee48c5 100644 --- a/src/analysis/normed_space/operator_norm.lean +++ b/src/analysis/normed_space/operator_norm.lean @@ -463,6 +463,88 @@ lipschitz_with_iff_norm_sub_le.2 $ λ f g, ((f - g).le_op_norm x).trans_eq (mul_ end +section Sup + +variables [ring_hom_isometric σ₁₂] + +lemma exists_mul_lt_apply_of_lt_op_nnnorm (f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ∥f∥₊) : + ∃ x, r * ∥x∥₊ < ∥f x∥₊ := +by simpa only [not_forall, not_le, set.mem_set_of] using not_mem_of_lt_cInf + (nnnorm_def f ▸ hr : r < Inf {c : ℝ≥0 | ∀ x, ∥f x∥₊ ≤ c * ∥x∥₊}) (order_bot.bdd_below _) + +lemma exists_mul_lt_of_lt_op_norm (f : E →SL[σ₁₂] F) {r : ℝ} (hr₀ : 0 ≤ r) (hr : r < ∥f∥) : + ∃ x, r * ∥x∥ < ∥f x∥ := +by { lift r to ℝ≥0 using hr₀, exact f.exists_mul_lt_apply_of_lt_op_nnnorm hr } + +lemma exists_lt_apply_of_lt_op_nnnorm {𝕜 𝕜₂ E F : Type*} [normed_add_comm_group E] + [seminormed_add_comm_group F] [densely_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] + {σ₁₂ : 𝕜 →+* 𝕜₂} [normed_space 𝕜 E] [normed_space 𝕜₂ F] [ring_hom_isometric σ₁₂] + (f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ∥f∥₊) : ∃ x : E, ∥x∥₊ < 1 ∧ r < ∥f x∥₊ := +begin + obtain ⟨y, hy⟩ := f.exists_mul_lt_apply_of_lt_op_nnnorm hr, + have hy' : ∥y∥₊ ≠ 0 := nnnorm_ne_zero_iff.2 + (λ heq, by simpa only [heq, nnnorm_zero, map_zero, not_lt_zero'] using hy), + have hfy : ∥f y∥₊ ≠ 0 := (zero_le'.trans_lt hy).ne', + rw [←inv_inv (∥f y∥₊), nnreal.lt_inv_iff_mul_lt (inv_ne_zero hfy), mul_assoc, mul_comm (∥y∥₊), + ←mul_assoc, ←nnreal.lt_inv_iff_mul_lt hy'] at hy, + obtain ⟨k, hk₁, hk₂⟩ := normed_field.exists_lt_nnnorm_lt 𝕜 hy, + refine ⟨k • y, (nnnorm_smul k y).symm ▸ (nnreal.lt_inv_iff_mul_lt hy').1 hk₂, _⟩, + have : ∥σ₁₂ k∥₊ = ∥k∥₊ := subtype.ext ring_hom_isometric.is_iso, + rwa [map_smulₛₗ f, nnnorm_smul, ←nnreal.div_lt_iff hfy, div_eq_mul_inv, this], +end + +lemma exists_lt_apply_of_lt_op_norm {𝕜 𝕜₂ E F : Type*} [normed_add_comm_group E] + [seminormed_add_comm_group F] [densely_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] + {σ₁₂ : 𝕜 →+* 𝕜₂} [normed_space 𝕜 E] [normed_space 𝕜₂ F] [ring_hom_isometric σ₁₂] + (f : E →SL[σ₁₂] F) {r : ℝ} (hr : r < ∥f∥) : ∃ x : E, ∥x∥ < 1 ∧ r < ∥f x∥ := +begin + by_cases hr₀ : r < 0, + { exact ⟨0, by simpa using hr₀⟩, }, + { lift r to ℝ≥0 using not_lt.1 hr₀, + exact f.exists_lt_apply_of_lt_op_nnnorm hr, } +end + +lemma Sup_unit_ball_eq_nnnorm {𝕜 𝕜₂ E F : Type*} [normed_add_comm_group E] + [seminormed_add_comm_group F] [densely_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] + {σ₁₂ : 𝕜 →+* 𝕜₂} [normed_space 𝕜 E] [normed_space 𝕜₂ F] [ring_hom_isometric σ₁₂] + (f : E →SL[σ₁₂] F) : Sup ((λ x, ∥f x∥₊) '' ball 0 1) = ∥f∥₊ := +begin + refine cSup_eq_of_forall_le_of_forall_lt_exists_gt ((nonempty_ball.mpr zero_lt_one).image _) + _ (λ ub hub, _), + { rintro - ⟨x, hx, rfl⟩, + simpa only [mul_one] using f.le_op_norm_of_le (mem_ball_zero_iff.1 hx).le }, + { obtain ⟨x, hx, hxf⟩ := f.exists_lt_apply_of_lt_op_nnnorm hub, + exact ⟨_, ⟨x, mem_ball_zero_iff.2 hx, rfl⟩, hxf⟩ }, +end + +lemma Sup_unit_ball_eq_norm {𝕜 𝕜₂ E F : Type*} [normed_add_comm_group E] + [seminormed_add_comm_group F] [densely_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] + {σ₁₂ : 𝕜 →+* 𝕜₂} [normed_space 𝕜 E] [normed_space 𝕜₂ F] [ring_hom_isometric σ₁₂] + (f : E →SL[σ₁₂] F) : Sup ((λ x, ∥f x∥) '' ball 0 1) = ∥f∥ := +by simpa only [nnreal.coe_Sup, set.image_image] using nnreal.coe_eq.2 f.Sup_unit_ball_eq_nnnorm + +lemma Sup_closed_unit_ball_eq_nnnorm {𝕜 𝕜₂ E F : Type*} [normed_add_comm_group E] + [seminormed_add_comm_group F] [densely_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] + {σ₁₂ : 𝕜 →+* 𝕜₂} [normed_space 𝕜 E] [normed_space 𝕜₂ F] [ring_hom_isometric σ₁₂] + (f : E →SL[σ₁₂] F) : Sup ((λ x, ∥f x∥₊) '' closed_ball 0 1) = ∥f∥₊ := +begin + have hbdd : ∀ y ∈ (λ x, ∥f x∥₊) '' closed_ball 0 1, y ≤ ∥f∥₊, + { rintro - ⟨x, hx, rfl⟩, exact f.unit_le_op_norm x (mem_closed_ball_zero_iff.1 hx) }, + refine le_antisymm (cSup_le ((nonempty_closed_ball.mpr zero_le_one).image _) hbdd) _, + rw ←Sup_unit_ball_eq_nnnorm, + exact cSup_le_cSup ⟨∥f∥₊, hbdd⟩ ((nonempty_ball.2 zero_lt_one).image _) + (set.image_subset _ ball_subset_closed_ball), +end + +lemma Sup_closed_unit_ball_eq_norm {𝕜 𝕜₂ E F : Type*} [normed_add_comm_group E] + [seminormed_add_comm_group F] [densely_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] + {σ₁₂ : 𝕜 →+* 𝕜₂} [normed_space 𝕜 E] [normed_space 𝕜₂ F] [ring_hom_isometric σ₁₂] + (f : E →SL[σ₁₂] F) : Sup ((λ x, ∥f x∥) '' closed_ball 0 1) = ∥f∥ := +by simpa only [nnreal.coe_Sup, set.image_image] using nnreal.coe_eq.2 + f.Sup_closed_unit_ball_eq_nnnorm + +end Sup + section lemma op_norm_ext [ring_hom_isometric σ₁₃] (f : E →SL[σ₁₂] F) (g : E →SL[σ₁₃] G)