Scalar series

This file contains API for analytic functions ∑ cᵢ • xⁱ defined in terms of scalars c₀, c₁, c₂, ….

Main definitions / results:

• FormalMultilinearSeries.ofScalars: the formal power series ∑ cᵢ • xⁱ.
• FormalMultilinearSeries.ofScalarsSum: the sum of such a power series, if it exists, and zero otherwise.
• FormalMultilinearSeries.ofScalars_radius_eq_(zero/inv/top)_of_tendsto: the ratio test for an analytic function defined in terms of a formal power series ∑ cᵢ • xⁱ.
• FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto_ENNReal: the ratio test for an analytic function using ENNReal division for all values ℝ≥0∞.

def FormalMultilinearSeries.ofScalars {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) : FormalMultilinearSeries 𝕜 E E

Formal power series of ∑ cᵢ • xⁱ for some scalar field 𝕜 and ring algebra E

Equations

• FormalMultilinearSeries.ofScalars E c n = c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E

@[simp]

theorem FormalMultilinearSeries.ofScalars_eq_zero {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] {c : ℕ → 𝕜} [Nontrivial E] (n : ℕ) : ofScalars E c n = 0 ↔ c n = 0

@[simp]

theorem FormalMultilinearSeries.ofScalars_eq_zero_of_scalar_zero {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] {c : ℕ → 𝕜} {n : ℕ} (hc : c n = 0) : ofScalars E c n = 0

@[simp]

theorem FormalMultilinearSeries.ofScalars_series_eq_zero {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] {c : ℕ → 𝕜} [Nontrivial E] : ofScalars E c = 0 ↔ c = 0

@[simp]

theorem FormalMultilinearSeries.ofScalars_series_eq_zero_of_scalar_zero (𝕜 : Type u_1) (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] : ofScalars E 0 = 0

@[simp]

theorem FormalMultilinearSeries.ofScalars_series_of_subsingleton {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] {c : ℕ → 𝕜} [Subsingleton E] : ofScalars E c = 0

theorem FormalMultilinearSeries.ofScalars_series_injective (𝕜 : Type u_1) (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] [Nontrivial E] : Function.Injective (ofScalars E)

@[simp]

theorem FormalMultilinearSeries.ofScalars_series_eq_iff {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) [Nontrivial E] (c' : ℕ → 𝕜) : ofScalars E c = ofScalars E c' ↔ c = c'

theorem FormalMultilinearSeries.ofScalars_apply_zero {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) (n : ℕ) : ((ofScalars E c n) fun (x : Fin n) => 0) = Pi.single 0 (c 0 • 1) n

@[simp]

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

theorem FormalMultilinearSeries.ofScalars_add {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c c' : ℕ → 𝕜) : ofScalars E (c + c') = ofScalars E c + ofScalars E c'

theorem FormalMultilinearSeries.ofScalars_smul {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) (x : 𝕜) : ofScalars E (x • c) = x • ofScalars E c

def FormalMultilinearSeries.ofScalarsSubmodule (𝕜 : Type u_1) (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] : Submodule 𝕜 (FormalMultilinearSeries 𝕜 E E)

The submodule generated by scalar series on FormalMultilinearSeries 𝕜 E E.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalMultilinearSeries.ofScalars_apply_eq {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) (x : E) (n : ℕ) : ((ofScalars E c n) fun (x_1 : Fin n) => x) = c n • x ^ n

theorem FormalMultilinearSeries.ofScalars_apply_eq' {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) (x : E) : (fun (n : ℕ) => (ofScalars E c n) fun (x_1 : Fin n) => x) = fun (n : ℕ) => c n • x ^ n

This naming follows the convention of NormedSpace.expSeries_apply_eq'.

noncomputable def FormalMultilinearSeries.ofScalarsSum {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) (x : E) : E

The sum of the formal power series. Takes the value 0 outside the radius of convergence.

Equations

• FormalMultilinearSeries.ofScalarsSum c = (FormalMultilinearSeries.ofScalars E c).sum

theorem FormalMultilinearSeries.ofScalars_sum_eq {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) (x : E) : ofScalarsSum c x = ∑' (n : ℕ), c n • x ^ n

theorem FormalMultilinearSeries.ofScalarsSum_eq_tsum {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) : ofScalarsSum c = fun (x : E) => ∑' (n : ℕ), c n • x ^ n

@[simp]

theorem FormalMultilinearSeries.ofScalarsSum_zero {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) : ofScalarsSum c 0 = c 0 • 1

@[simp]

theorem FormalMultilinearSeries.ofScalarsSum_of_subsingleton {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) [Subsingleton E] {x : E} : ofScalarsSum c x = 0

@[simp]

theorem FormalMultilinearSeries.ofScalarsSum_op {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) [T2Space E] (x : E) : ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (ofScalarsSum c x)

@[simp]

theorem FormalMultilinearSeries.ofScalarsSum_unop {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) [T2Space E] (x : Eᵐᵒᵖ) : ofScalarsSum c (MulOpposite.unop x) = MulOpposite.unop (ofScalarsSum c x)

theorem FormalMultilinearSeries.ofScalars_norm_eq_mul {𝕜 : Type u_1} (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedRing E] [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) (n : ℕ) : ‖ofScalars E c n‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖

theorem FormalMultilinearSeries.ofScalars_norm_le {𝕜 : Type u_1} (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedRing E] [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) (n : ℕ) (hn : n > 0) : ‖ofScalars E c n‖ ≤ ‖c n‖

@[simp]

theorem FormalMultilinearSeries.ofScalars_norm {𝕜 : Type u_1} (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedRing E] [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) (n : ℕ) [NormOneClass E] : ‖ofScalars E c n‖ = ‖c n‖

theorem FormalMultilinearSeries.ofScalars_radius_ge_inv_of_tendsto {𝕜 : Type u_1} (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedRing E] [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) {r : NNReal} (hr : r ≠ 0) (hc : Filter.Tendsto (fun (n : ℕ) => ‖c n.succ‖ / ‖c n‖) Filter.atTop (nhds ↑r)) : (ofScalars E c).radius ≥ ↑r⁻¹

theorem FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto {𝕜 : Type u_1} (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedRing E] [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) [NormOneClass E] {r : NNReal} (hr : r ≠ 0) (hc : Filter.Tendsto (fun (n : ℕ) => ‖c n.succ‖ / ‖c n‖) Filter.atTop (nhds ↑r)) : (ofScalars E c).radius = ↑r⁻¹

The radius of convergence of a scalar series is the inverse of the non-zero limit fun n ↦ ‖c n.succ‖ / ‖c n‖.

theorem FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto {𝕜 : Type u_1} (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedRing E] [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) [NormOneClass E] {r : NNReal} (hr : r ≠ 0) (hc : Filter.Tendsto (fun (n : ℕ) => ‖c n‖ / ‖c n.succ‖) Filter.atTop (nhds ↑r)) : (ofScalars E c).radius = ↑r

A convenience lemma restating the result of ofScalars_radius_eq_inv_of_tendsto under the inverse ratio.

theorem FormalMultilinearSeries.ofScalars_radius_eq_top_of_tendsto {𝕜 : Type u_1} (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedRing E] [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) (hc : ∀ᶠ (n : ℕ) in Filter.atTop, c n ≠ 0) (hc' : Filter.Tendsto (fun (n : ℕ) => ‖c n.succ‖ / ‖c n‖) Filter.atTop (nhds 0)) : (ofScalars E c).radius = ⊤

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 FormalMultilinearSeries.ofScalars_radius_eq_zero_of_tendsto {𝕜 : Type u_1} (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedRing E] [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) [NormOneClass E] (hc : Filter.Tendsto (fun (n : ℕ) => ‖c n.succ‖ / ‖c n‖) Filter.atTop Filter.atTop) : (ofScalars E c).radius = 0

If ‖c n.succ‖ / ‖c n‖ is unbounded, then the radius of convergence is zero.

theorem FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto_ENNReal {𝕜 : Type u_1} (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedRing E] [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) [NormOneClass E] {r : ENNReal} (hc' : Filter.Tendsto (fun (n : ℕ) => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) Filter.atTop (nhds r)) : (ofScalars E c).radius = r⁻¹

This theorem combines the results of the special cases above, using ENNReal division to remove the requirement that the ratio is eventually non-zero.