hasDerivAt_ofReal_cpow
theorem hasDerivAt_ofReal_cpow :
∀ {x : ℝ}, x ≠ 0 → ∀ {r : ℂ}, r ≠ -1 → HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
The theorem `hasDerivAt_ofReal_cpow` states that even though the function `fun x => x ^ r` for a fixed complex number `r` is not complex-differentiable along the negative real line, it is still real-differentiable. Furthermore, the derivative of the function is as one would expect. In specific, for any real number `x` that is not equal to zero and any complex number `r` that is not equal to `-1`, the derivative at `x` of the function `fun y => ↑y ^ (r + 1) / (r + 1)` is `↑x ^ r`. Here `↑` denotes the coercion from real numbers to complex numbers.
More concisely: For any real number `x ≠ 0` and complex number `r ≠ -1`, the real-differentiable function `x ↦ x^r` has derivative `x^(r+1) / (r+1)` at `x`.
|
tendsto_one_plus_div_pow_exp
theorem tendsto_one_plus_div_pow_exp :
∀ (t : ℝ), Filter.Tendsto (fun x => (1 + t / ↑x) ^ x) Filter.atTop (nhds t.exp)
The theorem `tendsto_one_plus_div_pow_exp` states that for any real number `t`, the function `(1 + t/x) ^ x`, where `x` is a natural number, tends to the exponential of `t` as `x` approaches positive infinity. In mathematical notation, this theorem could be written as: for all `t` in the set of real numbers, the limit as `x` approaches positive infinity of `(1 + t/x) ^ x` is `e^t`, where `e` is the base of the natural logarithm.
More concisely: For any real number `t`, as `x` approaches positive infinity, `(1 + t/x) ^ x` converges to `e^t`.
|
Real.deriv_rpow_const
theorem Real.deriv_rpow_const : ∀ {x p : ℝ}, x ≠ 0 ∨ 1 ≤ p → deriv (fun x => x ^ p) x = p * x ^ (p - 1)
This theorem states that for all real numbers `x` and `p`, if `x` is not zero or `p` is greater than or equal to one, then the derivative of the function `f(x) = x^p` at the point `x` is `p * x^(p - 1)`. This is a special case of the power rule in calculus, which gives the derivative of powers of `x`.
More concisely: For real numbers `x` and `p` with `x ≠ 0` and `p ≥ 1`, the derivative of `f(x) = x^p` is `p * x^(p - 1)`.
|
Real.hasStrictDerivAt_const_rpow_of_neg
theorem Real.hasStrictDerivAt_const_rpow_of_neg :
∀ {a x : ℝ},
a < 0 → HasStrictDerivAt (fun x => a ^ x) (a ^ x * a.log - (a.log * x).exp * (x * Real.pi).sin * Real.pi) x
This theorem states that the function `f(x) = a^x` is strictly differentiable at any real number `x` for all negative real numbers `a`. Here, strict differentiability means that the difference between the function values at two points `y` and `z` can be expressed as `(y - z) * f'(x) + o(y - z)` as `y` and `z` approach `x`. The derivative of this function at a point `x` is given by `a^x * log(a) - exp(log(a) * x) * sin(x * π) * π`. Note that these values of `a` are outside of the "official" domain of `a^x`, and `a^x` could be redefined for negative `a` if some other definition will be more convenient.
More concisely: For all negative real numbers `a`, the function `f(x) = a^x` is strictly differentiable at `x`, with derivative `a^x * log(a) - exp(log(a) * x) * sin(x * π) * π`.
|
tendsto_one_plus_div_rpow_exp
theorem tendsto_one_plus_div_rpow_exp :
∀ (t : ℝ), Filter.Tendsto (fun x => (1 + t / x) ^ x) Filter.atTop (nhds t.exp)
The theorem `tendsto_one_plus_div_rpow_exp` states that, for all real numbers `t`, the function `(1 + t/x) ^ x` tends to the exponential of `t` as `x` tends to positive infinity. In other words, as `x` increases without bound, the value of the expression `(1 + t/x) ^ x` gets arbitrarily close to the value of `exp(t)`, where `exp(t)` is the exponential function. This theorem is a formalization in Lean 4 of a well-known result in calculus and analysis concerning the limit of a function.
More concisely: As x approaches infinity, (1 + t/x)^x converges to e^t.
|
Real.hasStrictFDerivAt_rpow_of_pos
theorem Real.hasStrictFDerivAt_rpow_of_pos :
∀ (p : ℝ × ℝ),
0 < p.1 →
HasStrictFDerivAt (fun x => x.1 ^ x.2)
((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
(p.1 ^ p.2 * p.1.log) • ContinuousLinearMap.snd ℝ ℝ ℝ)
p
The theorem `Real.hasStrictFDerivAt_rpow_of_pos` states that, given a pair of real numbers `p`, if the first element of the pair is positive, then the function `(x, y) ↦ x ^ y`, which maps a pair of real numbers to the first element raised to the power of the second element, has a strict derivative at `p`. The derivative is given by `((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * Real.log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ)`. Here, `•` denotes scalar multiplication, `ContinuousLinearMap.fst ℝ ℝ ℝ` and `ContinuousLinearMap.snd ℝ ℝ ℝ` are the continuous linear functions that map a pair of real numbers to its first and second elements respectively, and `Real.log` is the real logarithm function.
More concisely: If `p` is a positive real number, then the function `x ^ y` has a strict derivative `p.2 * p.1 ^ (p.2 - 1) * x + p.1 ^ p.2 * log(p.1) * y` at `(p, _)`.
|
Real.differentiableAt_rpow_const_of_ne
theorem Real.differentiableAt_rpow_const_of_ne : ∀ (p : ℝ) {x : ℝ}, x ≠ 0 → DifferentiableAt ℝ (fun x => x ^ p) x := by
sorry
The theorem `Real.differentiableAt_rpow_const_of_ne` states that for any real number `p` and any real number `x` not equal to zero, the function `f(x) = x^p` (x raised to the power p) is differentiable at `x`. This means that there exists a derivative of the function `f` at the point `x`.
More concisely: For any real number `p` and non-zero `x`, the function `x => x^p` is differentiable at `x`.
|
Complex.hasStrictDerivAt_const_cpow
theorem Complex.hasStrictDerivAt_const_cpow :
∀ {x y : ℂ}, x ≠ 0 ∨ y ≠ 0 → HasStrictDerivAt (fun y => x ^ y) (x ^ y * x.log) y
This theorem states that for any complex numbers `x` and `y`, where either `x` or `y` is non-zero, the function `f(y) = x^y` is strictly differentiable at the point `y`. The derivative of this function at `y` is `x^y * Complex.log x`, where `Complex.log x` denotes the complex logarithm of `x`. In other words, the change in `x^y` with respect to `y` at any point `y` is described by the function `x^y * Complex.log x`, given that either `x` or `y` is not zero.
More concisely: For complex numbers `x` and `y` with `x` or `y` non-zero, the function `f(y) = x^y` is strictly differentiable with derivative `x^y * log(x)`, where `log(x)` denotes the complex logarithm of `x`.
|
Real.hasStrictDerivAt_const_rpow
theorem Real.hasStrictDerivAt_const_rpow :
∀ {a : ℝ}, 0 < a → ∀ (x : ℝ), HasStrictDerivAt (fun x => a ^ x) (a ^ x * a.log) x
This theorem states that for any real number `a` greater than `0`, and for any real number `x`, the function `f(x) = a^x` has a strict derivative at the point `x`. The derivative is given by the expression `a^x * Real.log a`. In mathematical notation, this would be written as `f'(x) = a^x * log(a)`. This means that the rate of change of the function `a^x` at any point `x` is `a^x` times the natural logarithm of `a`.
More concisely: For any real number `a > 0`, the function `f(x) = a^x` has a strict derivative at `x`, given by `f'(x) = a^x * log(a)`.
|
Real.contDiffAt_rpow_of_ne
theorem Real.contDiffAt_rpow_of_ne : ∀ (p : ℝ × ℝ), p.1 ≠ 0 → ∀ {n : ℕ∞}, ContDiffAt ℝ n (fun p => p.1 ^ p.2) p := by
sorry
The theorem `Real.contDiffAt_rpow_of_ne` states that for any pair of real numbers `(x, y)`, the function `f(x, y) = x ^ y` is infinitely continuously differentiable at the point `(x, y)`, provided that `x` is not equal to zero. This holds for any value of `n`, where `n` is a countably infinite integer (ℕ∞).
More concisely: For any `x ≠ 0` in ℝ and any `y` in ℝ, the function `x ^ y` is infinitely differentiable as a function of `x` at the point `(x, y)`.
|
Complex.hasStrictDerivAt_cpow_const
theorem Complex.hasStrictDerivAt_cpow_const :
∀ {x c : ℂ}, x ∈ Complex.slitPlane → HasStrictDerivAt (fun z => z ^ c) (c * x ^ (c - 1)) x
This theorem states that for any complex numbers `x` and `c`, with `x` belonging to the slit plane (the complex plane with the closed negative real axis removed), the function `f(z) = z ^ c` has a strict derivative at the point `x`. The derivative at this point is `c * x ^ (c - 1)`. In other words, the power function with a constant exponent has a strict derivative in the slit complex plane, and the derivative is computed using the standard power rule from calculus.
More concisely: For complex numbers `x` in the slit complex plane and constant `c`, the function `f(z) = z ^ c` has a strict derivative `deriv f x = c * x ^ (c - 1)`.
|
Real.hasDerivAt_rpow_const
theorem Real.hasDerivAt_rpow_const : ∀ {x p : ℝ}, x ≠ 0 ∨ 1 ≤ p → HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x := by
sorry
The theorem `Real.hasDerivAt_rpow_const` states that for any real numbers `x` and `p`, if `x` is not equal to 0 or `p` is greater than or equal to 1, then the function `f(x) = x^p` has the derivative `f'(x) = p * x^(p - 1)` at the point `x`. In other words, the derivative of the power function `x^p` at any point `x` that is not zero, or where `p` is at least 1, is given by the formula `p * x^(p - 1)`.
More concisely: If `x ≠ 0` and `p ≥ 1`, then the derivative of `x^p` at `x` is `p * x^(p - 1)`.
|
Real.hasStrictFDerivAt_rpow_of_neg
theorem Real.hasStrictFDerivAt_rpow_of_neg :
∀ (p : ℝ × ℝ),
p.1 < 0 →
HasStrictFDerivAt (fun x => x.1 ^ x.2)
((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
(p.1 ^ p.2 * p.1.log - (p.1.log * p.2).exp * (p.2 * Real.pi).sin * Real.pi) • ContinuousLinearMap.snd ℝ ℝ ℝ)
p
The theorem `Real.hasStrictFDerivAt_rpow_of_neg` states that the function mapping a pair of real numbers `(x, y)` to `x ^ y` is strictly differentiable at any point `p : ℝ × ℝ` where the first component `p.1` is negative. The derivative at such a point `p` is given by `(p.2 * p.1 ^ (p.2 - 1))` times the continuous linear map projecting onto the first component plus `(p.1 ^ p.2 * log(p.1) - exp(log(p.1) * p.2) * sin(p.2 * π) * π)` times the continuous linear map projecting onto the second component.
More concisely: The function `x => x ^ y` is strictly differentiable at `(x, y)` with `x < 0`, having derivative `(y * x ^ (y - 1)) * ∂x + (x ^ y * log x - exp(y * log x) * π * sin(y * π)) * ∂y`, where `∂x` and `∂y` denote the partial derivatives with respect to the first and second components, respectively.
|