feat(analysis/normed_space/operator_norm): generalize linear_map.boun…

…d_of_ball_bound (#11140)

This was proved over `is_R_or_C` but holds (in a slightly different form) over all nondiscrete normed fields.



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

src/analysis/normed_space/dual.lean

@@ -252,7 +252,7 @@ begin
   intros x' h,
   simp only [mem_closed_ball_zero_iff],
   refine continuous_linear_map.op_norm_le_of_ball hr (inv_nonneg.mpr hr.le) (λ z hz, _),
-  simpa only [one_div] using linear_map.bound_of_ball_bound hr 1 x'.to_linear_map h z
+  simpa only [one_div] using linear_map.bound_of_ball_bound' hr 1 x'.to_linear_map h z
 end
 
 /-- Given a neighborhood `s` of the origin in a normed space `E`, the dual norms

src/analysis/normed_space/is_R_or_C.lean

@@ -71,7 +71,10 @@ begin
   apply mul_le_mul norm_f_z₁ rfl.le (norm_nonneg z) ((norm_nonneg _).trans norm_f_z₁),
 end
 
-lemma linear_map.bound_of_ball_bound {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜)
+/--
+`linear_map.bound_of_ball_bound` is a version of this over arbitrary nondiscrete normed fields.
+It produces a less precise bound so we keep both versions. -/
+lemma linear_map.bound_of_ball_bound' {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜)
   (h : ∀ z ∈ closed_ball (0 : E) r, ∥f z∥ ≤ c) (z : E) :
   ∥f z∥ ≤ c / r * ∥z∥ :=
 f.bound_of_sphere_bound r_pos c (λ z hz, h z hz.le) z
@@ -84,6 +87,6 @@ begin
   { apply div_nonneg _ r_pos.le,
     exact (norm_nonneg _).trans
           (h 0 (by simp only [norm_zero, mem_closed_ball, dist_zero_left, r_pos.le])), },
-  apply linear_map.bound_of_ball_bound r_pos,
+  apply linear_map.bound_of_ball_bound' r_pos,
   exact λ z hz, h z hz,
 end

src/analysis/normed_space/operator_norm.lean

@@ -1077,6 +1077,26 @@ begin
   exact linear_map.bound_of_shell_semi_normed f ε_pos hc hf (ne_of_lt (norm_pos_iff.2 hx)).symm
 end
 
+/--
+`linear_map.bound_of_ball_bound'` is a version of this lemma over a field satisfying `is_R_or_C`
+that produces a concrete bound.
+-/
+lemma linear_map.bound_of_ball_bound {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] Fₗ)
+  (h : ∀ z ∈ metric.ball (0 : E) r, ∥f z∥ ≤ c) :
+  ∃ C, ∀ (z : E), ∥f z∥ ≤ C * ∥z∥ :=
+begin
+  cases @nondiscrete_normed_field.non_trivial 𝕜 _ with k hk,
+  use c * (∥k∥ / r),
+  intro z,
+  refine linear_map.bound_of_shell _ r_pos hk (λ x hko hxo, _) _,
+  calc ∥f x∥ ≤ c : h _ (mem_ball_zero_iff.mpr hxo)
+         ... ≤ c * ((∥x∥ * ∥k∥) / r) : le_mul_of_one_le_right _ _
+         ... = _ : by ring,
+  { exact le_trans (norm_nonneg _) (h 0 (by simp [r_pos])) },
+  { rw [div_le_iff (zero_lt_one.trans hk)] at hko,
+    exact (one_le_div r_pos).mpr hko }
+end
+
 namespace continuous_linear_map
 
 section op_norm