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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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)

source

@[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'

source

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

source

@[simp]

theorem FormalMultilinearSeries.coeff_ofScalars {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] {p : ℕ → 𝕜} {n : ℕ} :

(ofScalars 𝕜 p).coeff n = p n

source

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'

source

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

source

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

(ofScalars E c).compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 E) = ofScalars E fun (k : ℕ) => (-1) ^ k * c k

source

theorem FormalMultilinearSeries.ofScalars_comp_neg {𝕜 : Type u_1} (E : Type u_2) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) (f : E →L[𝕜] E) :

(ofScalars E c).compContinuousLinearMap (-f) = (ofScalars E fun (k : ℕ) => (-1) ^ k * c k).compContinuousLinearMap f

source

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.

Instances For

source

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

source

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'.

source

noncomputable def FormalMultilinearSeries.ofScalarsSum {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c : ℕ → 𝕜) (x : 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

Instances For

source

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

source

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

source

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

source

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

source

@[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)

source

@[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)

source

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‖

source

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‖

source

@[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‖

source

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⁻¹

source

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‖.

source

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.

source

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.

source

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.

source

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.

Documentation

Mathlib.Analysis.Analytic.OfScalars

Scalar series #

Main definitions / results: #