Stirling.log_stirlingSeq_sub_log_stirlingSeq_succ
theorem Stirling.log_stirlingSeq_sub_log_stirlingSeq_succ :
∀ (n : ℕ), (Stirling.stirlingSeq (n + 1)).log - (Stirling.stirlingSeq (n + 2)).log ≤ 1 / (4 * ↑(n + 1) ^ 2) := by
sorry
This theorem states that for any natural number `n`, the logarithm of the `Stirling.stirlingSeq` sequence at `n+1` minus the logarithm of the same sequence at `n+2` is less than or equal to `1/(4*(n+1)^2)`. In mathematical terms, for each `n` in the natural numbers, we have the inequality `log(stirlingSeq(n+1)) - log(stirlingSeq(n+2)) ≤ 1/(4*(n+1)^2)`.
More concisely: For each natural number `n`, the difference between the logarithms of the `Stirling.stirlingSeq` sequence at `n+1` and `n+2` is bounded above by `1/(4*(n+1)^2)`.
|
Stirling.stirlingSeq_has_pos_limit_a
theorem Stirling.stirlingSeq_has_pos_limit_a : ∃ a, 0 < a ∧ Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds a)
This theorem states that there exists a positive limit `a` for the Stirling sequence, which is defined as `n! / (sqrt(2n) * (n / e)^n)`. This limit is achieved as `n` tends to infinity. In other words, as we take larger and larger values of `n`, the values of the Stirling sequence get arbitrarily close to some positive number `a`.
More concisely: The Stirling sequence `n! / (sqrt(2*n) * (n / e)^n` converges to a positive limit as `n` approaches infinity.
|
Stirling.log_stirlingSeq_diff_hasSum
theorem Stirling.log_stirlingSeq_diff_hasSum :
∀ (m : ℕ),
HasSum (fun k => 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1))
((Stirling.stirlingSeq (m + 1)).log - (Stirling.stirlingSeq (m + 2)).log)
The theorem `Stirling.log_stirlingSeq_diff_hasSum` states that for any natural number `m`, the logarithmic difference between the `(m+1)`-th and `(m+2)`-th terms of the Stirling sequence, `log(stirlingSeq(m + 1)) - log(stirlingSeq(m + 2))`, sums up to a series. The series is given by the sum over all natural numbers `k` of the expression `1 / (2 * (k + 1) + 1) * ((1 / 2 * (m + 1) + 1) ^ 2) ^ (k + 1)`.
More concisely: The logarithmic difference between consecutive terms of the Stirling sequence sums to a series with terms given by `1 / (2 * k + 1) * (1/2 * (m + 1) + 1) ^ (k + 1)` for all natural numbers `m` and `k`.
|
Stirling.tendsto_self_div_two_mul_self_add_one
theorem Stirling.tendsto_self_div_two_mul_self_add_one :
Filter.Tendsto (fun n => ↑n / (2 * ↑n + 1)) Filter.atTop (nhds (1 / 2))
This theorem, named `Stirling.tendsto_self_div_two_mul_self_add_one`, states that the sequence defined by the function `n / (2 * n + 1)` tends towards `1/2` as `n` approaches infinity. In other words, for any neighborhood around `1/2`, there exists a point beyond which all terms of the sequence lie within that neighborhood. This is a statement about the limit behavior of this particular sequence.
More concisely: The sequence defined by `n / (2 * n + 1)` converges to `1/2` as `n` approaches infinity.
|
Stirling.stirlingSeq'_bounded_by_pos_constant
theorem Stirling.stirlingSeq'_bounded_by_pos_constant : ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ Stirling.stirlingSeq (n + 1) := by
sorry
This theorem states that there exists a positive real number 'a' such that 'a' is less than or equal to the value of the function 'stirlingSeq' at every positive integer 'n'. In other words, the sequence defined by 'stirlingSeq', which calculates the value $\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}$, has a positive lower bound.
More concisely: There exists a positive real number $a$ such that $a \leq \frac{n!}{\sqrt{2n}(\frac{n}{e})^n}$ for all positive integers $n$.
|
Stirling.tendsto_stirlingSeq_sqrt_pi
theorem Stirling.tendsto_stirlingSeq_sqrt_pi : Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds Real.pi.sqrt)
**Stirling's Formula**:
This theorem states that the sequence defined by Stirling's formula, `\(\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}\)`, tends to square root of pi (`π`) as `n` approaches infinity. In other words, as `n` gets larger and larger, the value of `\(\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}\)` gets closer and closer to square root of pi. This is a formalization of the well-known Stirling's approximation in mathematics.
More concisely: The limit of `(n! / (sqrt(2 * n) * (n / e)^n)`) as `n` approaches infinity is `sqrt(pi)`.
|
Stirling.second_wallis_limit
theorem Stirling.second_wallis_limit :
∀ (a : ℝ),
a ≠ 0 →
Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds a) →
Filter.Tendsto Real.Wallis.W Filter.atTop (nhds (a ^ 2 / 2))
This theorem, called `Stirling.second_wallis_limit`, states that given a real number `a` which is not equal to zero, if the sequence `stirlingSeq` (which is defined as the factorial of `n` divided by the square root of `2n` times `(n/e)^n`) tends to the number `a` as `n` goes to infinity, then the sequence `Real.Wallis.W` (which is the product of the first `n` terms of Wallis' formula for `π`) tends to `a^2 / 2` as `n` goes to infinity. In other words, if the limit of the Stirling sequence is a non-zero number `a` when `n` approaches infinity, then the limit of the Wallis sequence is `a^2 / 2` when `n` approaches infinity.
More concisely: If the limit of the Stirling sequence `(n! / (sqrt(2 * n) * (n / e)^n) : ℝ)` is a non-zero number `a` as `n` approaches infinity, then the limit of the Wallis sequence `(Real.Wallis.W n)` is equal to `(a ^ 2) / 2` as `n` approaches infinity.
|
Stirling.stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq
theorem Stirling.stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq :
∀ (n : ℕ),
n ≠ 0 → Stirling.stirlingSeq n ^ 4 / Stirling.stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Real.Wallis.W n
The theorem states that for any natural number `n` that is not zero, the square of the ratio of the fourth power of the `n`th term of Stirling's sequence to the square of the `2n`th term of the same sequence, multiplied by the ratio of `n` to `(2n + 1)`, equals the `n`th partial product of Wallis' formula for `π / 2`. In other words, if we denote Stirling's sequence as `S(n)` and the partial product of Wallis' formula as `W(n)`, then we have the identity `(S(n)^4 / S(2n)^2) * (n / (2n + 1)) = W(n)` for all non-zero natural numbers `n`.
More concisely: For any non-zero natural number `n`, the ratio of the fourth power of the `n`th term of Stirling's sequence to the square of the `2n`th term, multiplied by the ratio of `n` to `(2n + 1)`, equals the `n`th partial product of Wallis' formula for `π/2`. In other words, `(S(n)^4 / S(2n)^2 * (n / (2n + 1)) = W(n)` for all `n > 0`.
|
Stirling.stirlingSeq'_antitone
theorem Stirling.stirlingSeq'_antitone : Antitone (Stirling.stirlingSeq ∘ Nat.succ)
The theorem `Stirling.stirlingSeq'_antitone` states that the sequence obtained by applying the function `Stirling.stirlingSeq` to the successor (`Nat.succ`) of natural numbers is monotonically decreasing. In other words, if `a` and `b` are natural numbers and `a ≤ b`, then `Stirling.stirlingSeq (b + 1) ≤ Stirling.stirlingSeq (a + 1)`. In mathematical terms, this sequence is defined as $\frac{(n+1)!}{\sqrt{2(n+1)}((n+1)/e)^{(n+1)}}$ and this sequence decreases as `n` increases.
More concisely: For all natural numbers `a` and `b` with `a <= b`, the Stirling sequence `Stirling.stirlingSeq (a + 1)` is greater than or equal to `Stirling.stirlingSeq (b + 1)`. In other words, the sequence `Stirling.stirlingSeq (Nat.succ n)` decreases as `n` increases.
|
Stirling.log_stirlingSeq'_antitone
theorem Stirling.log_stirlingSeq'_antitone : Antitone (Real.log ∘ Stirling.stirlingSeq ∘ Nat.succ)
This theorem states that the sequence formed by applying the real logarithm function (`Real.log`) to the Stirling Sequence (`Stirling.stirlingSeq`) after incrementing (`Nat.succ`) each natural number is monotone decreasing. In other words, if `n` is less than or equal to `m`, then `log(stirlingSeq(m+1))` is less than or equal to `log(stirlingSeq(n+1))`. Here, `stirlingSeq(n)` is defined as $n!$ divided by the square root of $2n$ times $(n/e)^n$. This sequence is related to Stirling's formula, which states that as `n` approaches infinity, `stirlingSeq(n)` approaches square root of $\pi$. The real logarithm function used here is defined in a particular way to ensure that `log(x * y) = log(x) + log(y)` holds for all nonzero `x` and `y`, and that the derivative of `log` is `1/x` for `x` not equal to zero.
More concisely: The Stirling sequence, defined as the sequence of numbers obtained by applying the real logarithm function to the Stirling numbers and incrementing each natural number, is monotone decreasing.
|
Stirling.log_stirlingSeq_diff_le_geo_sum
theorem Stirling.log_stirlingSeq_diff_le_geo_sum :
∀ (n : ℕ),
(Stirling.stirlingSeq (n + 1)).log - (Stirling.stirlingSeq (n + 2)).log ≤
(1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
This theorem states that for any natural number `n`, the difference between the logarithm of the `n + 1`th element and the `n + 2`th element in the Stirling sequence, `log (stirlingSeq k)`, is less than or equal to the square of the fraction `1 / (2 * (n + 1) + 1)` divided by `1 - (1 / (2 * (n + 1) + 1)) ^ 2`. In other words, it provides an upper bound for the difference between consecutive logarithms in the Stirling sequence.
More concisely: For any natural number `n`, the difference between the logarithms of successive terms in the Stirling sequence, `log (stirlingSeq (S n)) - log (stirlingSeq (S (S n))`, is bounded above by `1 / (2 * (n + 1) + 1) ^ 2`.
|
Stirling.log_stirlingSeq_bounded_aux
theorem Stirling.log_stirlingSeq_bounded_aux :
∃ c, ∀ (n : ℕ), (Stirling.stirlingSeq 1).log - (Stirling.stirlingSeq (n + 1)).log ≤ c
This theorem states that there exists a constant `c` such that for any natural number `n`, the difference of the logarithms of the Stirling sequence at 1 and at `n + 1` is less than or equal to `c`. In other words, the logarithmic difference between subsequent terms of the Stirling sequence is bounded by some constant.
More concisely: There exists a constant `c` such that for all natural numbers `n`, |ln(Stirling n) - ln(Stirling (n+1))| ≤ c.
|
Stirling.factorial_isEquivalent_stirling
theorem Stirling.factorial_isEquivalent_stirling :
Asymptotics.IsEquivalent Filter.atTop (fun n => ↑n.factorial) fun n =>
(2 * ↑n * Real.pi).sqrt * (↑n / Real.exp 1) ^ n
**Stirling's Formula (Asymptotic Equivalent Version)**: This theorem states that the factorial function and a function derived from Stirling's formula are asymptotically equivalent at infinity. Specifically, for any positive integer `n`, the factorial of `n`, `n!`, is asymptotically equivalent to the square root of `2nπ` times `(n/e)^n` as `n` approaches infinity. This comparison is made under the filter `Filter.atTop`, which represents the limit as `n` goes to infinity. Stirling's formula provides an approximation for the factorial function and is widely used in mathematics and computer science.
More concisely: As `n` approaches infinity, `n!` is asymptotically equivalent to `√(2πn) * (n / e)^n` under the filter `Filter.atTop`.
|
Stirling.stirlingSeq'_pos
theorem Stirling.stirlingSeq'_pos : ∀ (n : ℕ), 0 < Stirling.stirlingSeq (n + 1)
This theorem states that for any natural number `n`, the sequence `stirlingSeq`, defined as the factorial of `n` divided by the square root of `2n` times `n` raised to the power of `n` divided by `e`, is always positive when evaluated at `n + 1`. In other words, the expression $\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}$ is always greater than zero for `n > 0`.
More concisely: For all natural numbers `n` greater than zero, the Stirling sequence `(n! / (√(2 * n) * (n / e)^n)` is positive.
|
Stirling.log_stirlingSeq_bounded_by_constant
theorem Stirling.log_stirlingSeq_bounded_by_constant : ∃ c, ∀ (n : ℕ), c ≤ (Stirling.stirlingSeq (n + 1)).log := by
sorry
The theorem states that there exists a constant `c` such that the natural logarithm of the Stirling Sequence, when computed for any natural number `n` (incremented by 1), is always greater than or equal to `c`. In other words, the logarithm of the Stirling Sequence for any `n ≥ 1` is lower bounded by a constant `c`.
More concisely: There exists a constant `c` such that for all natural numbers `n ≥ 1`, the natural logarithm of the Stirling sequence `(stirling n)` is greater than or equal to `c`. In other words, `∃c, ∀n ≥ 1, log (stirling n) ≥ c`.
|