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.ofScalars_radius_eq_of_tendsto: the ratio test for an analytic function defined in terms of a formal power series∑ cᵢ • xⁱ.
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
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
- FormalMultilinearSeries.ofScalarsSum c x = (FormalMultilinearSeries.ofScalars E c).sum x
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'.
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.ofScalars_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.ofScalars_unop
{𝕜 : Type u_1}
{E : Type u_2}
[Field 𝕜]
[Ring E]
[Algebra 𝕜 E]
[TopologicalSpace E]
[TopologicalRing E]
(c : ℕ → 𝕜)
[T2Space E]
(x : Eᵐᵒᵖ)
:
@[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
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_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 ratio of the norms of the coefficients.
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.