𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
⊢ Summable fun n => ‖expSeries 𝕂 𝔸 n‖ * ↑r ^ n
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
⊢ FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = ⊤
refine' (expSeries 𝕂 𝔸).radius_eq_top_of_summable_norm fun r => _
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖‖expSeries 𝕂 𝔸 i‖ * ↑r ^ i‖ ≤ ↑r ^ i / ↑i !
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
⊢ Summable fun n => ‖expSeries 𝕂 𝔸 n‖ * ↑r ^ n
refine' summable_of_norm_bounded_eventually _ (Real.summable_pow_div_factorial r) _
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
n : ℕ
hn : n ≠ 0
⊢ ‖‖expSeries 𝕂 𝔸 n‖ * ↑r ^ n‖ ≤ ↑r ^ n / ↑n !
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖‖expSeries 𝕂 𝔸 i‖ * ↑r ^ i‖ ≤ ↑r ^ i / ↑i !
filter_upwards [eventually_cofinite_ne 0] with n hn
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
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 !
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
inst✝⁴ : IsROrC 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedRing 𝔹
inst✝ : NormedAlgebra 𝕂 𝔹
r : NNReal
n : ℕ
hn : n ≠ 0
⊢ ‖‖expSeries 𝕂 𝔸 n‖ * ↑r ^ n‖ ≤ ↑r ^ n / ↑n !
rw [norm_mul, norm_norm (expSeries 𝕂 𝔸 n), expSeries]
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
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 !
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
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 !
rw [norm_smul (n ! : 𝕂)⁻¹ (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸)]
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
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 !
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
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 !
rw [norm_inv, norm_pow, NNReal.norm_eq, norm_natCast, mul_comm, ← mul_assoc, ← div_eq_mul_inv]
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
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 !
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
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 !
have : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ ≤ 1 :=
  norm_mkPiAlgebraFin_le_of_pos (Ei := fun _ => 𝔸) (Nat.pos_of_ne_zero hn)
no goals
case h
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type ?u.329102
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 !
exact mul_le_of_le_one_right (div_nonneg (pow_nonneg r.coe_nonneg n) n !.cast_nonneg) this