PowerSeries.le_order
theorem PowerSeries.le_order :
∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R) (n : PartENat),
(∀ (i : ℕ), ↑i < n → (PowerSeries.coeff R i) φ = 0) → n ≤ φ.order
The theorem `PowerSeries.le_order` states that, for a given formal power series `φ` over a semiring `R` and a natural number `n` (possibly infinite), if all the coefficients of the series at indices less than `n` are zero, then the order of the power series is at least `n`. In other words, the lowest index at which the power series has a non-zero coefficient is not less than `n`.
More concisely: If `φ` is a formal power series over semiring `R` with all coefficients at indices less than `n` being zero, then the order of `φ` is at least `n`.
|
PowerSeries.order_eq
theorem PowerSeries.order_eq :
∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} {n : PartENat},
φ.order = n ↔
(∀ (i : ℕ), ↑i = n → (PowerSeries.coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (PowerSeries.coeff R i) φ = 0
The theorem `PowerSeries.order_eq` states that for any given semiring `R` and a formal power series `φ` over `R`, the order of `φ` is exactly `n` (where `n` is a natural number or infinity) if and only if the `n`th coefficient of the power series is nonzero and all coefficients for indices less than `n` are zero. In other words, a power series order is determined by the position of its first non-zero coefficient.
More concisely: A formal power series over a semiring has order equal to the smallest index of a non-zero coefficient.
|
PowerSeries.coeff_of_lt_order
theorem PowerSeries.coeff_of_lt_order :
∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} (n : ℕ), ↑n < φ.order → (PowerSeries.coeff R n) φ = 0 := by
sorry
The theorem `PowerSeries.coeff_of_lt_order` states that for any coefficient type `R` with a semiring structure, any formal power series `φ` over `R`, and any natural number `n`, if `n` is strictly smaller than the order of the power series `φ`, then the `n`th coefficient of the power series `φ` is `0`. In other words, in a formal power series, any term whose degree is less than the order of the series has a zero coefficient.
More concisely: For any semiring `R`, formal power series `φ` over `R` of order `k`, and natural number `n` with `n < k`, the `n`th coefficient of `φ` is `0`.
|
PowerSeries.order_eq_top
theorem PowerSeries.order_eq_top : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, φ.order = ⊤ ↔ φ = 0 := by
sorry
This theorem states that for any type `R` equipped with a semiring structure, and for any formal power series `φ` over `R`, the order of `φ` is infinite if and only if `φ` equals to the zero power series. In other words, the zero power series is uniquely characterized by having an infinite order.
More concisely: For any semiring `R` and formal power series `φ` over `R`, `φ` has infinite order if and only if `φ` is the zero power series.
|
PowerSeries.order_mul_ge
theorem PowerSeries.order_mul_ge :
∀ {R : Type u_1} [inst : Semiring R] (φ ψ : PowerSeries R), φ.order + ψ.order ≤ (φ * ψ).order
This theorem states that for any given type `R` that forms a semiring, and for any two formal power series `φ` and `ψ` over `R`, the order of the product of `φ` and `ψ` is always greater than or equal to the sum of their individual orders. In other words, if we multiply two formal power series, the order of the resulting power series cannot be less than the sum of the orders of the original power series.
More concisely: For any semiring `R` and formal power series `φ` and `ψ` over `R`, the order of their product `φ ∘ ψ` is greater than or equal to the sum of their individual orders. (Here, `∘` denotes multiplication of formal power series.)
|
PowerSeries.order_le
theorem PowerSeries.order_le :
∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} (n : ℕ), (PowerSeries.coeff R n) φ ≠ 0 → φ.order ≤ ↑n := by
sorry
This theorem states that for any semiring `R` and for any formal power series `φ` over `R`, if the `n`th coefficient of `φ` is nonzero, then the order of `φ` is less than or equal to `n`. In other words, if a term in the power series has a nonzero coefficient, the order of the entire series cannot be more than the index of that term.
More concisely: For any semiring `R` and formal power series `φ` over `R`, if the `n`-th coefficient of `φ` is nonzero, then the order of `φ` is bounded by `n`.
|
PowerSeries.order_X_pow
theorem PowerSeries.order_X_pow :
∀ {R : Type u_1} [inst : Semiring R] [inst_1 : Nontrivial R] (n : ℕ), (PowerSeries.X ^ n).order = ↑n
This theorem states that, for any given natural number `n` and any semiring `R` that is not trivial (i.e., it is not the case that for all elements `a` and `b` in `R`, `a = b`), the order of the formal power series `X^n` is `n`. Here, 'order' refers to the smallest exponent in the series. The formal power series `X^n` is a series where each term has a coefficient multiplied by `X` raised to the power `n`.
More concisely: For any natural number `n` and non-trivial semiring `R`, the order of the formal power series `X^n` is `n`.
|
PowerSeries.order_eq_nat
theorem PowerSeries.order_eq_nat :
∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} {n : ℕ},
φ.order = ↑n ↔ (PowerSeries.coeff R n) φ ≠ 0 ∧ ∀ i < n, (PowerSeries.coeff R i) φ = 0
This theorem is about the order of a formal power series. It says that the order of a formal power series `φ` is exactly `n`, where `φ` is over a semiring `R` and `n` is a natural number, if and only if the `n`th coefficient of `φ` is nonzero and all the coefficients of `φ` for indices `i` less than `n` are zero. In other words, the series begins with `n` terms of zero coefficients, and the coefficient of the `n`th term is nonzero.
More concisely: A formal power series `φ` over a semiring `R` has order `n` if and only if its `n`th coefficient is nonzero and all its coefficients for indices less than `n` are zero.
|
PowerSeries.order_monomial_of_ne_zero
theorem PowerSeries.order_monomial_of_ne_zero :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R), a ≠ 0 → ((PowerSeries.monomial R n) a).order = ↑n
The theorem states that for any semiring `R`, given a non-zero coefficient `a` from `R` and a natural number `n`, the order of the monomial `a*X^n` (interpreted as a formal power series), is `n`. This means that the highest power `n` such that `X^n` divides the formal power series `a*X^n` (which is `n` itself) if the coefficient `a` is non-zero.
More concisely: For any semiring `R` and non-zero `a` in `R` and natural number `n`, the order of the monomial `a*X^n` as a formal power series is equal to `n`.
|
PowerSeries.order_zero
theorem PowerSeries.order_zero : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.order 0 = ⊤
The theorem `PowerSeries.order_zero` states that for any semiring `R`, the order of the zero power series is infinite. In other words, if we consider the power series where all coefficients are zero, then we say its 'order' (a measure of the greatest power of `X` that divides the series) is infinity for any semiring `R`. This is consistent with the convention where the order is `⊤` if and only if the power series equals `0`.
More concisely: For any semiring R, the order of the power series with all coefficients equal to 0 is infinite.
|
PowerSeries.le_order_add
theorem PowerSeries.le_order_add :
∀ {R : Type u_1} [inst : Semiring R] (φ ψ : PowerSeries R), min φ.order ψ.order ≤ (φ + ψ).order
The theorem `PowerSeries.le_order_add` states that for any given semiring `R` and any two formal power series `φ` and `ψ` over `R`, the order of the sum of `φ` and `ψ` is greater than or equal to the minimum of the orders of `φ` and `ψ`. In other words, while adding two formal power series, the lowest degree with non-zero coefficient in the resulting power series will be at least the smallest of the lowest degrees with non-zero coefficients in the original two series.
More concisely: For any semiring R and formal power series φ and ψ over R, the order of φ + ψ is greater than or equal to min (order φ, order ψ).
|
PowerSeries.nat_le_order
theorem PowerSeries.nat_le_order :
∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R) (n : ℕ),
(∀ i < n, (PowerSeries.coeff R i) φ = 0) → ↑n ≤ φ.order
The theorem states that for any formal power series `φ` over a semiring `R`, and for any natural number `n`, if all coefficients of `φ` at indices less than `n` are zero, then the order of the power series `φ` is at least `n`. In other words, the order of a formal power series cannot be less than the first index at which its coefficient is non-zero.
More concisely: If a formal power series φ over a semiring has all coefficients at indices less than n equal to 0, then the order of φ is at least n.
|
PowerSeries.coeff_order
theorem PowerSeries.coeff_order :
∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} (h : φ.order.Dom),
(PowerSeries.coeff R (φ.order.get h)) φ ≠ 0
This theorem states that if a formal power series over a coefficient type 'R', where 'R' is a semiring, has a finite order, then the coefficient at the index corresponding to this order is non-zero. In other words, the coefficient associated with the order of the series, when it is finite, cannot be zero.
More concisely: If a formal power series over a semiring 'R' has finite order, then its coefficient of the maximum order is non-zero.
|
PowerSeries.order_one
theorem PowerSeries.order_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : Nontrivial R], PowerSeries.order 1 = 0
The theorem `PowerSeries.order_one` states that for any type `R` that has a semiring structure and is nontrivial, the order of the formal power series `1` is `0`. In other words, the greatest exponent `n` such that `X^n` divides the power series `1` is `0`.
More concisely: For any semiring type R that is nontrivial, the formal power series 1 in R[['x']] has order 0.
|
PowerSeries.order_X
theorem PowerSeries.order_X : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : Nontrivial R], PowerSeries.X.order = 1
This theorem establishes that the order of the formal power series `X` is `1` in any semiring `R` that is nontrivial. Here, `X` is defined as a specific power series in the ring of formal power series over `R`. The order of a power series is the smallest exponent in its monomial terms. In this case, the power series `X` has its smallest exponent as `1`, hence its order is `1`.
More concisely: The power series `X` over any nontrivial semiring `R` has order 1.
|
PowerSeries.order_monomial
theorem PowerSeries.order_monomial :
∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R) [inst_1 : Decidable (a = 0)],
((PowerSeries.monomial R n) a).order = if a = 0 then ⊤ else ↑n
The theorem `PowerSeries.order_monomial` describes the order of a monomial in a formal power series over a semiring. Specifically, it states that for any semiring `R`, any natural number `n`, and any element `a` of `R`, the order of the monomial `a*X^n` is infinite (`⊤`) if `a` is zero, and is equal to `n` otherwise. The equality is determined in a decidable context for `a = 0`.
More concisely: For any semiring R and natural number n, the order of the monomial a * X^n in a formal power series over R is 0 if a is zero, and is equal to n otherwise.
|
PowerSeries.order_mul
theorem PowerSeries.order_mul :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (φ ψ : PowerSeries R),
(φ * ψ).order = φ.order + ψ.order
This theorem states that for any commutative ring `R` that is also an integral domain, and for any two formal power series `φ` and `ψ` over `R`, the order of the product of `φ` and `ψ` is equal to the sum of their individual orders. In mathematical terms, if we represent the order of a power series as a function `order`, then for the product of two power series, the order of the product is the sum of their orders, i.e., `order(φ * ψ) = order(φ) + order(ψ)`.
More concisely: For any commutative ring `R` that is an integral domain, the order of the product of two formal power series `φ` and `ψ` over `R` is equal to the sum of their individual orders, i.e., `order(φ * ψ) = order(φ) + order(ψ)`.
|
PowerSeries.order.proof_1
theorem PowerSeries.order.proof_1 :
∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R), ¬φ = 0 → ∃ n, (PowerSeries.coeff R n) φ ≠ 0
The theorem `PowerSeries.order.proof_1` states that for any non-zero formal power series `φ` over a semiring `R`, there exists an integer `n` such that the `n`th coefficient of the power series is non-zero. This essentially means that every non-zero power series has a non-zero coefficient at some position.
More concisely: Every non-zero formal power series over a semiring has a non-zero coefficient at some position.
|
PowerSeries.coeff_mul_of_lt_order
theorem PowerSeries.coeff_mul_of_lt_order :
∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R} {n : ℕ},
↑n < ψ.order → (PowerSeries.coeff R n) (φ * ψ) = 0
The theorem `PowerSeries.coeff_mul_of_lt_order` states that for any type `R` with a semiring structure, and for any two power series `φ` and `ψ` over this type, along with a natural number `n`, if `n` is strictly less than the order of `ψ` (where the order of a power series is the smallest `n` such that the `n`th coefficient is nonzero), then the `n`th coefficient of the product of `φ` and `ψ` is zero. In other words, when multiplying two power series, any coefficient of the result that corresponds to an exponent smaller than the order of the second series is zero.
More concisely: For any semiring `R`, if power series `φ` and `ψ` over `R` have orders `m` and `n` respectively with `m < n`, then the `n`th coefficient of their product `φ * ψ` is zero.
|
PowerSeries.order_add_of_order_eq
theorem PowerSeries.order_add_of_order_eq :
∀ {R : Type u_1} [inst : Semiring R] (φ ψ : PowerSeries R), φ.order ≠ ψ.order → (φ + ψ).order = φ.order ⊓ ψ.order
The theorem `PowerSeries.order_add_of_order_eq` states that for any type `R` with a semiring structure and for any two formal power series `φ` and `ψ` over `R`, if the orders of `φ` and `ψ` are not equal, then the order of the sum of these two power series is equal to the minimum of their orders. Here, the term "order of a power series" refers to the smallest exponent in the series with a non-zero coefficient, and "semiring" is a mathematical object similar to a ring but without the requirement of additive inverses.
More concisely: For power series φ and ψ over a semiring R, if the orders of φ and ψ are different, then the order of their sum is equal to the smaller order.
|