[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
E : Type u_2
inst✝ : NormedAddCommGroup E
z : E
⊢ ‖↑‖z‖‖ = ‖z‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1
[PROOFSTEP]
have : ‖x‖ ≠ 0 := by simp [hx]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1
[PROOFSTEP]
field_simp [norm_smul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r
[PROOFSTEP]
have : ‖x‖ ≠ 0 := by simp [hx]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r
[PROOFSTEP]
field_simp [norm_smul, r_nonneg, isROrC_simps]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
by_cases z_zero : z = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
rw [z_zero]
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖↑f 0‖ ≤ c / r * ‖0‖
[PROOFSTEP]
simp only [LinearMap.map_zero, norm_zero, mul_zero]
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ 0 ≤ 0
[PROOFSTEP]
exact le_rfl
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
set z₁ := ((r : 𝕜) * (‖z‖ : 𝕜)⁻¹) • z with hz₁
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
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
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖↑f z₁‖ ≤ c
[PROOFSTEP]
apply h
[GOAL]
case a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ z₁ ∈ sphere 0 r
[PROOFSTEP]
rw [mem_sphere_zero_iff_norm]
[GOAL]
case a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖z₁‖ = r
[PROOFSTEP]
exact norm_smul_inv_norm' r_pos.le z_zero
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
have r_ne_zero : (r : 𝕜) ≠ 0 := IsROrC.ofReal_ne_zero.mpr r_pos.ne'
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
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, IsROrC.ofReal_eq_zero, norm_eq_zero, Ne.def, not_false_iff]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑f z = ↑‖z‖ / ↑r * ↑f z₁
[PROOFSTEP]
rw [hz₁, LinearMap.map_smul, smul_eq_mul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑f z = ↑‖z‖ / ↑r * (↑r * (↑‖z‖)⁻¹ * ↑f z)
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc, div_mul_cancel _ r_ne_zero, mul_inv_cancel, one_mul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑‖z‖ ≠ 0
[PROOFSTEP]
simp only [z_zero, IsROrC.ofReal_eq_zero, norm_eq_zero, Ne.def, not_false_iff]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
[PROOFSTEP]
rw [eq, norm_mul, norm_div, IsROrC.norm_coe_norm, IsROrC.norm_of_nonneg r_pos.le, div_mul_eq_mul_div,
  div_mul_eq_mul_div, mul_comm]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z₁‖ * ‖z‖ / r ≤ c * ‖z‖ / r
[PROOFSTEP]
apply div_le_div _ _ r_pos rfl.ge
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ 0 ≤ c * ‖z‖
[PROOFSTEP]
exact mul_nonneg ((norm_nonneg _).trans norm_f_z₁) (norm_nonneg z)
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z₁‖ * ‖z‖ ≤ c * ‖z‖
[PROOFSTEP]
apply mul_le_mul norm_f_z₁ rfl.le (norm_nonneg z) ((norm_nonneg _).trans norm_f_z₁)
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ ‖f‖ ≤ c / r
[PROOFSTEP]
apply ContinuousLinearMap.op_norm_le_bound
[GOAL]
case hMp
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ 0 ≤ c / r
[PROOFSTEP]
apply div_nonneg _ r_pos.le
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ 0 ≤ c
[PROOFSTEP]
exact (norm_nonneg _).trans (h 0 (by simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]))
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ 0 ∈ closedBall 0 r
[PROOFSTEP]
simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]
[GOAL]
case hM
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ ∀ (x : E), ‖↑f x‖ ≤ c / r * ‖x‖
[PROOFSTEP]
apply LinearMap.bound_of_ball_bound' r_pos
[GOAL]
case hM.h
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ (z : E), z ∈ closedBall 0 r → ‖↑f z‖ ≤ c
⊢ ∀ (z : E), z ∈ closedBall 0 r → ‖↑↑f z‖ ≤ c
[PROOFSTEP]
exact fun z hz => h z hz
