LiouvilleNumber.remainder_lt
theorem LiouvilleNumber.remainder_lt :
∀ (n : ℕ) {m : ℝ}, 2 ≤ m → LiouvilleNumber.remainder m n < 1 / (m ^ n.factorial) ^ n
This theorem provides an upper bound on the remainder of a Liouville number series. It states that for any natural number `n` and any real number `m` such that `m` is greater than or equal to 2, the remainder of the Liouville number series for `m` starting from `n+1` (represented as `LiouvilleNumber.remainder m n`) is less than `1 / (m ^ n.factorial) ^ n`. This bound is weaker than that provided by the `LiouvilleNumber.remainder_lt'` theorem, but is more useful for certain proofs.
More concisely: For any natural number `n` and real number `m` >= 2, the remainder of the Liouville number series for `m` starting from `n+1` is less than `1 / (m ^ (n+1))!`.
|
LiouvilleNumber.remainder_lt'
theorem LiouvilleNumber.remainder_lt' :
∀ (n : ℕ) {m : ℝ}, 1 < m → LiouvilleNumber.remainder m n < (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1).factorial)
This theorem provides an upper estimate for the remainder of a Liouville number series. Specifically, it states that for any natural number `n` and any real number `m` such that `m` is larger than 1, the remainder of the series for the Liouville number `m` starting from `n+1` is less than the reciprocal of `(1 - 1/m)` multiplied by `1` divided by `m` to the power of the factorial of `n+1`. This estimate is stronger than the one provided by the theorem `LiouvilleNumber.remainder_lt`, however, the latter estimate is more useful for the proof.
More concisely: For any natural number `n` and Liouville number `m > 1`, the remainder of the Liouville series for `m` starting from `n+1` is strictly less than `1 / (m * (m-1)!)^(n+1)`.
|
LiouvilleNumber.partialSum_eq_rat
theorem LiouvilleNumber.partialSum_eq_rat :
∀ {m : ℕ}, 0 < m → ∀ (k : ℕ), ∃ p, LiouvilleNumber.partialSum (↑m) k = ↑p / ↑(m ^ k.factorial)
The theorem states that for any natural number `m` greater than zero and any natural number `k`, there exists a natural number `p` such that the sum of the first `k` terms of the Liouville number with base `m` is equal to the ratio `p` over `m` raised to the power of `k` factorial. In mathematical terms, if you calculate the sum of the series $\sum_{i=0}^k\frac{1}{m^{i!}}$, you will obtain a number `p` in a way that this sum equals $\frac{p}{m^{k!}}$.
More concisely: For any natural numbers `m` greater than 1 and `k`, there exists a natural number `p` such that $\sum_{i=0}^k\frac{1}{m^{i!}} = \frac{p}{m^{k!}}$.
|
LiouvilleNumber.partialSum_add_remainder
theorem LiouvilleNumber.partialSum_add_remainder :
∀ {m : ℝ}, 1 < m → ∀ (k : ℕ), LiouvilleNumber.partialSum m k + LiouvilleNumber.remainder m k = liouvilleNumber m
This theorem states that for any given real number `m` that is greater than 1 and any natural number `k`, the sum of the first `k+1` terms of Liouville's constant and the sum of the remaining terms starting from `k+1` of Liouville's constant is equal to the total sum of terms of Liouville's constant. In mathematical terms, it says that for `1 < m`, we have
$$
\sum_{i=0}^k\frac{1}{m^{i!}} + \sum_{i=k+1}^\infty\frac{1}{m^{i!}} = \sum_{i=0}^\infty\frac{1}{m^{i!}}.
$$
This is essentially splitting the sum defining a Liouville number into the first `k` terms and the rest.
More concisely: For any real number `m > 1`, the sum of the first `k+1` terms and the remaining terms of the infinite series $\sum\_{i=0}^\infty \frac{1}{m^{i!}}$ are equal: $\sum\_{i=0}^k \frac{1}{m^{i!}} + \sum\_{i=k+1}^\infty \frac{1}{m^{i!}} = \sum\_{i=0}^\infty \frac{1}{m^{i!}}$.
|