[GOAL]
t : ℝ
⊢ ‖exp (↑t * I)‖ = 1
[PROOFSTEP]
simp only [norm_eq_abs, abs_exp_ofReal_mul_I]
[GOAL]
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
x : ℝ
h : r₁ < x ∧ x < r₂
⊢ r₁ < ‖↑x‖ ∧ ‖↑x‖ < r₂
[PROOFSTEP]
rwa [norm_eq_abs, abs_ofReal, abs_of_pos (h₀.trans_lt h.1)]
[GOAL]
R : Type u_1
inst✝¹ : NormedField R
inst✝ : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
[PROOFSTEP]
rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_eq_abs, abs_ofReal, ← Real.norm_eq_abs, norm_algebraMap']
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
⊢ dist z w = Real.sqrt ((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)
[PROOFSTEP]
rw [sq, sq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
⊢ dist z w = Real.sqrt ((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im))
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
h : z.re = w.re
⊢ dist z w = dist z.im w.im
[PROOFSTEP]
rw [dist_eq_re_im, h, sub_self, zero_pow two_pos, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
h : z.re = w.re
⊢ edist z w = edist z.im w.im
[PROOFSTEP]
rw [edist_nndist, edist_nndist, nndist_of_re_eq h]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
h : z.im = w.im
⊢ dist z w = dist z.re w.re
[PROOFSTEP]
rw [dist_eq_re_im, h, sub_self, zero_pow two_pos, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
h : z.im = w.im
⊢ edist z w = edist z.re w.re
[PROOFSTEP]
rw [edist_nndist, edist_nndist, nndist_of_im_eq h]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ dist (↑(starRingEnd ℂ) z) z = 2 * |z.im|
[PROOFSTEP]
rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul, _root_.abs_mul,
  abs_of_pos (zero_lt_two' ℝ)]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ ↑(nndist (↑(starRingEnd ℂ) z) z) = ↑(2 * ↑Real.nnabs z.im)
[PROOFSTEP]
rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ dist z (↑(starRingEnd ℂ) z) = 2 * |z.im|
[PROOFSTEP]
rw [dist_comm, dist_conj_self]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ nndist z (↑(starRingEnd ℂ) z) = 2 * ↑Real.nnabs z.im
[PROOFSTEP]
rw [nndist_comm, nndist_conj_self]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
r : ℚ
⊢ ‖↑r‖ = |↑r|
[PROOFSTEP]
rw [← ofReal_rat_cast]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
r : ℚ
⊢ ‖↑↑r‖ = |↑r|
[PROOFSTEP]
exact norm_real _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
n : ℤ
hn : 0 ≤ n
⊢ ‖↑n‖ = ↑n
[PROOFSTEP]
rw [norm_int, ← Int.cast_abs, _root_.abs_of_nonneg hn]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
⊢ Continuous ↑normSq
[PROOFSTEP]
simpa [← normSq_eq_abs] using continuous_abs.pow 2
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
n : ℕ
⊢ ↑‖↑n‖₊ = ↑↑n
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ = 1
[PROOFSTEP]
refine' (@pow_left_inj NNReal _ _ _ _ zero_le' zero_le' hn.bot_lt).mp _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ ^ n = 1 ^ n
[PROOFSTEP]
rw [← nnnorm_pow, h, nnnorm_one, one_pow]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ ‖↑equivRealProd z‖ ≤ ↑abs z
[PROOFSTEP]
simp [Prod.norm_def, abs_re_le_abs, abs_im_le_abs]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ ‖↑equivRealProd z‖ ≤ 1 * ↑abs z
[PROOFSTEP]
simpa using equivRealProd_apply_le z
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
⊢ LipschitzWith 1 ↑equivRealProd
[PROOFSTEP]
simpa using AddMonoidHomClass.lipschitz_of_bound equivRealProdLm 1 equivRealProd_apply_le'
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ ‖z‖ ≤ ↑(↑NNReal.sqrt 2) * ‖↑equivRealProdLm z‖
[PROOFSTEP]
simpa only [Real.coe_sqrt, NNReal.coe_ofNat] using abs_le_sqrt_two_mul_max z
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
⊢ Tendsto (↑normSq) (cocompact ℂ) atTop
[PROOFSTEP]
simpa [mul_self_abs] using tendsto_abs_cocompact_atTop.atTop_mul_atTop tendsto_abs_cocompact_atTop
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ ‖↑reLm x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
simp [abs_re_le_abs]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ ‖↑imLm x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
simp [abs_im_le_abs]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
⊢ restrictScalars ℝ (smulRight 1 x) = smulRight reClm x + I • smulRight imClm x
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case h.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
a b : ℝ
⊢ ↑(restrictScalars ℝ (smulRight 1 x)) { re := a, im := b } =
    ↑(smulRight reClm x + I • smulRight imClm x) { re := a, im := b }
[PROOFSTEP]
simp [mk_eq_add_mul_I, mul_smul, smul_comm I b x]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ restrictScalars ℝ (smulRight 1 x) = x • 1
[PROOFSTEP]
ext1 z
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x z : ℂ
⊢ ↑(restrictScalars ℝ (smulRight 1 x)) z = ↑(x • 1) z
[PROOFSTEP]
dsimp
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x z : ℂ
⊢ z * x = x * z
[PROOFSTEP]
apply mul_comm
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
⊢ dist (↑(starRingEnd ℂ) z) w = dist z (↑(starRingEnd ℂ) w)
[PROOFSTEP]
rw [← dist_conj_conj, conj_conj]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ →+* ℂ
hf : Continuous ↑f
⊢ f = RingHom.id ℂ ∨ f = starRingEnd ℂ
[PROOFSTEP]
simpa only [FunLike.ext_iff] using real_algHom_eq_id_or_conj (AlgHom.mk' f (map_real_smul f hf))
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ →+* ℂ
h : Continuous ↑f
⊢ f = ofReal
[PROOFSTEP]
convert congr_arg AlgHom.toRingHom <| Subsingleton.elim (AlgHom.mk' f <| map_real_smul f h) (Algebra.ofId ℝ ℂ)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
hz : 0 ≤ z
⊢ z = ↑‖z‖
[PROOFSTEP]
lift z to ℝ using hz.2.symm
[GOAL]
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℝ
hz : 0 ≤ ↑z
⊢ ↑z = ↑‖↑z‖
[PROOFSTEP]
rw [norm_eq_abs, abs_ofReal, _root_.abs_of_nonneg (id hz.1 : 0 ≤ z)]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
x : ℝ
h : HasSum (fun x => ↑(f x)) ↑x
⊢ HasSum f x
[PROOFSTEP]
simpa only [IsROrC.reClm_apply, IsROrC.ofReal_re] using reClm.hasSum h
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
h : Summable fun x => ↑(f x)
⊢ Summable f
[PROOFSTEP]
simpa only [IsROrC.reClm_apply, IsROrC.ofReal_re] using reClm.summable h
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
[PROOFSTEP]
by_cases h : Summable f
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
h : Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
[PROOFSTEP]
exact ContinuousLinearMap.map_tsum ofRealClm h
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
h : ¬Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable h, tsum_eq_zero_of_not_summable ((summable_ofReal _).not.mpr h), ofReal_zero]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum f c ↔ HasSum (fun x => ↑re (f x)) (↑re c) ∧ HasSum (fun x => ↑im (f x)) (↑im c)
[PROOFSTEP]
refine' ⟨fun h => ⟨hasSum_re _ h, hasSum_im _ h⟩, _⟩
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum (fun x => ↑re (f x)) (↑re c) ∧ HasSum (fun x => ↑im (f x)) (↑im c) → HasSum f c
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case intro
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
h₁ : HasSum (fun x => ↑re (f x)) (↑re c)
h₂ : HasSum (fun x => ↑im (f x)) (↑im c)
⊢ HasSum f c
[PROOFSTEP]
simpa only [re_add_im] using ((hasSum_ofReal 𝕜).mpr h₁).add (((hasSum_ofReal 𝕜).mpr h₂).mul_right I)
