HasDerivAt.comp_ofReal
theorem HasDerivAt.comp_ofReal : ∀ {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}, HasDerivAt e e' ↑z → HasDerivAt (fun y => e ↑y) e' z
This theorem states that if a complex function `e` is differentiable at a real point, then its restriction to the real numbers is also differentiable at that point as a function from the reals to the complex numbers, and importantly, it has the same derivative. In mathematical terms, given a complex function `e` with derivative `e'` at a certain real point `z`, if `e` has a derivative `e'` at the complexified `z`, then the function `e` also has a derivative `e'` at `z` when it's restricted to the real numbers.
More concisely: If a complex function `e` is complex differentiable at a real point `z`, then `e` has a real differentiable restriction to the reals at `z` with the same real derivative.
|
HasDerivAt.real_of_complex
theorem HasDerivAt.real_of_complex :
∀ {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}, HasDerivAt e e' ↑z → HasDerivAt (fun x => (e ↑x).re) e'.re z
This theorem states that if a complex-valued function `e` has a derivative at a real number `z`, then the function that takes a real number to the real part of `e` at that number is also differentiable at `z`. Furthermore, the derivative of this real function at `z` is the real part of the derivative of `e` at `z`.
More concisely: If `e` is a complex-valued function with a complex derivative at a real number `z`, then the real-valued function `Re(e)` is differentiable at `z` and its derivative is equal to the real part of `e'(z)`.
|
conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj
theorem conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj :
∀ {f : ℂ → ℂ} {z : ℂ},
ConformalAt f z ↔
(DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
The theorem `conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj` states that a complex function `f` is conformal at a point `z` if and only if the function is either holomorphic at `z` (i.e., the function `f` is differentiable at `z` in the complex plane), or it is antiholomorphic at the conjugate of `z` (i.e., the function `f` composed with the conjugate function is differentiable at the conjugate of `z`), and additionally, the real derivative of the function `f` at `z` is not zero. In other words, a map between complex numbers preserves angles if and only if it is either a complex-differentiable map or a complex conjugation composed with a complex-differentiable map, and its derivative is nonzero.
More concisely: A complex function is conformal at a point if and only if it is complex-differentiable there or complex-differentiable at the conjugate point with non-zero real derivative.
|
HasStrictDerivAt.real_of_complex
theorem HasStrictDerivAt.real_of_complex :
∀ {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}, HasStrictDerivAt e e' ↑z → HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
The theorem `HasStrictDerivAt.real_of_complex` states that if a function from complex numbers to complex numbers (denoted as `e`) is strictly differentiable at a point `z` that is a real number, then the real function induced by `e` (obtained by taking the real part of the output of `e`) is also strictly differentiable at the same point `z`. Furthermore, the derivative of the induced real function at the point `z` is equal to the real part of the derivative of the complex function `e` at that point. In mathematical terms, if we have that `e` has a strict derivative `e'` at `z` (expressed as `HasStrictDerivAt e e' ↑z`), then `(fun x => (e ↑x).re)` has a strict derivative `e'.re` at `z` (expressed as `HasStrictDerivAt (fun x => (e ↑x).re) e'.re z`).
More concisely: If a complex function `e` is strictly differentiable at a real number `z`, then the real function induced by `e` is also strictly differentiable at `z` and their derivatives are equal, i.e., `HasStrictDerivAt e e' ↑z` implies `HasStrictDerivAt (fun x => (e ↑x).re) (e'.re) z`.
|
DifferentiableAt.conformalAt
theorem DifferentiableAt.conformalAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {z : ℂ} {f : ℂ → E},
DifferentiableAt ℂ f z → deriv f z ≠ 0 → ConformalAt f z
This theorem states that for a function `f` which maps the complex plane to a complex normed space `E`, if `f` is differentiable at a point `z` (in the sense that it admits a derivative at that point) and the derivative of `f` at `z` is non-zero, then `f` is conformal at `z`. Here, being conformal implies that `f` has a derivative at point `z` that preserves angles. This is a version of the Cauchy-Riemann equations, which are a fundamental tool in complex analysis.
More concisely: If a complex function `f` has a non-zero complex derivative at a point `z`, then `f` is conformal (preserves angles) at `z`.
|
HasDerivAt.ofReal_comp
theorem HasDerivAt.ofReal_comp :
∀ {z : ℝ} {f : ℝ → ℝ} {u : ℝ}, HasDerivAt f u z → HasDerivAt (fun y => ↑(f y)) (↑u) z
This theorem states that if a function `f : ℝ → ℝ` is differentiable at a real point `x`, then it retains its differentiability when considered as a function `ℝ → ℂ`, mapping real numbers to complex numbers. Specifically, if `f` has a derivative `u` at a point `z` in the real number domain, then the complex-valued version of `f` also has a derivative at that same point `z`, where the derivative is the complex number equivalent of `u`.
More concisely: If a real-valued function `f : ℝ → ℝ` is differentiable at a point `x ∈ ℝ`, then the complex-valued extension `f : ℝ → ℂ` is differentiable at `x` with derivative `u : ℂ` such that `u` is the complex number equivalent of `f'(x)`.
|
ContDiff.real_of_complex
theorem ContDiff.real_of_complex : ∀ {e : ℂ → ℂ} {n : ℕ∞}, ContDiff ℂ n e → ContDiff ℝ n fun x => (e ↑x).re
This theorem states that for every function `e` from complex numbers to complex numbers, and for any natural number `n` (which could be the special value `ℕ∞` representing infinity), if `e` is `n`-times continuously differentiable (meaning we can take the derivative of `e` `n` times and the result is still a continuous function), then the function that takes a real number `x`, converts it to a complex number `↑x`, applies `e`, and then takes the real part `.re`, is also `n`-times continuously differentiable over the real numbers.
More concisely: If a complex function `e` is `n`-times differentiable, then the real-part function `x ↔>.re<. (↑x ↔> e ↔>.re)` is also `n`-times differentiable over the real numbers.
|