norm of a linear map from R

Stream: Is there code for X?

[Kevin Buzzard]

Do we have the following? (it's true, right?)

import analysis.normed_space.operator_norm

variables (F : Type) [normed_add_comm_group F] [normed_space ℝ F]
variable (f : ℝ →L[ℝ] F)

example : ‖f‖ = ‖f 1‖ :=
begin
  sorry,
end

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

import analysis.normed_space.operator_norm

variables (F : Type) [normed_add_comm_group F] [normed_space ℝ F]
variable (f : ℝ →L[ℝ] F)

example : ‖f‖ = ‖f 1‖ :=
begin
  refine le_antisymm (continuous_linear_map.op_norm_le_of_unit_norm (norm_nonneg _) (λ x hx, _))
    (f.unit_le_op_norm _ norm_one_class.norm_one.le),
  rw [real.norm_eq_abs, abs_eq (zero_le_one : (0 : ℝ) ≤ 1)] at hx,
  rcases hx with (rfl | rfl),
  { exact le_rfl },
  { simp only [map_neg, norm_neg] },
end

[Jireh Loreaux]

I don't think we have it exactly, but docs#continuous_linear_map.op_norm_le_of_unit_norm is the key result (relies on the fact that we have a normed space over ℝ).

[Jireh Loreaux]

Note that for a docs#densely_normed_field we also have the characterization of the operator norm in terms of the supremum over the unit ball (see docs#continuous_linear_map.Sup_closed_unit_ball_eq_norm and the things immediately above it).

[Jireh Loreaux]

@Kevin Buzzard you caused me to write up some other things we should probably have.

import analysis.normed_space.operator_norm

lemma metric.sphere_empty {E : Type*} [metric_space E] [subsingleton E]
  (x : E) {r : ℝ} (hr : 0 < r) : metric.sphere x r = ∅ :=
begin
  refine eq_bot_iff.mpr (λ y hy, _),
  rw metric.mem_sphere at hy,
  exact (dist_ne_zero.mp (hy.symm ▸ hr.ne' : dist y x ≠ 0) $ subsingleton.elim y x).elim,
end

@[simp]
lemma metric.unit_sphere_empty {E : Type*} [metric_space E] [subsingleton E]
  (x : E) : metric.sphere x 1 = ∅ :=
metric.sphere_empty x zero_lt_one

variables {E F : Type} [normed_add_comm_group E] [seminormed_add_comm_group F]
  [normed_space ℝ E] [normed_space ℝ F]

example (f : ℝ →L[ℝ] F) : ‖f‖ = ‖f 1‖ :=
begin
  refine le_antisymm (continuous_linear_map.op_norm_le_of_unit_norm (norm_nonneg _) (λ x hx, _))
    (f.unit_le_op_norm _ norm_one_class.norm_one.le),
  rw [real.norm_eq_abs, abs_eq (zero_le_one : (0 : ℝ) ≤ 1)] at hx,
  rcases hx with (rfl | rfl),
  { exact le_rfl },
  { simp only [map_neg, norm_neg] },
end

lemma norm_norm_inv_smul_self {x : E} (hx : x ≠ 0) : ‖(‖x‖⁻¹) • x‖ = 1 :=
by simpa only [norm_smul, norm_inv, norm_norm] using inv_mul_cancel (norm_pos_iff.mpr hx).ne'

lemma continuous_linear_map.Sup_unit_sphere_eq_norm (g : E →L[ℝ] F) :
  Sup ((λ x, ‖g x‖) '' metric.sphere 0 1) = ‖g‖ :=
begin
  casesI (subsingleton_or_nontrivial E),
  { simp, },
  have bdd : ‖g‖ ∈ upper_bounds ((λ x, ‖g x‖) '' metric.sphere 0 1),
  { rintro - ⟨x, hx, rfl⟩,
    exact g.unit_le_op_norm _ (mem_sphere_zero_iff_norm.mp hx).le, },
  refine le_antisymm (cSup_le (set.nonempty.image _ _) bdd) _,
  { obtain ⟨x, hx⟩ := exists_ne (0 : E),
    refine ⟨‖x‖⁻¹ • x, mem_sphere_zero_iff_norm.mpr (norm_norm_inv_smul_self hx)⟩ },
  { refine continuous_linear_map.op_norm_le_of_unit_norm (real.Sup_nonneg _ _)
      (λ x hx, le_cSup ⟨‖g‖, bdd⟩ ⟨x, mem_sphere_zero_iff_norm.mpr hx, rfl⟩),
    rintro _ ⟨_, _, rfl⟩,
    exact norm_nonneg _ },
end

lemma continuous_linear_map.Sup_unit_sphere_eq_nnnorm (g : E →L[ℝ] F) :
  Sup ((λ x, ‖g x‖₊) '' metric.sphere 0 1) = ‖g‖₊ :=
subtype.ext $ by simpa only [nnreal.coe_Sup, set.image_image] using g.Sup_unit_sphere_eq_norm

If you want to PR any of it that's fine. I won't have time until next week.