Mathlib.Analysis.Analytic.OfScalars

FormalMultilinearSeries.ofScalars definition

(c : ℕ → 𝕜) : FormalMultilinearSeries 𝕜 E E

Full source

/-- Formal power series of `∑ cᵢ • xⁱ` for some scalar field `𝕜` and ring algebra `E` -/
def ofScalars (c : ℕ → 𝕜) : FormalMultilinearSeries 𝕜 E E :=
  fun n ↦ c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E

Formal power series of scalar multiples

Informal description

Given a sequence of scalars $ (c_i)_{i \in \mathbb{N}} $ in a field $ \mathbb{K} $, the formal multilinear series $ \sum_{i} c_i \cdot x^i $ is defined, where each term $ c_i \cdot x^i $ is interpreted as a continuous multilinear map from $ \mathbb{K}^i $ to $ E $ via the canonical algebra structure on $ E $.

FormalMultilinearSeries.ofScalars_eq_zero theorem

[Nontrivial E] (n : ℕ) : ofScalars E c n = 0 ↔ c n = 0

Full source

@[simp]
theorem ofScalars_eq_zero [Nontrivial E] (n : ℕ) : ofScalarsofScalars E c n = 0 ↔ c n = 0 := by
  rw [ofScalars, smul_eq_zero (c := c n) (x := ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]
  refine or_iff_left (ContinuousMultilinearMap.ext_iff.1.mt <| not_forall_of_exists_not ?_)
  use fun _ ↦ 1
  simp

Vanishing of $n$-th Term in Formal Power Series $\sum c_i x^i$ is Equivalent to $c_n = 0$

Informal description

Let $E$ be a nontrivial topological vector space over a field $\mathbb{K}$. For any natural number $n$, the $n$-th term of the formal power series $\sum_{i} c_i x^i$ is zero if and only if the coefficient $c_n$ is zero.

FormalMultilinearSeries.ofScalars_eq_zero_of_scalar_zero theorem

{n : ℕ} (hc : c n = 0) : ofScalars E c n = 0

Full source

@[simp]
theorem ofScalars_eq_zero_of_scalar_zero {n : ℕ} (hc : c n = 0) : ofScalars E c n = 0 := by
  rw [ofScalars, hc, zero_smul 𝕜 (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]

Vanishing of $n$-th Term in Formal Power Series When Coefficient $c_n$ is Zero

Informal description

For any natural number $n$, if the coefficient $c_n$ in the sequence $(c_i)_{i \in \mathbb{N}}$ is zero, then the $n$-th term of the formal multilinear series $\sum_{i} c_i \cdot x^i$ is also zero.

FormalMultilinearSeries.ofScalars_series_eq_zero theorem

[Nontrivial E] : ofScalars E c = 0 ↔ c = 0

Full source

@[simp]
theorem ofScalars_series_eq_zero [Nontrivial E] : ofScalarsofScalars E c = 0 ↔ c = 0 := by
  simp [FormalMultilinearSeries.ext_iff, funext_iff]

Vanishing of Formal Power Series $\sum c_i x^i$ is Equivalent to Vanishing of Coefficients $c_i$

Informal description

Let $E$ be a nontrivial topological vector space over a field $\mathbb{K}$. The formal multilinear series $\sum_{i} c_i \cdot x^i$ is identically zero if and only if the sequence of scalars $(c_i)_{i \in \mathbb{N}}$ is identically zero.

FormalMultilinearSeries.ofScalars_series_eq_zero_of_scalar_zero theorem

: ofScalars E (0 : ℕ → 𝕜) = 0

Full source

@[simp]
theorem ofScalars_series_eq_zero_of_scalar_zero : ofScalars E (0 : ℕ → 𝕜) = 0 := by
  simp [FormalMultilinearSeries.ext_iff]

Vanishing of Formal Power Series with Zero Coefficients

Informal description

The formal multilinear series $\sum_{i} 0 \cdot x^i$ is identically zero.

FormalMultilinearSeries.ofScalars_series_of_subsingleton theorem

[Subsingleton E] : ofScalars E c = 0

Full source

@[simp]
theorem ofScalars_series_of_subsingleton [Subsingleton E] : ofScalars E c = 0 := by
  simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff]
  exact fun _ _ ↦ Subsingleton.allEq _ _

Vanishing of Formal Power Series in Subsingleton Spaces

Informal description

If the topological vector space $E$ is a subsingleton (i.e., has at most one element), then the formal power series $\sum_{i} c_i \cdot x^i$ is identically zero for any sequence of scalars $(c_i)_{i \in \mathbb{N}}$.

FormalMultilinearSeries.ofScalars_series_injective theorem

[Nontrivial E] : Function.Injective (ofScalars E (𝕜 := 𝕜))

Full source

theorem ofScalars_series_injective [Nontrivial E] : Function.Injective (ofScalars E (𝕜 := 𝕜)) := by
  intro _ _
  refine Function.mtr fun h ↦ ?_
  simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff,
    ContinuousMultilinearMap.smul_apply]
  push_neg
  obtain ⟨n, hn⟩ := Function.ne_iff.1 h
  refine ⟨n, fun _ ↦ 1, ?_⟩
  simp only [mkPiAlgebraFin_apply, List.ofFn_const, List.prod_replicate, one_pow, ne_eq]
  exact (smul_left_injective 𝕜 one_ne_zero).ne hn

Injectivity of Scalar-to-Series Map in Nontrivial Spaces

Informal description

If the topological vector space $E$ is nontrivial (i.e., contains at least two distinct elements), then the map that associates to each sequence of scalars $(c_i)_{i \in \mathbb{N}}$ the formal power series $\sum_i c_i \cdot x^i$ is injective. In other words, if two formal power series $\sum_i c_i \cdot x^i$ and $\sum_i c_i' \cdot x^i$ are equal, then $c_i = c_i'$ for all $i \in \mathbb{N}$.

FormalMultilinearSeries.ofScalars_series_eq_iff theorem

[Nontrivial E] (c' : ℕ → 𝕜) : ofScalars E c = ofScalars E c' ↔ c = c'

Full source

@[simp]
theorem ofScalars_series_eq_iff [Nontrivial E] (c' : ℕ → 𝕜) :
    ofScalarsofScalars E c = ofScalars E c' ↔ c = c' :=
  ⟨fun e => ofScalars_series_injective 𝕜 E e, _root_.congrArg _⟩

Equality of Scalar Power Series in Nontrivial Spaces

Informal description

Let $E$ be a nontrivial topological vector space over a field $\mathbb{K}$, and let $(c_i)_{i \in \mathbb{N}}$ and $(c'_i)_{i \in \mathbb{N}}$ be two sequences of scalars in $\mathbb{K}$. Then the formal power series $\sum_i c_i \cdot x^i$ and $\sum_i c'_i \cdot x^i$ are equal if and only if $c_i = c'_i$ for all $i \in \mathbb{N}$.

FormalMultilinearSeries.ofScalars_apply_zero theorem

(n : ℕ) : (ofScalars E c n fun _ => 0) = Pi.single (f := fun _ => E) 0 (c 0 • 1) n

Full source

theorem ofScalars_apply_zero (n : ℕ) :
    (ofScalars E c n fun _ => 0) = Pi.single (f := fun _ => E) 0 (c 0 • 1) n := by
  rw [ofScalars]
  cases n <;> simp

Evaluation of Scalar Series at Zero: $\sum_i c_i \cdot 0^i = c_0 \cdot 1$

Informal description

For any natural number $n$, the $n$-th term of the formal multilinear series $\sum_i c_i \cdot x^i$ evaluated at the zero function (i.e., $x = 0$) is equal to $c_0 \cdot 1$ if $n = 0$, and zero otherwise.

FormalMultilinearSeries.coeff_ofScalars theorem

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {p : ℕ → 𝕜} {n : ℕ} : (FormalMultilinearSeries.ofScalars 𝕜 p).coeff n = p n

Full source

@[simp]
lemma coeff_ofScalars {𝕜 : Type*} [NontriviallyNormedField 𝕜] {p : ℕ → 𝕜} {n : ℕ} :
    (FormalMultilinearSeries.ofScalars 𝕜 p).coeff n = p n := by
  simp [FormalMultilinearSeries.coeff, FormalMultilinearSeries.ofScalars, List.prod_ofFn]

Coefficient Extraction from Scalar Series: $(\sum_i p_i x^i)_n = p_n$

Informal description

For any sequence of scalars $(p_i)_{i \in \mathbb{N}}$ in a nontrivially normed field $\mathbb{K}$ and any natural number $n$, the $n$-th coefficient of the formal multilinear series $\sum_i p_i \cdot x^i$ is equal to $p_n$.

FormalMultilinearSeries.ofScalars_add theorem

(c' : ℕ → 𝕜) : ofScalars E (c + c') = ofScalars E c + ofScalars E c'

Full source

theorem ofScalars_add (c' : ℕ → 𝕜) : ofScalars E (c + c') = ofScalars E c + ofScalars E c' := by
  unfold ofScalars
  simp_rw [Pi.add_apply, Pi.add_def _ _]
  exact funext fun n ↦ Module.add_smul (c n) (c' n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)

Additivity of Formal Scalar Series: $\text{ofScalars}_E (c + c') = \text{ofScalars}_E c + \text{ofScalars}_E c'$

Informal description

For any two sequences of scalars $(c_i)_{i \in \mathbb{N}}$ and $(c'_i)_{i \in \mathbb{N}}$ in a field $\mathbb{K}$, the formal multilinear series $\sum_i (c_i + c'_i) x^i$ is equal to the sum of the formal multilinear series $\sum_i c_i x^i$ and $\sum_i c'_i x^i$, i.e., \[ \text{ofScalars}_E (c + c') = \text{ofScalars}_E c + \text{ofScalars}_E c'. \]

FormalMultilinearSeries.ofScalars_smul theorem

(x : 𝕜) : ofScalars E (x • c) = x • ofScalars E c

Full source

theorem ofScalars_smul (x : 𝕜) : ofScalars E (x • c) = x • ofScalars E c := by
  unfold ofScalars
  simp [Pi.smul_def x _, smul_smul]

Scalar Multiplication Commutes with Formal Series Construction: $\text{ofScalars}_E (x \cdot c) = x \cdot \text{ofScalars}_E c$

Informal description

For any scalar $x$ in the field $\mathbb{K}$ and any sequence of scalars $(c_i)_{i \in \mathbb{N}}$ in $\mathbb{K}$, the formal multilinear series $\sum_i (x \cdot c_i) \cdot y^i$ is equal to $x$ times the formal multilinear series $\sum_i c_i \cdot y^i$, i.e., \[ \text{ofScalars}_E (x \cdot c) = x \cdot \text{ofScalars}_E c. \]

FormalMultilinearSeries.ofScalarsSubmodule definition

: Submodule 𝕜 (FormalMultilinearSeries 𝕜 E E)

Full source

/-- The submodule generated by scalar series on `FormalMultilinearSeries 𝕜 E E`. -/
def ofScalarsSubmodule : Submodule 𝕜 (FormalMultilinearSeries 𝕜 E E) where
  carrier := {ofScalars E f | f}
  add_mem' := fun ⟨c, hc⟩ ⟨c', hc'⟩ ↦ ⟨c + c', hc' ▸ hc ▸ ofScalars_add E c c'⟩
  zero_mem' := ⟨0, ofScalars_series_eq_zero_of_scalar_zero 𝕜 E⟩
  smul_mem' := fun x _ ⟨c, hc⟩ ↦ ⟨x • c, hc ▸ ofScalars_smul E c x⟩

Submodule of scalar formal multilinear series

Informal description

The submodule of formal multilinear series over a field $\mathbb{K}$ and a vector space $E$ consisting of all series of the form $\sum_i c_i \cdot x^i$ where $(c_i)_{i \in \mathbb{N}}$ is a sequence of scalars in $\mathbb{K}$. This submodule is closed under addition and scalar multiplication, with the zero element being the series where all coefficients $c_i$ are zero.

FormalMultilinearSeries.ofScalars_apply_eq theorem

(x : E) (n : ℕ) : ofScalars E c n (fun _ ↦ x) = c n • x ^ n

Full source

theorem ofScalars_apply_eq (x : E) (n : ℕ) :
    ofScalars E c n (fun _ ↦ x) = c n • x ^ n := by
  simp [ofScalars]

Evaluation of Scalar Formal Series Term: $(\sum_i c_i x^i)_n(\lambda \_, x) = c_n x^n$

Informal description

For any element $x$ in a vector space $E$ over a field $\mathbb{K}$ and any natural number $n$, the $n$-th term of the formal multilinear series $\sum_i c_i \cdot x^i$ evaluated at the constant function $\lambda \_, x$ equals $c_n \cdot x^n$.

FormalMultilinearSeries.ofScalars_apply_eq' theorem

(x : E) : (fun n ↦ ofScalars E c n (fun _ ↦ x)) = fun n ↦ c n • x ^ n

Full source

/-- This naming follows the convention of `NormedSpace.expSeries_apply_eq'`. -/
theorem ofScalars_apply_eq' (x : E) :
    (fun n ↦ ofScalars E c n (fun _ ↦ x)) = fun n ↦ c n • x ^ n := by
  simp [ofScalars]

Term-wise Evaluation of Scalar Formal Series: $(\sum_i c_i x^i)_n(\lambda \_, x) = c_n x^n$ for all $n$

Informal description

For any element $x$ in a vector space $E$ over a field $\mathbb{K}$, the sequence of terms of the formal multilinear series $\sum_i c_i \cdot x^i$ evaluated at the constant function $\lambda \_, x$ is equal to the sequence $(c_n \cdot x^n)_{n \in \mathbb{N}}$.

FormalMultilinearSeries.ofScalarsSum definition

Full source

/-- The sum of the formal power series. Takes the value `0` outside the radius of convergence. -/
noncomputable def ofScalarsSum := (ofScalars E c).sum

Sum of scalar formal power series

Informal description

The sum of the formal power series $\sum_{i} c_i \cdot x^i$ in a vector space $E$ over a field $\mathbb{K}$, where $(c_i)_{i \in \mathbb{N}}$ is a sequence of scalars. The sum is defined to be zero outside the radius of convergence of the series.

FormalMultilinearSeries.ofScalars_sum_eq theorem

(x : E) : ofScalarsSum c x = ∑' n, c n • x ^ n

Full source

theorem ofScalars_sum_eq (x : E) : ofScalarsSum c x =
    ∑' n, c n • x ^ n := tsum_congr fun n => ofScalars_apply_eq c x n

Sum of Scalar Formal Power Series Equals Infinite Series

Informal description

For any element $x$ in a vector space $E$ over a field $\mathbb{K}$, the sum of the formal power series $\sum_{i} c_i x^i$ is equal to the infinite series $\sum_{n=0}^\infty c_n x^n$, i.e., $\text{ofScalarsSum}\, c\, x = \sum_{n=0}^\infty c_n x^n$.

FormalMultilinearSeries.ofScalarsSum_eq_tsum theorem

: ofScalarsSum c = fun (x : E) => ∑' n : ℕ, c n • x ^ n

Full source

theorem ofScalarsSum_eq_tsum : ofScalarsSum c =
    fun (x : E) => ∑' n : ℕ, c n • x ^ n := funext (ofScalars_sum_eq c)

Equality of Scalar Power Series Sum and Infinite Series

Informal description

The sum of the scalar formal power series $\text{ofScalarsSum}\, c$ is equal to the function that maps each $x \in E$ to the infinite series $\sum_{n=0}^\infty c_n x^n$, i.e., $\text{ofScalarsSum}\, c = \lambda x, \sum_{n=0}^\infty c_n x^n$.

FormalMultilinearSeries.ofScalarsSum_zero theorem

: ofScalarsSum c (0 : E) = c 0 • 1

Full source

@[simp]
theorem ofScalarsSum_zero : ofScalarsSum c (0 : E) = c 0 • 1 := by
  simp [ofScalarsSum_eq_tsum, ← ofScalars_apply_eq, ofScalars_apply_zero]

Evaluation of Scalar Power Series at Zero: $\sum_i c_i \cdot 0^i = c_0 \cdot 1$

Informal description

For any sequence of scalars $(c_i)_{i \in \mathbb{N}}$ in a field $\mathbb{K}$ and vector space $E$, the sum of the formal power series $\sum_{i} c_i \cdot x^i$ evaluated at $x = 0$ equals $c_0 \cdot 1$, where $1$ is the multiplicative identity in $E$.

FormalMultilinearSeries.ofScalarsSum_of_subsingleton theorem

[Subsingleton E] {x : E} : ofScalarsSum c x = 0

Full source

@[simp]
theorem ofScalarsSum_of_subsingleton [Subsingleton E] {x : E} : ofScalarsSum c x = 0 := by
  simp [Subsingleton.eq_zero x, Subsingleton.eq_zero (1 : E)]

Vanishing of Scalar Power Series Sum in Subsingleton Spaces

Informal description

For any vector space $E$ that is a subsingleton (i.e., has at most one element) and any sequence of scalars $(c_i)_{i \in \mathbb{N}}$, the sum of the formal power series $\sum_{i} c_i \cdot x^i$ evaluated at any $x \in E$ is equal to $0$.

FormalMultilinearSeries.ofScalarsSum_op theorem

[T2Space E] (x : E) : ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (ofScalarsSum c x)

Full source

@[simp]
theorem ofScalarsSum_op [T2Space E] (x : E) :
    ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (ofScalarsSum c x) := by
  simp [ofScalars, ofScalars_sum_eq, ← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

Opposite Sum Identity for Scalar Formal Power Series in Hausdorff Spaces

Informal description

For any element $x$ in a Hausdorff topological vector space $E$, the sum of the scalar formal power series evaluated at the opposite element $\text{op}(x)$ is equal to the opposite of the sum evaluated at $x$, i.e., $\text{ofScalarsSum}\, c\, (\text{op}\, x) = \text{op}\, (\text{ofScalarsSum}\, c\, x)$.

FormalMultilinearSeries.ofScalarsSum_unop theorem

[T2Space E] (x : Eᵐᵒᵖ) : ofScalarsSum c (MulOpposite.unop x) = MulOpposite.unop (ofScalarsSum c x)

Full source

@[simp]
theorem ofScalarsSum_unop [T2Space E] (x : Eᵐᵒᵖ) :
    ofScalarsSum c (MulOpposite.unop x) = MulOpposite.unop (ofScalarsSum c x) := by
  simp [ofScalars, ofScalars_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]

Unop Preservation of Scalar Power Series Sum in Hausdorff Spaces

Informal description

For any Hausdorff topological vector space $E$ and any element $x$ in the opposite monoid $E^{\text{op}}$, the sum of the scalar formal power series evaluated at the unopposite of $x$ is equal to the unopposite of the sum of the series evaluated at $x$, i.e., \[ \text{ofScalarsSum}\, c\, (\text{unop}\, x) = \text{unop}\, (\text{ofScalarsSum}\, c\, x). \]

FormalMultilinearSeries.ofScalars_norm_eq_mul theorem

: ‖ofScalars E c n‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖

Full source

theorem ofScalars_norm_eq_mul :
    ‖ofScalars E c n‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖ := by
  rw [ofScalars, norm_smul]

Norm Equality for Scalar Formal Power Series Term

Informal description

For any natural number $n$, the norm of the $n$-th term in the formal multilinear series $\text{ofScalars}\, E\, c$ is equal to the product of the norm of the scalar coefficient $c_n$ and the norm of the continuous multilinear map $\text{mkPiAlgebraFin}\, \mathbb{K}\, n\, E$, i.e., \[ \|\text{ofScalars}\, E\, c\, n\| = \|c_n\| \cdot \|\text{mkPiAlgebraFin}\, \mathbb{K}\, n\, E\|. \]

FormalMultilinearSeries.ofScalars_norm_le theorem

(hn : n > 0) : ‖ofScalars E c n‖ ≤ ‖c n‖

Full source

theorem ofScalars_norm_le (hn : n > 0) : ‖ofScalars E c n‖ ≤ ‖c n‖ := by
  simp only [ofScalars_norm_eq_mul]
  exact (mul_le_of_le_one_right (norm_nonneg _)
    (ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos hn))

Norm Bound for Scalar Formal Power Series Term: $\|\text{ofScalars}\, E\, c\, n\| \leq \|c_n\|$ when $n > 0$

Informal description

For any natural number $n > 0$, the norm of the $n$-th term in the formal multilinear series $\text{ofScalars}\, E\, c$ is bounded by the norm of the scalar coefficient $c_n$, i.e., \[ \|\text{ofScalars}\, E\, c\, n\| \leq \|c_n\|. \]

FormalMultilinearSeries.ofScalars_norm theorem

[NormOneClass E] : ‖ofScalars E c n‖ = ‖c n‖

Full source

@[simp]
theorem ofScalars_norm [NormOneClass E] : ‖ofScalars E c n‖ = ‖c n‖ := by
  simp [ofScalars_norm_eq_mul]

Norm Identity for Scalar Formal Power Series Term: $\|\text{ofScalars}\, E\, c\, n\| = \|c_n\|$

Informal description

For any natural number $n$ and any normed algebra $E$ over a field $\mathbb{K}$ with $\|1\| = 1$, the norm of the $n$-th term in the formal multilinear series $\sum_i c_i \cdot x^i$ is equal to the norm of the scalar coefficient $c_n$, i.e., \[ \|\text{ofScalars}\, E\, c\, n\| = \|c_n\|. \]

FormalMultilinearSeries.ofScalars_radius_ge_inv_of_tendsto theorem

 {r : ℝ≥0} (hr : r ≠ 0) (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) : (ofScalars E c).radius ≥ ofNNReal r⁻¹

Full source

theorem ofScalars_radius_ge_inv_of_tendsto {r : ℝ≥0} (hr : r ≠ 0)
    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
      (ofScalars E c).radius ≥ ofNNReal r⁻¹ := by
  refine le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
  rw [coe_lt_coe, NNReal.lt_inv_iff_mul_lt hr] at hr'
  by_cases hrz : r' = 0
  · simp [hrz]
  apply FormalMultilinearSeries.le_radius_of_summable_norm
  refine Summable.of_norm_bounded_eventually (fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
  · refine summable_of_ratio_test_tendsto_lt_one hr' ?_ ?_
    · refine (hc.eventually_ne (NNReal.coe_ne_zero.mpr hr)).mp (Eventually.of_forall ?_)
      aesop
    · simp_rw [norm_norm]
      exact tendsto_succ_norm_div_norm c hrz hc
  · filter_upwards [eventually_cofinite_ne 0] with n hn
    simp only [norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
    gcongr
    exact ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)

Lower bound for radius of convergence: $\text{radius}(\sum c_n x^n) \geq r^{-1}$ when $\lim_{n\to\infty} \frac{\|c_{n+1}\|}{\|c_n\|} = r \neq 0$

Informal description

Let $E$ be a normed algebra over a field $\mathbb{K}$ and let $(c_n)_{n \in \mathbb{N}}$ be a sequence of scalars in $\mathbb{K}$. For any nonzero nonnegative real number $r \neq 0$, if the sequence $\left(\frac{\|c_{n+1}\|}{\|c_n\|}\right)_{n \in \mathbb{N}}$ converges to $r$, then the radius of convergence of the formal power series $\sum_{n=0}^\infty c_n x^n$ is at least $r^{-1}$.

FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto theorem

 [NormOneClass E] {r : ℝ≥0} (hr : r ≠ 0) (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
  (ofScalars E c).radius = ofNNReal r⁻¹

Full source

/-- The radius of convergence of a scalar series is the inverse of the non-zero limit
`fun n ↦ ‖c n.succ‖ / ‖c n‖`. -/
theorem ofScalars_radius_eq_inv_of_tendsto [NormOneClass E] {r : ℝ≥0} (hr : r ≠ 0)
    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
      (ofScalars E c).radius = ofNNReal r⁻¹ := by
  refine le_antisymm ?_ (ofScalars_radius_ge_inv_of_tendsto E c hr hc)
  refine le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
  rw [coe_le_coe, NNReal.le_inv_iff_mul_le hr]
  have := FormalMultilinearSeries.summable_norm_mul_pow _ hr'
  contrapose! this
  apply not_summable_of_ratio_test_tendsto_gt_one this
  simp_rw [ofScalars_norm]
  exact tendsto_succ_norm_div_norm c (by aesop) hc

Radius of convergence identity: $\text{radius}(\sum c_n x^n) = r^{-1}$ when $\lim_{n\to\infty} \frac{\|c_{n+1}\|}{\|c_n\|} = r \neq 0$

Informal description

Let $E$ be a normed algebra over a field $\mathbb{K}$ with $\|1\| = 1$, and let $(c_n)_{n \in \mathbb{N}}$ be a sequence of scalars in $\mathbb{K}$. For any nonzero nonnegative real number $r \neq 0$, if the sequence $\left(\frac{\|c_{n+1}\|}{\|c_n\|}\right)_{n \in \mathbb{N}}$ converges to $r$, then the radius of convergence of the formal power series $\sum_{n=0}^\infty c_n x^n$ is equal to $r^{-1}$.

FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto theorem

 [NormOneClass E] {r : NNReal} (hr : r ≠ 0) (hc : Tendsto (fun n ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 r)) :
  (ofScalars E c).radius = ofNNReal r

Full source

/-- A convenience lemma restating the result of `ofScalars_radius_eq_inv_of_tendsto` under
the inverse ratio. -/
theorem ofScalars_radius_eq_of_tendsto [NormOneClass E] {r : NNReal} (hr : r ≠ 0)
    (hc : Tendsto (fun n ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 r)) :
      (ofScalars E c).radius = ofNNReal r := by
  suffices Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r⁻¹) by
    convert ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this
    simp
  convert hc.inv₀ (NNReal.coe_ne_zero.mpr hr) using 1
  simp

Radius of convergence identity: $\text{radius}(\sum c_n x^n) = r$ when $\lim_{n\to\infty} \frac{\|c_n\|}{\|c_{n+1}\|} = r \neq 0$

Informal description

Let $E$ be a normed algebra over a field $\mathbb{K}$ with $\|1\| = 1$, and let $(c_n)_{n \in \mathbb{N}}$ be a sequence of scalars in $\mathbb{K}$. For any nonzero nonnegative real number $r \neq 0$, if the sequence $\left(\frac{\|c_n\|}{\|c_{n+1}\|}\right)_{n \in \mathbb{N}}$ converges to $r$, then the radius of convergence of the formal power series $\sum_{n=0}^\infty c_n x^n$ is equal to $r$.

FormalMultilinearSeries.ofScalars_radius_eq_top_of_tendsto theorem

 (hc : ∀ᶠ n in atTop, c n ≠ 0) (hc' : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)) : (ofScalars E c).radius = ⊤

Full source

/-- The ratio test stating that if `‖c n.succ‖ / ‖c n‖` tends to zero, the radius is unbounded.
This requires that the coefficients are eventually non-zero as
`‖c n.succ‖ / 0 = 0` by convention. -/
theorem ofScalars_radius_eq_top_of_tendsto (hc : ∀ᶠ n in atTop, c n ≠ 0)
    (hc' : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)) : (ofScalars E c).radius = ⊤ := by
  refine radius_eq_top_of_summable_norm _ fun r' ↦ ?_
  by_cases hrz : r' = 0
  · apply Summable.comp_nat_add (k := 1)
    simp [hrz]
    exact (summable_const_iff 0).mpr rfl
  · refine Summable.of_norm_bounded_eventually (fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
    · apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))
      · simp only [norm_norm]
        exact mul_zero (_ : ℝ) ▸ tendsto_succ_norm_div_norm _ hrz (NNReal.coe_zero ▸ hc')
      · aesop
    · filter_upwards [eventually_cofinite_ne 0] with n hn
      simp only [norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
      gcongr
      exact ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)

Infinite Radius of Convergence for Scalar Power Series with Vanishing Ratio Test

Informal description

Let $E$ be a normed space with norm one class, and let $(c_n)_{n \in \mathbb{N}}$ be a sequence of scalars such that: 1. $c_n \neq 0$ for all sufficiently large $n$, and 2. The ratio $\frac{\|c_{n+1}\|}{\|c_n\|}$ tends to $0$ as $n \to \infty$. Then the radius of convergence of the formal power series $\sum_{n=0}^\infty c_n x^n$ is infinite, i.e., $\text{radius}(\sum_{n} c_n x^n) = \infty$.

FormalMultilinearSeries.ofScalars_radius_eq_zero_of_tendsto theorem

[NormOneClass E] (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop) : (ofScalars E c).radius = 0

Full source

/-- If `‖c n.succ‖ / ‖c n‖` is unbounded, then the radius of convergence is zero. -/
theorem ofScalars_radius_eq_zero_of_tendsto [NormOneClass E]
    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop) : (ofScalars E c).radius = 0 := by
  suffices (ofScalars E c).radius ≤ 0 by aesop
  refine le_of_forall_nnreal_lt (fun r hr ↦ ?_)
  rw [← coe_zero, coe_le_coe]
  have := FormalMultilinearSeries.summable_norm_mul_pow _ hr
  contrapose! this
  apply not_summable_of_ratio_norm_eventually_ge one_lt_two
  · contrapose! hc
    apply not_tendsto_atTop_of_tendsto_nhds (a:=0)
    rw [not_frequently] at hc
    apply Tendsto.congr' ?_ tendsto_const_nhds
    filter_upwards [hc] with n hc'
    rw [ofScalars_norm, norm_mul, norm_norm, not_ne_iff, mul_eq_zero] at hc'
    cases hc' <;> aesop
  · filter_upwards [hc.eventually_ge_atTop (2*r⁻¹), eventually_ne_atTop 0] with n hc hn
    simp only [ofScalars_norm, norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
    rw [mul_comm ‖c n‖, ← mul_assoc, ← div_le_div_iff₀, mul_div_assoc]
    · convert hc
      rw [pow_succ, div_mul_cancel_left₀, NNReal.coe_inv]
      aesop
    · aesop
    · refine Ne.lt_of_le (fun hr' ↦ Not.elim ?_ hc) (norm_nonneg _)
      rw [← hr']
      simp [this]

Zero Radius of Convergence for Unbounded Ratio of Coefficients

Informal description

Let $E$ be a normed algebra with $\|1\| = 1$ and let $(c_n)_{n \in \mathbb{N}}$ be a sequence of scalars. If the ratio $\frac{\|c_{n+1}\|}{\|c_n\|}$ tends to infinity as $n$ tends to infinity, then the radius of convergence of the formal power series $\sum_{n=0}^\infty c_n x^n$ is zero.

FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto_ENNReal theorem

 [NormOneClass E] {r : ℝ≥0∞} (hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)) :
  (ofScalars E c).radius = r⁻¹

Full source

/-- This theorem combines the results of the special cases above, using `ENNReal` division to remove
the requirement that the ratio is eventually non-zero. -/
theorem ofScalars_radius_eq_inv_of_tendsto_ENNReal [NormOneClass E] {r : ℝ≥0∞}
    (hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)) :
      (ofScalars E c).radius = r⁻¹ := by
  rcases ENNReal.trichotomy r with (hr | hr | hr)
  · simp_rw [hr, inv_zero] at hc' ⊢
    by_cases h : (∀ᶠ (n : ℕ) in atTop, c n ≠ 0)
    · apply ofScalars_radius_eq_top_of_tendsto E c h ?_
      refine Tendsto.congr' ?_ <| (tendsto_toReal zero_ne_top).comp hc'
      filter_upwards [h]
      simp
    · apply (ofScalars E c).radius_eq_top_of_eventually_eq_zero
      simp only [eventually_atTop, not_exists, not_forall, Classical.not_imp, not_not] at h ⊢
      obtain ⟨ti, hti⟩ := eventually_atTop.mp (hc'.eventually_ne zero_ne_top)
      obtain ⟨zi, hzi, z⟩ := h ti
      refine ⟨zi, Nat.le_induction (ofScalars_eq_zero_of_scalar_zero E z) fun n hmn a ↦ ?_⟩
      nontriviality E
      simp only [ofScalars_eq_zero] at a ⊢
      contrapose! hti
      exact ⟨n, hzi.trans hmn, ENNReal.div_eq_top.mpr (by simp [a, hti])⟩
  · simp_rw [hr, inv_top] at hc' ⊢
    apply ofScalars_radius_eq_zero_of_tendsto E c ((tendsto_add_atTop_iff_nat 1).mp ?_)
    refine tendsto_ofReal_nhds_top.mp (Tendsto.congr' ?_ ((tendsto_add_atTop_iff_nat 1).mpr hc'))
    filter_upwards [hc'.eventually_ne top_ne_zero] with n hn
    apply (ofReal_div_of_pos (Ne.lt_of_le (Ne.symm ?_) (norm_nonneg _))).symm
    aesop
  · have hr' := toReal_ne_zero.mp hr.ne.symm
    have hr'' := toNNReal_ne_zero.mpr hr' -- this result could go in ENNReal
    convert ofScalars_radius_eq_inv_of_tendsto E c hr'' ?_
    · simp [ENNReal.coe_inv hr'', ENNReal.coe_toNNReal (toReal_ne_zero.mp hr.ne.symm).2]
    · simp_rw [ENNReal.coe_toNNReal_eq_toReal]
      refine Tendsto.congr' ?_ <| (tendsto_toReal hr'.2).comp hc'
      filter_upwards [hc'.eventually_ne hr'.1, hc'.eventually_ne hr'.2]
      simp

Radius of Convergence Identity: $\text{radius}(\sum c_n x^n) = r^{-1}$ for Extended Ratio Test

Informal description

Let $E$ be a normed algebra with $\|1\| = 1$ and let $(c_n)_{n \in \mathbb{N}}$ be a sequence of scalars. If the sequence $\left(\frac{\|c_{n+1}\|}{\|c_n\|}\right)_{n \in \mathbb{N}}$ converges to an extended non-negative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ when mapped via $\text{ENNReal.ofReal}$, then the radius of convergence of the formal power series $\sum_{n=0}^\infty c_n x^n$ is equal to $r^{-1}$.

Main definitions / results: