English
If a linear map f is bounded on the sphere of radius r, then it is globally bounded by a proportional bound: ∥f z∥ ≤ (c/r) ∥z∥ for all z, given ∥f z∥ ≤ c on the sphere.
Русский
Если линейное отображение f ограничено на сфере радиуса r, то существует константа c, такая что для всех z выполняется ∥f z∥ ≤ (c/r) ∥z∥.
LaTeX
$$$\\forall z, \\|f z\\| \\le \\frac{c}{r} \\|z\\|$$$
Lean4
theorem bound_of_sphere_bound {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ z ∈ sphere (0 : E) r, ‖f z‖ ≤ c)
(z : E) : ‖f z‖ ≤ c / r * ‖z‖ := by
by_cases z_zero : z = 0
· rw [z_zero]
simp only [LinearMap.map_zero, norm_zero, mul_zero]
exact le_rfl
set z₁ := ((r : 𝕜) * (‖z‖ : 𝕜)⁻¹) • z with hz₁
have norm_f_z₁ : ‖f z₁‖ ≤ c := by
apply h
rw [mem_sphere_zero_iff_norm]
exact norm_smul_inv_norm' r_pos.le z_zero
have r_ne_zero : (r : 𝕜) ≠ 0 := RCLike.ofReal_ne_zero.mpr r_pos.ne'
have eq : f z = ‖z‖ / r * f z₁ := by
rw [hz₁, LinearMap.map_smul, smul_eq_mul]
rw [← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ r_ne_zero, mul_inv_cancel₀, one_mul]
simp only [z_zero, RCLike.ofReal_eq_zero, norm_eq_zero, Ne, not_false_iff]
rw [eq, norm_mul, norm_div, RCLike.norm_coe_norm, RCLike.norm_of_nonneg r_pos.le, div_mul_eq_mul_div,
div_mul_eq_mul_div, mul_comm]
apply div_le_div₀ _ _ r_pos rfl.ge
· exact mul_nonneg ((norm_nonneg _).trans norm_f_z₁) (norm_nonneg z)
apply mul_le_mul norm_f_z₁ rfl.le (norm_nonneg z) ((norm_nonneg _).trans norm_f_z₁)
