feat(analysis/normed_space/operator_norm): characterize the operator norm over a densely_normed_field in terms of the supremum (#16963)

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`.

Author: j-loreaux

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)