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 usingENNRealdivision for all valuesℝ≥0∞.
def
FormalMultilinearSeries.ofScalars
{𝕜 : Type u_1}
(E : Type u_2)
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing 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
@[simp]
theorem
FormalMultilinearSeries.ofScalars_eq_zero
{𝕜 : Type u_1}
(E : Type u_2)
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
{c : ℕ → 𝕜}
[Nontrivial E]
(n : ℕ)
:
FormalMultilinearSeries.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]
[TopologicalRing E]
{c : ℕ → 𝕜}
{n : ℕ}
(hc : c n = 0)
:
FormalMultilinearSeries.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]
[TopologicalRing E]
{c : ℕ → 𝕜}
[Nontrivial E]
:
FormalMultilinearSeries.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]
[TopologicalRing E]
:
@[simp]
theorem
FormalMultilinearSeries.ofScalars_series_of_subsingleton
{𝕜 : Type u_1}
(E : Type u_2)
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
{c : ℕ → 𝕜}
[Subsingleton E]
:
theorem
FormalMultilinearSeries.ofScalars_series_injective
(𝕜 : Type u_1)
(E : Type u_2)
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
[Nontrivial E]
:
@[simp]
theorem
FormalMultilinearSeries.ofScalars_series_eq_iff
{𝕜 : Type u_1}
(E : Type u_2)
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
(c : ℕ → 𝕜)
[Nontrivial E]
(c' : ℕ → 𝕜)
:
FormalMultilinearSeries.ofScalars E c = FormalMultilinearSeries.ofScalars E c' ↔ c = c'
theorem
FormalMultilinearSeries.ofScalars_apply_zero
{𝕜 : Type u_1}
(E : Type u_2)
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
(c : ℕ → 𝕜)
(n : ℕ)
:
((FormalMultilinearSeries.ofScalars E c n) fun (x : Fin n) => 0) = Pi.single 0 (c 0 • 1) n
theorem
FormalMultilinearSeries.ofScalars_add
{𝕜 : Type u_1}
(E : Type u_2)
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
(c c' : ℕ → 𝕜)
:
theorem
FormalMultilinearSeries.ofScalars_smul
{𝕜 : Type u_1}
(E : Type u_2)
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
(c : ℕ → 𝕜)
(x : 𝕜)
:
FormalMultilinearSeries.ofScalars E (x • c) = x • FormalMultilinearSeries.ofScalars E c
def
FormalMultilinearSeries.ofScalarsSubmodule
(𝕜 : Type u_1)
(E : Type u_2)
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing 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
theorem
FormalMultilinearSeries.ofScalars_apply_eq
{𝕜 : Type u_1}
{E : Type u_2}
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
(c : ℕ → 𝕜)
(x : E)
(n : ℕ)
:
((FormalMultilinearSeries.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]
[TopologicalRing E]
(c : ℕ → 𝕜)
(x : E)
:
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]
[TopologicalRing E]
(c : ℕ → 𝕜)
(x : E)
:
E
The sum of the formal power series. Takes the value 0 outside the radius of convergence.
Equations
Instances For
theorem
FormalMultilinearSeries.ofScalars_sum_eq
{𝕜 : Type u_1}
{E : Type u_2}
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
(c : ℕ → 𝕜)
(x : E)
:
FormalMultilinearSeries.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]
[TopologicalRing E]
(c : ℕ → 𝕜)
:
FormalMultilinearSeries.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]
[TopologicalRing E]
(c : ℕ → 𝕜)
:
FormalMultilinearSeries.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]
[TopologicalRing E]
(c : ℕ → 𝕜)
[Subsingleton E]
{x : E}
:
@[simp]
theorem
FormalMultilinearSeries.ofScalarsSum_op
{𝕜 : Type u_1}
{E : Type u_2}
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
(c : ℕ → 𝕜)
[T2Space E]
(x : E)
:
@[simp]
theorem
FormalMultilinearSeries.ofScalarsSum_unop
{𝕜 : Type u_1}
{E : Type u_2}
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
(c : ℕ → 𝕜)
[T2Space E]
(x : Eᵐᵒᵖ)
:
theorem
FormalMultilinearSeries.ofScalars_norm_eq_mul
{𝕜 : Type u_1}
(E : Type u_2)
[NontriviallyNormedField 𝕜]
[NormedRing E]
[NormedAlgebra 𝕜 E]
(c : ℕ → 𝕜)
(n : ℕ)
:
theorem
FormalMultilinearSeries.ofScalars_norm_le
{𝕜 : Type u_1}
(E : Type u_2)
[NontriviallyNormedField 𝕜]
[NormedRing E]
[NormedAlgebra 𝕜 E]
(c : ℕ → 𝕜)
(n : ℕ)
(hn : n > 0)
:
@[simp]
theorem
FormalMultilinearSeries.ofScalars_norm
{𝕜 : Type u_1}
(E : Type u_2)
[NontriviallyNormedField 𝕜]
[NormedRing E]
[NormedAlgebra 𝕜 E]
(c : ℕ → 𝕜)
(n : ℕ)
[NormOneClass E]
:
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))
:
(FormalMultilinearSeries.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))
:
(FormalMultilinearSeries.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))
:
(FormalMultilinearSeries.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))
:
(FormalMultilinearSeries.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)
:
(FormalMultilinearSeries.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))
:
(FormalMultilinearSeries.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.