Complex.continuousAt_ofReal_cpow
theorem Complex.continuousAt_ofReal_cpow :
∀ (x : ℝ) (y : ℂ), 0 < y.re ∨ x ≠ 0 → ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)
The theorem `Complex.continuousAt_ofReal_cpow` states that for all real numbers `x` and complex numbers `y`, if the real part of `y` is greater than zero or `x` is not equal to zero, then the function `(x, y) ↦ x ^ y` is continuous at the point `(x, y)`. This function, mapping pairs of a real and a complex number to complex numbers by raising the real number to the power of the complex number, is continuous in the topological space of pairs of real and complex numbers.
More concisely: For real numbers x ≠ 0 and complex numbers y with Re(y) > 0, the function (x, y) ↦ x^y is continuous at (x, y) in the complex plane.
|
continuousAt_cpow
theorem continuousAt_cpow : ∀ {p : ℂ × ℂ}, p.1 ∈ Complex.slitPlane → ContinuousAt (fun x => x.1 ^ x.2) p
The theorem `continuousAt_cpow` states that the function `z ^ w` where `z` and `w` are complex numbers (`ℂ`) is continuous at a point `p`, which is a pair of complex numbers, provided that the first component of `p` (i.e., `p.1` or `z`) does not belong to the interval `(-∞, 0]` on the real line. In other words, `z` must not be lying on the negative real axis or be zero. This condition is captured by the requirement that `p.1` must be in the "slit plane", which is the complex plane with the closed negative real axis removed. Note that there is also another version of this theorem `Complex.continuousAt_cpow_zero_of_re_pos` that allows `z` to be zero but under the additional assumption that the real part of `w` is strictly positive.
More concisely: The function `z ^ w` is continuous at the complex number `p = (z, w)` if `z` is not in the closed negative half-plane.
|
Real.continuousAt_rpow
theorem Real.continuousAt_rpow : ∀ (p : ℝ × ℝ), p.1 ≠ 0 ∨ 0 < p.2 → ContinuousAt (fun p => p.1 ^ p.2) p
The theorem states that for any pair of real numbers `(p : ℝ × ℝ)`, as long as either the first element of the pair is not equal to zero or the second element of the pair is greater than zero, the function which raises the first element of the pair to the power of the second element, i.e., `(fun p => p.1 ^ p.2)`, is continuous at the point `p`. In mathematical terms, it means that as we approach the point `p`, the value of the function `(fun p => p.1 ^ p.2)` approaches the value at the point `p`.
More concisely: For any real numbers `p`, if `p.1 ≠ 0` or `p.2 > 0`, then the function `x ↦ x.1 ^ x.2` is continuous at `x = p`.
|
Complex.continuousAt_cpow_zero_of_re_pos
theorem Complex.continuousAt_cpow_zero_of_re_pos : ∀ {z : ℂ}, 0 < z.re → ContinuousAt (fun x => x.1 ^ x.2) (0, z) := by
sorry
This theorem, named `Complex.continuousAt_cpow_zero_of_re_pos`, states that for any complex number `z` with a positive real part, the function `x.1 ^ x.2` is continuous at the point `(0, z)`. In other words, for any complex number whose real part is greater than zero, as you get closer and closer to the point `(0, z)` in the complex plane, the values of the function `x.1 ^ x.2` also get arbitrarily close to the value of the function at `(0, z)`. Here, continuity is defined in the topological sense, i.e., the function's output values get arbitrarily close to a limit value as the input values get arbitrarily close to a certain point.
More concisely: For any complex number `z` with a positive real part, the function `x ⟩ 0 => x.1 ^ x.2` is continuous at `(0, z)`.
|
Complex.continuousAt_cpow_of_re_pos
theorem Complex.continuousAt_cpow_of_re_pos :
∀ {p : ℂ × ℂ}, 0 ≤ p.1.re ∨ p.1.im ≠ 0 → 0 < p.2.re → ContinuousAt (fun x => x.1 ^ x.2) p
The theorem `Complex.continuousAt_cpow_of_re_pos` states that for any pair of complex numbers `p`, if the real part of the first complex number of `p` is nonnegative or its imaginary part is nonzero, and the real part of the second complex number of `p` is positive, then the function which maps `x` to the power of its first component raised to the second component, i.e., `x.1 ^ x.2`, is continuous at `p`. In other words, as we approach `p` in the complex plane, `x.1 ^ x.2` approaches `(p.1 ^ p.2)`, where `(x.1, x.2)` denotes a complex number in the plane.
More concisely: If the real part of the first complex number is non-negative or its imaginary part is non-zero, and the real part of the second complex number is positive, then the function `x ↦ x.1 ^ x.2` is continuous at `p`.
|
Filter.Tendsto.rpow
theorem Filter.Tendsto.rpow :
∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ} {x y : ℝ},
Filter.Tendsto f l (nhds x) →
Filter.Tendsto g l (nhds y) → x ≠ 0 ∨ 0 < y → Filter.Tendsto (fun t => f t ^ g t) l (nhds (x ^ y))
The theorem `Filter.Tendsto.rpow` states that for any type `α` and a filter `l` on it, along with two functions `f` and `g` from `α` to real numbers `ℝ`, and two real numbers `x` and `y`; if `f` tends to `x` according to the filter `l` and `g` tends to `y` according to the same filter, and if either `x` is not zero or `y` is positive, then the function that maps any element `t` of `α` to the real number `f(t) ^ g(t)` will also tend to `x ^ y` according to the filter `l`.
In simpler terms, this theorem deals with the limit of a function that raises one function (`f`) to the power of another function (`g`). If the individual functions `f` and `g` converge to `x` and `y` respectively, then under some conditions on `x` and `y`, the combined function will converge to `x ^ y`.
More concisely: If filters `l` on `α` make functions `f : α → ℝ` and `g : α → ℝ` tend to limit values `x` and `y` respectively, and `x` is nonzero or `y` is positive, then the function `t ↦ f(t) ^ g(t)` tends to the limit `x ^ y` according to `l`.
|
Complex.continuousAt_cpow_const_of_re_pos
theorem Complex.continuousAt_cpow_const_of_re_pos :
∀ {z w : ℂ}, 0 ≤ z.re ∨ z.im ≠ 0 → 0 < w.re → ContinuousAt (fun x => x ^ w) z
The theorem `Complex.continuousAt_cpow_const_of_re_pos` states that for any two complex numbers `z` and `w`, if the real part of `z` is non-negative or the imaginary part is non-zero, and the real part of `w` is positive, then the function that raises `x` to the power of `w` is continuous at point `z`. This theorem is a special case of `continuousAt_cpow_const` where `z` is not equal to `0`.
More concisely: For complex numbers `z` with non-negative real part or non-zero imaginary part, and positive real part `w`, the function `x => x ^ w` is continuous at `z`.
|
continuousAt_const_cpow
theorem continuousAt_const_cpow : ∀ {a b : ℂ}, a ≠ 0 → ContinuousAt (fun x => a ^ x) b
The theorem `continuousAt_const_cpow` states that for any two complex numbers `a` and `b`, given that `a` is not equal to zero, the function that takes `x` to `a ^ x` (i.e., raises `a` to the power `x`) is continuous at `b`. In mathematical terms, this means that as `x` approaches `b`, `a ^ x` tends to `a ^ b`.
More concisely: For complex numbers `a ≠ 0` and `b`, the function `x ↦ a ^ x` is continuous at `b`.
|
Complex.continuousAt_ofReal_cpow_const
theorem Complex.continuousAt_ofReal_cpow_const :
∀ (x : ℝ) (y : ℂ), 0 < y.re ∨ x ≠ 0 → ContinuousAt (fun a => ↑a ^ y) x
The theorem `Complex.continuousAt_ofReal_cpow_const` states that for any real number `x` and any complex number `y`, if the real part of `y` is greater than zero or `x` is not equal to zero, then the function that maps a real number `a` to its complex power `y`, denoted as `a ^ y`, is continuous at `x`. In mathematical terms, this means the limit as `a` approaches `x` of `a ^ y` equals `x ^ y`.
More concisely: For real numbers `x` neither zero nor equal to the real part of complex number `y`, the complex power function `a => a ^ y` is continuous at `x`.
|