homothety_norm — Mathlib

English

If ∀ x, ‖f x‖ = a‖x‖ for some a ≥ 0, then the operator norm of f is a.

Русский

Если для всех x верно ‖f x‖ = a‖x‖, то операторная норма f равна a.

LaTeX

$$$\\forall x:\\, \\|f x\\| = a \\|x\\| \\implies \\|f\\| = a.$$$

Lean4

theorem homothety_norm [RingHomIsometric σ₁₂] [Nontrivial E] (f : E →SL[σ₁₂] F) {a : ℝ} (hf : ∀ x, ‖f x‖ = a * ‖x‖) :
    ‖f‖ = a := by
  obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0
  rw [← norm_pos_iff] at hx
  have ha : 0 ≤ a := by simpa only [hf, hx, mul_nonneg_iff_of_pos_right] using norm_nonneg (f x)
  apply le_antisymm (f.opNorm_le_bound ha fun y => le_of_eq (hf y))
  simpa only [hf, hx, mul_le_mul_iff_left₀] using f.le_opNorm x

Похожие утверждения