PowerSeries.exp_pow_eq_rescale_exp
theorem PowerSeries.exp_pow_eq_rescale_exp :
∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] (k : ℕ),
PowerSeries.exp A ^ k = (PowerSeries.rescale ↑k) (PowerSeries.exp A)
This theorem states that in the context of a commutative ring `A` over which there is a rational number algebra structure, for any natural number `k`, the `k`-th power of the power series for the exponential function at zero is equal to the rescaling of the power series for the exponential function at zero by `k`. In mathematical terms, this means that $(e^{X})^k = e^{kX}$, where $e^X$ is the power series for the exponential function at zero. This is analogous to the property of the exponential function in real and complex analysis where the exponentiation of k times a number is the same as the number raised to the kth power.
More concisely: In a commutative ring `A` with a rational number algebra structure, for any natural number `k`, the `k`-th power of the power series for the exponential function at zero equals the rescaled power series, that is, $(e^{X})^k = e^{kX}$.
|
PowerSeries.coeff_invUnitsSub
theorem PowerSeries.coeff_invUnitsSub :
∀ {R : Type u_1} [inst : Ring R] (u : Rˣ) (n : ℕ),
(PowerSeries.coeff R n) (PowerSeries.invUnitsSub u) = 1 /ₚ u ^ (n + 1)
The theorem `PowerSeries.coeff_invUnitsSub` states that for any ring `R`, any unit `u` of `R`, and any natural number `n`, the `n`th coefficient of the power series for `1 / (u - x)` is `1 /ₚ u ^ (n + 1)`. In other words, it says that when you construct a power series as the series `1 / (u - x)`, then the coefficient of `x^n` in that series is `1 / u ^ (n + 1)`. This theorem essentially describes the structure of the power series for `1 / (u - x)`.
More concisely: The `n`th coefficient of the power series expansion of `1 / (u - x)` in a ring `R` with a unit `u` is equal to `1 / u ^ (n + 1)`.
|
PowerSeries.exp_mul_exp_neg_eq_one
theorem PowerSeries.exp_mul_exp_neg_eq_one :
∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A],
PowerSeries.exp A * PowerSeries.evalNegHom (PowerSeries.exp A) = 1
This theorem states that the product of the power series of the exponential function at a point 'x' and the power series of the exponential function at '-x' is equal to one, for any commutative ring 'A' that has a structure of an algebra over the rationals. In other words, it shows that $e^{x} * e^{-x} = 1$ in the context of power series.
More concisely: For any commutative ring A with a rational algebra structure, the product of the power series expansions of $e^x$ and $e^{-x}$ equals 1.
|
PowerSeries.coeff_exp
theorem PowerSeries.coeff_exp :
∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℚ A] (n : ℕ),
(PowerSeries.coeff A n) (PowerSeries.exp A) = (algebraMap ℚ A) (1 / ↑n.factorial)
The theorem `PowerSeries.coeff_exp` expresses that for any ring `A`, equipped with an algebra structure over the rational numbers `ℚ`, and for any natural number `n`, the `n`-th coefficient of the power series for the exponential function at zero is equal to the algebraic map of `(1 / (n factorial))`, where `n factorial` is represented as `Nat.factorial n`. In other words, when we look at the `n`-th term of the exponential power series, it is equal to `1 / n!` transformed into our algebra `A` using the algebra's structure.
More concisely: For any commutative ring `A` equipped with an algebra structure over the rational numbers, the `n`-th coefficient of the power series for the exponential function at zero equals `1 / (n!)|\_A`, where `n!` is the factorial of `n` and `|_A` denotes the algebra homomorphism from the rational numbers to `A`.
|
PowerSeries.exp_pow_sum
theorem PowerSeries.exp_pow_sum :
∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] (n : ℕ),
((Finset.range n).sum fun k => PowerSeries.exp A ^ k) =
PowerSeries.mk fun p => (Finset.range n).sum fun k => ↑k ^ p * (algebraMap ℚ A) (↑p.factorial)⁻¹
This theorem, `PowerSeries.exp_pow_sum`, states that for any commutative ring `A` with an algebra structure over the rational numbers `ℚ`, and for any natural number `n`, the sum of the `k`th powers of the exponential power series for all `k` in the range from 0 to `n - 1` is equal to the formal power series whose `p`th term is the sum over the range from 0 to `n - 1` of `k` raised to the power `p` times the reciprocal of `p!` (factorial of `p`), where the sum and the power series are understood in the ring `A`. In mathematical notation, this is saying that:
$\sum_{k = 0}^{n - 1} (e^{X})^k = \sum_{p = 0}^{\infty} \sum_{k = 0}^{n - 1} \frac{k^p}{p!}X^p$.
More concisely: For any commutative ring `A` with an algebra structure over the rational numbers `ℚ`, and for any natural number `n`, the sum of the power series $\sum\_{k = 0}^{n - 1} (e^X)^k$ equals the power series $\sum\_{p = 0}^{\infty} \sum\_{k = 0}^{n - 1} \frac{k^p}{p!}X^p$ in `A`.
|
PowerSeries.exp_mul_exp_eq_exp_add
theorem PowerSeries.exp_mul_exp_eq_exp_add :
∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] (a b : A),
(PowerSeries.rescale a) (PowerSeries.exp A) * (PowerSeries.rescale b) (PowerSeries.exp A) =
(PowerSeries.rescale (a + b)) (PowerSeries.exp A)
The theorem `PowerSeries.exp_mul_exp_eq_exp_add` states that for a commutative ring `A` with an algebra structure over the rational numbers, the product of two exponential power series, each rescaled by a different factor, is equal to the exponential power series rescaled by the sum of the two factors. In other words, given any two elements `a` and `b` of `A`, `e^{aX} * e^{bX} = e^{(a + b)X}`, mimicking the familiar identity from calculus in the context of power series.
More concisely: For any commutative ring `A` with an algebra structure over the rational numbers, `e^{aX} * e^{bX} = e^{(a + b)X}` for all `a, b ∈ A`.
|