[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]
