[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ‖↑(mul 𝕜 E) a‖₊ = ‖a‖₊
[PROOFSTEP]
rw [← sSup_closed_unit_ball_eq_nnnorm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ sSup ((fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1) = ‖a‖₊
[PROOFSTEP]
refine' csSup_eq_of_forall_le_of_forall_lt_exists_gt _ _ fun r hr => _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ Set.Nonempty ((fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
exact (Metric.nonempty_closedBall.mpr zero_le_one).image _
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ∀ (a_1 : NNReal), a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 → a_1 ≤ ‖a‖₊
[PROOFSTEP]
rintro - ⟨x, hx, rfl⟩
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a x : E
hx : x ∈ Metric.closedBall 0 1
⊢ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) x ≤ ‖a‖₊
[PROOFSTEP]
exact ((mul 𝕜 E a).unit_le_op_norm x <| mem_closedBall_zero_iff.mp hx).trans (op_norm_mul_apply_le 𝕜 E a)
[GOAL]
case refine'_3
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
[PROOFSTEP]
have ha : 0 < ‖a‖₊ := zero_le'.trans_lt hr
[GOAL]
case refine'_3
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
ha : 0 < ‖a‖₊
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
[PROOFSTEP]
rw [← inv_inv ‖a‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero ha.ne')] at hr
[GOAL]
case refine'_3
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
[PROOFSTEP]
obtain ⟨k, hk₁, hk₂⟩ := NormedField.exists_lt_nnnorm_lt 𝕜 (mul_lt_mul_of_pos_right hr <| inv_pos.2 ha)
[GOAL]
case refine'_3.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
[PROOFSTEP]
refine' ⟨_, ⟨k • star a, _, rfl⟩, _⟩
[GOAL]
case refine'_3.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ k • a⋆ ∈ Metric.closedBall 0 1
[PROOFSTEP]
simpa only [mem_closedBall_zero_iff, norm_smul, one_mul, norm_star] using
  (NNReal.le_inv_iff_mul_le ha.ne').1 (one_mul ‖a‖₊⁻¹ ▸ hk₂.le : ‖k‖₊ ≤ ‖a‖₊⁻¹)
[GOAL]
case refine'_3.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) (k • a⋆)
[PROOFSTEP]
simp only [map_smul, nnnorm_smul, mul_apply', mul_smul_comm, CstarRing.nnnorm_self_mul_star]
[GOAL]
case refine'_3.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < ‖k‖₊ * (‖a‖₊ * ‖a‖₊)
[PROOFSTEP]
rwa [← NNReal.div_lt_iff (mul_pos ha ha).ne', div_eq_mul_inv, mul_inv, ← mul_assoc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ‖↑(ContinuousLinearMap.flip (mul 𝕜 E)) a‖₊ = ‖a‖₊
[PROOFSTEP]
rw [← sSup_unit_ball_eq_nnnorm, ← nnnorm_star, ← @op_nnnorm_mul 𝕜 E, ← sSup_unit_ball_eq_nnnorm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ sSup ((fun x => ‖↑(↑(ContinuousLinearMap.flip (mul 𝕜 E)) a) x‖₊) '' Metric.ball 0 1) =
    sSup ((fun x => ‖↑(↑(mul 𝕜 E) a⋆) x‖₊) '' Metric.ball 0 1)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ (fun x => ‖↑(↑(ContinuousLinearMap.flip (mul 𝕜 E)) a) x‖₊) '' Metric.ball 0 1 =
    (fun x => ‖↑(↑(mul 𝕜 E) a⋆) x‖₊) '' Metric.ball 0 1
[PROOFSTEP]
simp only [mul_apply', flip_apply]
[GOAL]
case e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1 = (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1
[PROOFSTEP]
refine' Set.Subset.antisymm _ _
[GOAL]
case e_a.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1 ⊆ (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1
[PROOFSTEP]
rintro - ⟨b, hb, rfl⟩
[GOAL]
case e_a.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1 ⊆ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1
[PROOFSTEP]
rintro - ⟨b, hb, rfl⟩
[GOAL]
case e_a.refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a_1 * a‖₊) b ∈ (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1
[PROOFSTEP]
refine' ⟨star b, by simpa only [norm_star, mem_ball_zero_iff] using hb, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ b⋆ ∈ Metric.ball 0 1
[PROOFSTEP]
simpa only [norm_star, mem_ball_zero_iff] using hb
[GOAL]
case e_a.refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a⋆ * a_1‖₊) b ∈ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1
[PROOFSTEP]
refine' ⟨star b, by simpa only [norm_star, mem_ball_zero_iff] using hb, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ b⋆ ∈ Metric.ball 0 1
[PROOFSTEP]
simpa only [norm_star, mem_ball_zero_iff] using hb
[GOAL]
case e_a.refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a⋆ * a_1‖₊) b⋆ = (fun a_1 => ‖a_1 * a‖₊) b
[PROOFSTEP]
simp only [← star_mul, nnnorm_star]
[GOAL]
case e_a.refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a_1 * a‖₊) b⋆ = (fun a_1 => ‖a⋆ * a_1‖₊) b
[PROOFSTEP]
simpa using (nnnorm_star (star b * a)).symm


[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑(expSeries 𝕂 𝔸 n) fun x_1 => x) = (↑n !)⁻¹ • x ^ n
[PROOFSTEP]
simp [expSeries]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
n : ℕ
⊢ (↑(expSeries 𝕂 𝔸 n) fun x => 0) = Pi.single 0 1 n
[PROOFSTEP]
rw [expSeries_apply_eq]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • 0 ^ n = Pi.single 0 1 n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
⊢ (↑Nat.zero !)⁻¹ • 0 ^ Nat.zero = Pi.single 0 1 Nat.zero
[PROOFSTEP]
rw [pow_zero, Nat.factorial_zero, Nat.cast_one, inv_one, one_smul, Pi.single_eq_same]
[GOAL]
case succ
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
n : ℕ
⊢ (↑(Nat.succ n)!)⁻¹ • 0 ^ Nat.succ n = Pi.single 0 1 (Nat.succ n)
[PROOFSTEP]
rw [zero_pow (Nat.succ_pos _), smul_zero, Pi.single_eq_of_ne n.succ_ne_zero]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
⊢ exp 𝕂 0 = 1
[PROOFSTEP]
simp_rw [exp_eq_tsum, ← expSeries_apply_eq, expSeries_apply_zero, tsum_pi_single]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : TopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
⊢ exp 𝕂 (MulOpposite.op x) = MulOpposite.op (exp 𝕂 x)
[PROOFSTEP]
simp_rw [exp, expSeries_sum_eq, ← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : TopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸ᵐᵒᵖ
⊢ exp 𝕂 (MulOpposite.unop x) = MulOpposite.unop (exp 𝕂 x)
[PROOFSTEP]
simp_rw [exp, expSeries_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁷ : Field 𝕂
inst✝⁶ : Ring 𝔸
inst✝⁵ : Algebra 𝕂 𝔸
inst✝⁴ : TopologicalSpace 𝔸
inst✝³ : TopologicalRing 𝔸
inst✝² : T2Space 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
⊢ star (exp 𝕂 x) = exp 𝕂 (star x)
[PROOFSTEP]
simp_rw [exp_eq_tsum, ← star_pow, ← star_inv_nat_cast_smul, ← tsum_star]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : TopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute x (exp 𝕂 y)
[PROOFSTEP]
rw [exp_eq_tsum]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : TopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute x ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) y)
[PROOFSTEP]
exact Commute.tsum_right x fun n => (h.pow_right n).smul_right _
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑(expSeries 𝕂 𝔸 n) fun x_1 => x) = x ^ n / ↑n !
[PROOFSTEP]
rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul, expSeries_apply_eq,
  inv_nat_cast_smul_eq 𝕂 𝔸]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : NormedAlgebra 𝕂 𝔹
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable fun n => ‖(↑n !)⁻¹ • x ^ n‖
[PROOFSTEP]
change Summable (norm ∘ _)
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : NormedAlgebra 𝕂 𝔹
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable (norm ∘ fun n => (↑n !)⁻¹ • x ^ n)
[PROOFSTEP]
rw [← expSeries_apply_eq']
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : NormedAlgebra 𝕂 𝔹
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable (norm ∘ fun n => ↑(expSeries 𝕂 𝔸 n) fun x_1 => x)
[PROOFSTEP]
exact norm_expSeries_summable_of_mem_ball x hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasSum (fun n => (↑n !)⁻¹ • x ^ n) (exp 𝕂 x)
[PROOFSTEP]
rw [← expSeries_apply_eq']
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasSum (fun n => ↑(expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)
[PROOFSTEP]
exact expSeries_hasSum_exp_of_mem_ball x hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ AnalyticAt 𝕂 (exp 𝕂) x
[PROOFSTEP]
by_cases h : (expSeries 𝕂 𝔸).radius = 0
[GOAL]
case pos
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x
[PROOFSTEP]
rw [h] at hx
[GOAL]
case pos
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 0
h : FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x
[PROOFSTEP]
exact (ENNReal.not_lt_zero hx).elim
[GOAL]
case neg
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : ¬FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x
[PROOFSTEP]
have h := pos_iff_ne_zero.mpr h
[GOAL]
case neg
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h✝ : ¬FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ AnalyticAt 𝕂 (exp 𝕂) x
[PROOFSTEP]
exact (hasFPowerSeriesOnBall_exp_of_radius_pos h).analyticAt_of_mem hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y
[PROOFSTEP]
rw [exp_eq_tsum,
  tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm (norm_expSeries_summable_of_mem_ball' x hx)
    (norm_expSeries_summable_of_mem_ball' y hy)]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x + y) =
    ∑' (n : ℕ), ∑ kl in Finset.Nat.antidiagonal n, (↑kl.fst !)⁻¹ • x ^ kl.fst * (↑kl.snd !)⁻¹ • y ^ kl.snd
[PROOFSTEP]
dsimp only
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ∑' (n : ℕ), (↑n !)⁻¹ • (x + y) ^ n =
    ∑' (n : ℕ), ∑ kl in Finset.Nat.antidiagonal n, (↑kl.fst !)⁻¹ • x ^ kl.fst * (↑kl.snd !)⁻¹ • y ^ kl.snd
[PROOFSTEP]
conv_lhs =>
  congr
  ext
  rw [hxy.add_pow' _, Finset.smul_sum]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
| ∑' (n : ℕ), (↑n !)⁻¹ • (x + y) ^ n
[PROOFSTEP]
  congr
  ext
  rw [hxy.add_pow' _, Finset.smul_sum]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
| ∑' (n : ℕ), (↑n !)⁻¹ • (x + y) ^ n
[PROOFSTEP]
  congr
  ext
  rw [hxy.add_pow' _, Finset.smul_sum]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
| ∑' (n : ℕ), (↑n !)⁻¹ • (x + y) ^ n
[PROOFSTEP]
congr
[GOAL]
case f
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
| fun n => (↑n !)⁻¹ • (x + y) ^ n
[PROOFSTEP]
ext
[GOAL]
case f.h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
x✝ : ℕ
| (↑x✝!)⁻¹ • (x + y) ^ x✝
[PROOFSTEP]
rw [hxy.add_pow' _, Finset.smul_sum]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ∑' (x_1 : ℕ),
      ∑ x_2 in Finset.Nat.antidiagonal x_1, (↑x_1 !)⁻¹ • Nat.choose x_1 x_2.fst • (x ^ x_2.fst * y ^ x_2.snd) =
    ∑' (n : ℕ), ∑ kl in Finset.Nat.antidiagonal n, (↑kl.fst !)⁻¹ • x ^ kl.fst * (↑kl.snd !)⁻¹ • y ^ kl.snd
[PROOFSTEP]
refine' tsum_congr fun n => Finset.sum_congr rfl fun kl hkl => _
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.Nat.antidiagonal n
⊢ (↑n !)⁻¹ • Nat.choose n kl.fst • (x ^ kl.fst * y ^ kl.snd) = (↑kl.fst !)⁻¹ • x ^ kl.fst * (↑kl.snd !)⁻¹ • y ^ kl.snd
[PROOFSTEP]
rw [nsmul_eq_smul_cast 𝕂, smul_smul, smul_mul_smul, ← Finset.Nat.mem_antidiagonal.mp hkl, Nat.cast_add_choose,
  Finset.Nat.mem_antidiagonal.mp hkl]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.Nat.antidiagonal n
⊢ ((↑n !)⁻¹ * (↑n ! / (↑kl.fst ! * ↑kl.snd !))) • (x ^ kl.fst * y ^ kl.snd) =
    ((↑kl.fst !)⁻¹ * (↑kl.snd !)⁻¹) • (x ^ kl.fst * y ^ kl.snd)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.Nat.antidiagonal n
⊢ (↑n !)⁻¹ * (↑n ! / (↑kl.fst ! * ↑kl.snd !)) = (↑kl.fst !)⁻¹ * (↑kl.snd !)⁻¹
[PROOFSTEP]
have : (n ! : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr n.factorial_ne_zero
[GOAL]
case e_a
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.Nat.antidiagonal n
this : ↑n ! ≠ 0
⊢ (↑n !)⁻¹ * (↑n ! / (↑kl.fst ! * ↑kl.snd !)) = (↑kl.fst !)⁻¹ * (↑kl.snd !)⁻¹
[PROOFSTEP]
field_simp [this]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 (-x) * exp 𝕂 x = 1
[PROOFSTEP]
have hnx : -x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
  by
  rw [EMetric.mem_ball, ← neg_zero, edist_neg_neg]
  exact hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ -x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
[PROOFSTEP]
rw [EMetric.mem_ball, ← neg_zero, edist_neg_neg]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ edist x 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
[PROOFSTEP]
exact hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hnx : -x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 (-x) * exp 𝕂 x = 1
[PROOFSTEP]
rw [← exp_add_of_commute_of_mem_ball (Commute.neg_left <| Commute.refl x) hnx hx, neg_add_self, exp_zero]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 x * exp 𝕂 (-x) = 1
[PROOFSTEP]
have hnx : -x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
  by
  rw [EMetric.mem_ball, ← neg_zero, edist_neg_neg]
  exact hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ -x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
[PROOFSTEP]
rw [EMetric.mem_ball, ← neg_zero, edist_neg_neg]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ edist x 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
[PROOFSTEP]
exact hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hnx : -x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 x * exp 𝕂 (-x) = 1
[PROOFSTEP]
rw [← exp_add_of_commute_of_mem_ball (Commute.neg_right <| Commute.refl x) hx hnx, add_neg_self, exp_zero]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕂
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedRing 𝔹
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔹
inst✝² : CompleteSpace 𝔸
inst✝¹ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
inst✝ : Invertible (exp 𝕂 x)
⊢ ⅟(exp 𝕂 x) = exp 𝕂 (-x)
[PROOFSTEP]
letI := invertibleExpOfMemBall hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕂
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedRing 𝔹
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔹
inst✝² : CompleteSpace 𝔸
inst✝¹ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
inst✝ : Invertible (exp 𝕂 x)
this : Invertible (exp 𝕂 x) := invertibleExpOfMemBall hx
⊢ ⅟(exp 𝕂 x) = exp 𝕂 (-x)
[PROOFSTEP]
convert (rfl : ⅟(exp 𝕂 x) = _)
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_4
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ↑f (exp 𝕂 x) = exp 𝕂 (↑f x)
[PROOFSTEP]
rw [exp_eq_tsum, exp_eq_tsum]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_4
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ↑f ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x) = (fun x_1 => ∑' (n : ℕ), (↑n !)⁻¹ • x_1 ^ n) (↑f x)
[PROOFSTEP]
refine' ((expSeries_summable_of_mem_ball' _ hx).hasSum.map f hf).tsum_eq.symm.trans _
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_4
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ∑' (b : ℕ), (↑f ∘ fun n => (↑n !)⁻¹ • x ^ n) b = (fun x_1 => ∑' (n : ℕ), (↑n !)⁻¹ • x_1 ^ n) (↑f x)
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_4
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ∑' (b : ℕ), ↑f ((↑b !)⁻¹ • x ^ b) = ∑' (n : ℕ), (↑n !)⁻¹ • ↑f x ^ n
[PROOFSTEP]
simp_rw [map_inv_nat_cast_smul f 𝕂 𝕂, map_pow]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable fun n => ‖x ^ n / ↑n !‖
[PROOFSTEP]
change Summable (norm ∘ _)
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable (norm ∘ fun n => x ^ n / ↑n !)
[PROOFSTEP]
rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable (norm ∘ fun n => ↑(expSeries 𝕂 𝔸 n) fun x_1 => x)
[PROOFSTEP]
exact norm_expSeries_summable_of_mem_ball x hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasSum (fun n => x ^ n / ↑n !) (exp 𝕂 x)
[PROOFSTEP]
rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasSum (fun n => ↑(expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)
[PROOFSTEP]
exact expSeries_hasSum_exp_of_mem_ball x hx
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
⊢ FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = ⊤
[PROOFSTEP]
refine' (expSeries 𝕂 𝔸).radius_eq_top_of_summable_norm fun r => _
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
⊢ Summable fun n => ‖expSeries 𝕂 𝔸 n‖ * ↑r ^ n
[PROOFSTEP]
refine' summable_of_norm_bounded_eventually _ (Real.summable_pow_div_factorial r) _
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖‖expSeries 𝕂 𝔸 i‖ * ↑r ^ i‖ ≤ ↑r ^ i / ↑i !
[PROOFSTEP]
filter_upwards [eventually_cofinite_ne 0] with n hn
[GOAL]
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
n : ℕ
hn : n ≠ 0
⊢ ‖‖expSeries 𝕂 𝔸 n‖ * ↑r ^ n‖ ≤ ↑r ^ n / ↑n !
[PROOFSTEP]
rw [norm_mul, norm_norm (expSeries 𝕂 𝔸 n), expSeries]
[GOAL]
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
n : ℕ
hn : n ≠ 0
⊢ ‖(↑n !)⁻¹ • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ * ‖↑r ^ n‖ ≤ ↑r ^ n / ↑n !
[PROOFSTEP]
rw [norm_smul (n ! : 𝕂)⁻¹ (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸)]
  -- porting note: Lean needed this to be explicit for some reason
[GOAL]
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
n : ℕ
hn : n ≠ 0
⊢ ‖(↑n !)⁻¹‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ * ‖↑r ^ n‖ ≤ ↑r ^ n / ↑n !
[PROOFSTEP]
rw [norm_inv, norm_pow, NNReal.norm_eq, norm_natCast, mul_comm, ← mul_assoc, ← div_eq_mul_inv]
[GOAL]
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
n : ℕ
hn : n ≠ 0
⊢ ↑r ^ n / ↑n ! * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ ≤ ↑r ^ n / ↑n !
[PROOFSTEP]
have : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ ≤ 1 :=
  norm_mkPiAlgebraFin_le_of_pos (Ei := fun _ => 𝔸) (Nat.pos_of_ne_zero hn)
[GOAL]
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
n : ℕ
hn : n ≠ 0
this : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ ≤ 1
⊢ ↑r ^ n / ↑n ! * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ ≤ ↑r ^ n / ↑n !
[PROOFSTEP]
exact mul_le_of_le_one_right (div_nonneg (pow_nonneg r.coe_nonneg n) n !.cast_nonneg) this
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
⊢ 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
[PROOFSTEP]
rw [expSeries_radius_eq_top]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
⊢ 0 < ⊤
[PROOFSTEP]
exact WithTop.zero_lt_top
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
⊢ Continuous (exp 𝕂)
[PROOFSTEP]
rw [continuous_iff_continuousOn_univ, ← Metric.eball_top_eq_univ (0 : 𝔸), ← expSeries_radius_eq_top 𝕂 𝔸]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
⊢ ContinuousOn (exp 𝕂) (EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)))
[PROOFSTEP]
exact continuousOn_exp
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁷ : IsROrC 𝕂
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedAlgebra 𝕂 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔹
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ exp 𝕂 x ∈ unitary 𝔸
[PROOFSTEP]
rw [unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ← exp_add_of_commute (Commute.refl x).neg_left, ←
  exp_add_of_commute (Commute.refl x).neg_right, add_left_neg, add_right_neg, exp_zero, and_self_iff]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
ι : Type u_4
s : Finset ι
f : ι → 𝔸
h : Set.Pairwise ↑s fun i j => Commute (f i) (f j)
⊢ exp 𝕂 (∑ i in s, f i) =
    Finset.noncommProd s (fun i => exp 𝕂 (f i))
      (_ : ∀ (i : ι), i ∈ ↑s → ∀ (j : ι), j ∈ ↑s → i ≠ j → Commute (exp 𝕂 (f i)) (exp 𝕂 (f j)))
[PROOFSTEP]
classical
induction' s using Finset.induction_on with a s ha ih
· simp
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
  ih (h.mono <| Finset.subset_insert _ _)]
refine' Commute.sum_right _ _ _ fun i hi => _
exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
ι : Type u_4
s : Finset ι
f : ι → 𝔸
h : Set.Pairwise ↑s fun i j => Commute (f i) (f j)
⊢ exp 𝕂 (∑ i in s, f i) =
    Finset.noncommProd s (fun i => exp 𝕂 (f i))
      (_ : ∀ (i : ι), i ∈ ↑s → ∀ (j : ι), j ∈ ↑s → i ≠ j → Commute (exp 𝕂 (f i)) (exp 𝕂 (f j)))
[PROOFSTEP]
induction' s using Finset.induction_on with a s ha ih
[GOAL]
case empty
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
ι : Type u_4
s : Finset ι
f : ι → 𝔸
h✝ : Set.Pairwise ↑s fun i j => Commute (f i) (f j)
h : Set.Pairwise ↑∅ fun i j => Commute (f i) (f j)
⊢ exp 𝕂 (∑ i in ∅, f i) =
    Finset.noncommProd ∅ (fun i => exp 𝕂 (f i))
      (_ : ∀ (i : ι), i ∈ ↑∅ → ∀ (j : ι), j ∈ ↑∅ → i ≠ j → Commute (exp 𝕂 (f i)) (exp 𝕂 (f j)))
[PROOFSTEP]
simp
[GOAL]
case insert
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
ι : Type u_4
s✝ : Finset ι
f : ι → 𝔸
h✝ : Set.Pairwise ↑s✝ fun i j => Commute (f i) (f j)
a : ι
s : Finset ι
ha : ¬a ∈ s
ih :
  ∀ (h : Set.Pairwise ↑s fun i j => Commute (f i) (f j)),
    exp 𝕂 (∑ i in s, f i) =
      Finset.noncommProd s (fun i => exp 𝕂 (f i))
        (_ : ∀ (i : ι), i ∈ ↑s → ∀ (j : ι), j ∈ ↑s → i ≠ j → Commute (exp 𝕂 (f i)) (exp 𝕂 (f j)))
h : Set.Pairwise ↑(insert a s) fun i j => Commute (f i) (f j)
⊢ exp 𝕂 (∑ i in insert a s, f i) =
    Finset.noncommProd (insert a s) (fun i => exp 𝕂 (f i))
      (_ : ∀ (i : ι), i ∈ ↑(insert a s) → ∀ (j : ι), j ∈ ↑(insert a s) → i ≠ j → Commute (exp 𝕂 (f i)) (exp 𝕂 (f j)))
[PROOFSTEP]
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
  ih (h.mono <| Finset.subset_insert _ _)]
[GOAL]
case insert
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
ι : Type u_4
s✝ : Finset ι
f : ι → 𝔸
h✝ : Set.Pairwise ↑s✝ fun i j => Commute (f i) (f j)
a : ι
s : Finset ι
ha : ¬a ∈ s
ih :
  ∀ (h : Set.Pairwise ↑s fun i j => Commute (f i) (f j)),
    exp 𝕂 (∑ i in s, f i) =
      Finset.noncommProd s (fun i => exp 𝕂 (f i))
        (_ : ∀ (i : ι), i ∈ ↑s → ∀ (j : ι), j ∈ ↑s → i ≠ j → Commute (exp 𝕂 (f i)) (exp 𝕂 (f j)))
h : Set.Pairwise ↑(insert a s) fun i j => Commute (f i) (f j)
⊢ Commute (f a) (∑ x in s, f x)
[PROOFSTEP]
refine' Commute.sum_right _ _ _ fun i hi => _
[GOAL]
case insert
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
ι : Type u_4
s✝ : Finset ι
f : ι → 𝔸
h✝ : Set.Pairwise ↑s✝ fun i j => Commute (f i) (f j)
a : ι
s : Finset ι
ha : ¬a ∈ s
ih :
  ∀ (h : Set.Pairwise ↑s fun i j => Commute (f i) (f j)),
    exp 𝕂 (∑ i in s, f i) =
      Finset.noncommProd s (fun i => exp 𝕂 (f i))
        (_ : ∀ (i : ι), i ∈ ↑s → ∀ (j : ι), j ∈ ↑s → i ≠ j → Commute (exp 𝕂 (f i)) (exp 𝕂 (f j)))
h : Set.Pairwise ↑(insert a s) fun i j => Commute (f i) (f j)
i : ι
hi : i ∈ s
⊢ Commute (f a) (f i)
[PROOFSTEP]
exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
n : ℕ
x : 𝔸
⊢ exp 𝕂 (n • x) = exp 𝕂 x ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
⊢ exp 𝕂 (Nat.zero • x) = exp 𝕂 x ^ Nat.zero
[PROOFSTEP]
rw [Nat.zero_eq, zero_smul, pow_zero, exp_zero]
[GOAL]
case succ
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : IsROrC 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp 𝕂 (n • x) = exp 𝕂 x ^ n
⊢ exp 𝕂 (Nat.succ n • x) = exp 𝕂 x ^ Nat.succ n
[PROOFSTEP]
rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_right n), ih]
[GOAL]
𝕂 : Type u_1
𝔸✝ : Type u_2
𝔹 : Type u_3
inst✝¹⁰ : IsROrC 𝕂
inst✝⁹ : NormedRing 𝔸✝
inst✝⁸ : NormedAlgebra 𝕂 𝔸✝
inst✝⁷ : NormedRing 𝔹
inst✝⁶ : NormedAlgebra 𝕂 𝔹
inst✝⁵ : CompleteSpace 𝔸✝
ι : Type u_4
𝔸 : ι → Type u_5
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
⊢ update (exp 𝕂 x) j (exp 𝕂 xj) = exp 𝕂 (update x j xj)
[PROOFSTEP]
ext i
[GOAL]
case h
𝕂 : Type u_1
𝔸✝ : Type u_2
𝔹 : Type u_3
inst✝¹⁰ : IsROrC 𝕂
inst✝⁹ : NormedRing 𝔸✝
inst✝⁸ : NormedAlgebra 𝕂 𝔸✝
inst✝⁷ : NormedRing 𝔹
inst✝⁶ : NormedAlgebra 𝕂 𝔹
inst✝⁵ : CompleteSpace 𝔸✝
ι : Type u_4
𝔸 : ι → Type u_5
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ update (exp 𝕂 x) j (exp 𝕂 xj) i = exp 𝕂 (update x j xj) i
[PROOFSTEP]
simp_rw [Pi.exp_def]
[GOAL]
case h
𝕂 : Type u_1
𝔸✝ : Type u_2
𝔹 : Type u_3
inst✝¹⁰ : IsROrC 𝕂
inst✝⁹ : NormedRing 𝔸✝
inst✝⁸ : NormedAlgebra 𝕂 𝔸✝
inst✝⁷ : NormedRing 𝔹
inst✝⁶ : NormedAlgebra 𝕂 𝔹
inst✝⁵ : CompleteSpace 𝔸✝
ι : Type u_4
𝔸 : ι → Type u_5
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ update (fun i => exp 𝕂 (x i)) j (exp 𝕂 xj) i = exp 𝕂 (update x j xj i)
[PROOFSTEP]
exact (Function.apply_update (fun i => exp 𝕂) x j xj i).symm
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
z : ℤ
x : 𝔸
⊢ exp 𝕂 (z • x) = exp 𝕂 x ^ z
[PROOFSTEP]
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
[GOAL]
case intro.inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (↑n • x) = exp 𝕂 x ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, coe_nat_zsmul, exp_nsmul]
[GOAL]
case intro.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (-↑n • x) = exp 𝕂 x ^ (-↑n)
[PROOFSTEP]
rw [zpow_neg, zpow_ofNat, neg_smul, exp_neg, coe_nat_zsmul, exp_nsmul]
[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
⊢ exp 𝕂 (∑ i in s, f i) = ∏ i in s, exp 𝕂 (f i)
[PROOFSTEP]
rw [exp_sum_of_commute, Finset.noncommProd_eq_prod]
[GOAL]
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
⊢ Set.Pairwise ↑s fun i j => Commute (f i) (f j)
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
⊢ Set.Pairwise ↑s fun i j => Commute (f i) (f j)
[PROOFSTEP]
exact fun i _hi j _hj _ => Commute.all _ _
[GOAL]
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
n : ℕ
x : 𝔸
⊢ (↑(expSeries 𝕂 𝔸 n) fun x_1 => x) = ↑(expSeries 𝕂' 𝔸 n) fun x_1 => x
[PROOFSTEP]
rw [expSeries_apply_eq, expSeries_apply_eq, inv_nat_cast_smul_eq 𝕂 𝕂']
[GOAL]
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
⊢ exp 𝕂 = exp 𝕂'
[PROOFSTEP]
ext x
[GOAL]
case h
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
⊢ exp 𝕂 x = exp 𝕂' x
[PROOFSTEP]
rw [exp, exp]
[GOAL]
case h
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸) x = FormalMultilinearSeries.sum (expSeries 𝕂' 𝔸) x
[PROOFSTEP]
refine' tsum_congr fun n => _
[GOAL]
case h
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑(expSeries 𝕂 𝔸 n) fun x_1 => x) = ↑(expSeries 𝕂' 𝔸 n) fun x_1 => x
[PROOFSTEP]
rw [expSeries_eq_expSeries 𝕂 𝕂' 𝔸 n x]


[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
x : ℝ
⊢ ‖x⋆ * x‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
simp only [star, id.def, norm_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
⊢ ∀ (x : E), ‖x⋆‖ = ‖x‖
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
by_cases htriv : x = 0
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : x = 0
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
simp only [htriv, star_zero]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
have hnt : 0 < ‖x‖ := norm_pos_iff.mpr htriv
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
have hnt_star : 0 < ‖x⋆‖ := norm_pos_iff.mpr ((AddEquiv.map_ne_zero_iff starAddEquiv (M := E)).mpr htriv)
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
hnt_star : 0 < ‖x⋆‖
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
have h₁ :=
  calc
    ‖x‖ * ‖x‖ = ‖x⋆ * x‖ := norm_star_mul_self.symm
    _ ≤ ‖x⋆‖ * ‖x‖ := norm_mul_le _ _
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
hnt_star : 0 < ‖x⋆‖
h₁ : ‖x‖ * ‖x‖ ≤ ‖x⋆‖ * ‖x‖
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
have h₂ :=
  calc
    ‖x⋆‖ * ‖x⋆‖ = ‖x * x⋆‖ := by rw [← norm_star_mul_self, star_star]
    _ ≤ ‖x‖ * ‖x⋆‖ := norm_mul_le _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
hnt_star : 0 < ‖x⋆‖
h₁ : ‖x‖ * ‖x‖ ≤ ‖x⋆‖ * ‖x‖
⊢ ‖x⋆‖ * ‖x⋆‖ = ‖x * x⋆‖
[PROOFSTEP]
rw [← norm_star_mul_self, star_star]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
hnt_star : 0 < ‖x⋆‖
h₁ : ‖x‖ * ‖x‖ ≤ ‖x⋆‖ * ‖x‖
h₂ : ‖x⋆‖ * ‖x⋆‖ ≤ ‖x‖ * ‖x⋆‖
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
exact le_antisymm (le_of_mul_le_mul_right h₂ hnt_star) (le_of_mul_le_mul_right h₁ hnt)
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x * x⋆‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
nth_rw 1 [← star_star x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
simp only [norm_star_mul_self, norm_star]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖
[PROOFSTEP]
rw [norm_star_mul_self, norm_star]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x⋆ * x = 0 ↔ x = 0
[PROOFSTEP]
rw [← norm_eq_zero, norm_star_mul_self]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x‖ * ‖x‖ = 0 ↔ x = 0
[PROOFSTEP]
exact mul_self_eq_zero.trans norm_eq_zero
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x⋆ * x ≠ 0 ↔ x ≠ 0
[PROOFSTEP]
simp only [Ne.def, star_mul_self_eq_zero_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x * x⋆ = 0 ↔ x = 0
[PROOFSTEP]
simpa only [star_eq_zero, star_star] using @star_mul_self_eq_zero_iff _ _ _ _ (star x)
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x * x⋆ ≠ 0 ↔ x ≠ 0
[PROOFSTEP]
simp only [Ne.def, mul_star_self_eq_zero_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x⋆ * x‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
dsimp only [norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖(x⋆ * x).fst‖ ⊔ ‖(x⋆ * x).snd‖ = (‖x.fst‖ ⊔ ‖x.snd‖) * (‖x.fst‖ ⊔ ‖x.snd‖)
[PROOFSTEP]
simp only [Prod.fst_mul, Prod.fst_star, Prod.snd_mul, Prod.snd_star, norm_star_mul_self, ← sq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.fst‖ ^ 2 ⊔ ‖x.snd‖ ^ 2 = (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.fst‖ ^ 2 ⊔ ‖x.snd‖ ^ 2 ≤ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2
[PROOFSTEP]
refine' max_le _ _
[GOAL]
case refine'_1.refine'_1
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.fst‖ ^ 2 ≤ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2
[PROOFSTEP]
rw [sq_le_sq, abs_of_nonneg (norm_nonneg _)]
[GOAL]
case refine'_1.refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.snd‖ ^ 2 ≤ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2
[PROOFSTEP]
rw [sq_le_sq, abs_of_nonneg (norm_nonneg _)]
[GOAL]
case refine'_1.refine'_1
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.fst‖ ≤ |‖x.fst‖ ⊔ ‖x.snd‖|
case refine'_1.refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.snd‖ ≤ |‖x.fst‖ ⊔ ‖x.snd‖|
[PROOFSTEP]
exact (le_max_left _ _).trans (le_abs_self _)
[GOAL]
case refine'_1.refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.snd‖ ≤ |‖x.fst‖ ⊔ ‖x.snd‖|
[PROOFSTEP]
exact (le_max_right _ _).trans (le_abs_self _)
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.fst‖ ^ 2 ⊔ ‖x.snd‖ ^ 2
[PROOFSTEP]
rw [le_sup_iff]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.fst‖ ^ 2 ∨ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.snd‖ ^ 2
[PROOFSTEP]
rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h)
[GOAL]
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
h : ‖x.fst‖ ≤ ‖x.snd‖
⊢ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.fst‖ ^ 2 ∨ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.snd‖ ^ 2
[PROOFSTEP]
simp [h]
[GOAL]
case refine'_2.inr
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
h : ‖x.snd‖ ≤ ‖x.fst‖
⊢ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.fst‖ ^ 2 ∨ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.snd‖ ^ 2
[PROOFSTEP]
simp [h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : (i : ι) → R i
⊢ ‖x⋆ * x‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
simp only [norm, Pi.mul_apply, Pi.star_apply, nnnorm_star_mul_self, ← sq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : (i : ι) → R i
⊢ ↑(Finset.sup Finset.univ fun b => ‖x b‖₊ ^ 2) = ↑(Finset.sup Finset.univ fun b => ‖x b‖₊) ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : (i : ι) → R i
⊢ (Finset.sup Finset.univ fun b => ‖x b‖₊ ^ 2) = (Finset.sup Finset.univ fun b => ‖x b‖₊) ^ 2
[PROOFSTEP]
exact
  (Finset.comp_sup_eq_sup_comp_of_is_total (fun x : NNReal => x ^ 2)
      (fun x y h => by simpa only [sq] using mul_le_mul' h h) (by simp)).symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x✝ : (i : ι) → R i
x y : NNReal
h : x ≤ y
⊢ (fun x => x ^ 2) x ≤ (fun x => x ^ 2) y
[PROOFSTEP]
simpa only [sq] using mul_le_mul' h h
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : (i : ι) → R i
⊢ (fun x => x ^ 2) ⊥ = ⊥
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
⊢ ‖1‖ = 1
[PROOFSTEP]
have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = 1
[PROOFSTEP]
rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
U : { x // x ∈ unitary E }
⊢ ‖↑U‖ = 1
[PROOFSTEP]
rw [← sq_eq_sq (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CstarRing.norm_star_mul_self, unitary.coe_star_mul_self,
  CstarRing.norm_one]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
⊢ ‖↑U * A‖ = ‖A‖
[PROOFSTEP]
nontriviality E
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U * A‖ = ‖A‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U * A‖ ≤ ‖A‖
[PROOFSTEP]
calc
  _ ≤ ‖(U : E)‖ * ‖A‖ := norm_mul_le _ _
  _ = ‖A‖ := by rw [norm_coe_unitary, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U‖ * ‖A‖ = ‖A‖
[PROOFSTEP]
rw [norm_coe_unitary, one_mul]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖A‖ ≤ ‖↑U * A‖
[PROOFSTEP]
calc
  _ = ‖(U : E)⋆ * U * A‖ := by rw [unitary.coe_star_mul_self U, one_mul]
  _ ≤ ‖(U : E)⋆‖ * ‖(U : E) * A‖ := by
    rw [mul_assoc]
    exact norm_mul_le _ _
  _ = ‖(U : E) * A‖ := by rw [norm_star, norm_coe_unitary, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖A‖ = ‖(↑U)⋆ * ↑U * A‖
[PROOFSTEP]
rw [unitary.coe_star_mul_self U, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆ * ↑U * A‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆ * (↑U * A)‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖
[PROOFSTEP]
exact norm_mul_le _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆‖ * ‖↑U * A‖ = ‖↑U * A‖
[PROOFSTEP]
rw [norm_star, norm_coe_unitary, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
A : E
U : { x // x ∈ unitary E }
⊢ ‖A * ↑U‖ = ‖((↑U)⋆ * A⋆)⋆‖
[PROOFSTEP]
simp only [star_star, star_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
A : E
U : { x // x ∈ unitary E }
⊢ ‖((↑U)⋆ * A⋆)⋆‖ = ‖(↑U)⋆ * A⋆‖
[PROOFSTEP]
rw [norm_star]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
⊢ ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n
[PROOFSTEP]
induction' n with k hk
[GOAL]
case zero
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x ^ 2 ^ Nat.zero‖₊ = ‖x‖₊ ^ 2 ^ Nat.zero
[PROOFSTEP]
simp only [pow_zero, pow_one, Nat.zero_eq]
[GOAL]
case succ
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ Nat.succ k‖₊ = ‖x‖₊ ^ 2 ^ Nat.succ k
[PROOFSTEP]
rw [pow_succ, pow_mul', sq]
[GOAL]
case succ
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
[PROOFSTEP]
nth_rw 1 [← selfAdjoint.mem_iff.mp hx]
[GOAL]
case succ
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x⋆ ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
[PROOFSTEP]
rw [← star_pow, CstarRing.nnnorm_star_mul_self, ← sq, hk, pow_mul']