Complex.deriv_eq_smul_circleIntegral
theorem Complex.deriv_eq_smul_circleIntegral :
∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] [inst_2 : CompleteSpace F] {R : ℝ} {c : ℂ}
{f : ℂ → F},
0 < R →
DiffContOnCl ℂ f (Metric.ball c R) →
deriv f c = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c) ^ (-2) • f z
This theorem states that if a complex-valued function `f` is differentiable on an open disk of radius `R > 0` centered at `c` and is continuous on the closure of this disk, then the derivative of `f` at `c` can be expressed as an integral over the boundary of this disk. Specifically, the derivative at `c` is equal to the reciprocal of `2 * pi * i` times the line integral of `(z - c)^(-2) * f(z)`, where `z` traces the boundary of the disk. This theorem is a result in complex analysis known as Cauchy's integral formula. Future work includes extending this theorem to the case where the point `w` is inside the disk, and to higher order derivatives.
More concisely: If a complex-valued function `f` is differentiable and continuous on an open disk of radius `R > 0` around `c`, then the derivative of `f` at `c` is equal to `(1 / (2 * pi * i)) * ∫ₕₛ (z - c)^(-2) * f(z) dz`, where the integration is taken over the boundary of the disk.
|
Differentiable.eq_const_of_tendsto_cocompact
theorem Differentiable.eq_const_of_tendsto_cocompact :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : Nontrivial E] {f : E → F},
Differentiable ℂ f → ∀ {c : F}, Filter.Tendsto f (Filter.cocompact E) (nhds c) → f = Function.const E c
This theorem is a corollary of Liouville's theorem and it states that, for any complex differentiable function `f` from a non-trivial normed additive commutative group `E` to another normed additive commutative group `F`, if the function `f` tends to a finite value `c` at infinity (that is, along the filter generated by complements to compact sets in `E`, which in proper spaces coincides with the filter of sets not bounded above), then the function `f` must be a constant function with the value `c`. In other words, if the limit of the function `f` as it approaches infinity (in the sense of `Filter.cocompact`) is `c`, then `f` is the constant function that always returns `c` for any input from `E`.
More concisely: If a complex differentiable function from a non-trivial normed additive commutative group to another such group tends to a finite value at infinity, then it is a constant function.
|
Differentiable.apply_eq_of_tendsto_cocompact
theorem Differentiable.apply_eq_of_tendsto_cocompact :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : Nontrivial E] {f : E → F},
Differentiable ℂ f → ∀ {c : F} (x : E), Filter.Tendsto f (Filter.cocompact E) (nhds c) → f x = c
This theorem is a corollary of Liouville's theorem, stating that if a function `f` from a complex normed additive commutative group `E` to another such group `F` is differentiable everywhere, and if this function tends to a finite value `c` at infinity (more precisely, along the filter `cocompact E`, which in proper spaces is synonymous with being co-bounded), then the function takes the constant value `c` everywhere in `E`. In other words, any such differentiable function that has a limiting value at infinity must be a constant function.
More concisely: If a differentiable function from a complex normed additive commutative group to another such group has a limiting value at infinity, then it is a constant function.
|
Complex.liouville_theorem_aux
theorem Complex.liouville_theorem_aux :
∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {f : ℂ → F},
Differentiable ℂ f → Bornology.IsBounded (Set.range f) → ∀ (z w : ℂ), f z = f w
This Lean theorem `Complex.liouville_theorem_aux` states that for any normed additive commutative group `F` which is also a normed space over the complex numbers `ℂ`, and any function `f` from the complex numbers to `F`, given that `f` is differentiable at any point and the range of `f` is bounded, then for any two complex numbers `z` and `w`, `f(z)` is equal to `f(w)`. This theorem is used as an auxiliary lemma for Liouville's theorem `Differentiable.apply_eq_apply_of_bounded`.
More concisely: If `F` is a normed additive commutative group over the complex numbers that is also a normed space, and `f` is a differentiable function from `ℂ` to `F` with a bounded range, then `f(z) = f(w)` for all `z, w ∈ ℂ`.
|
Differentiable.exists_const_forall_eq_of_bounded
theorem Differentiable.exists_const_forall_eq_of_bounded :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] {f : E → F},
Differentiable ℂ f → Bornology.IsBounded (Set.range f) → ∃ c, ∀ (z : E), f z = c
The theorem is known as Liouville's theorem. It states that, for any function `f` that maps from a complex normed additive commutative group `E` to another complex normed additive commutative group `F`, if `f` is differentiable with respect to complex numbers at all points in `E` and the range of `f` is bounded, then there exists a constant `c` such that for all `z` in `E`, `f(z)` is equal to `c`. In other words, any bounded, complex differentiable function must be constant.
More concisely: Any complex differentiable function mapping between complex normed additive commutative groups with a bounded range is constant.
|
Differentiable.apply_eq_apply_of_bounded
theorem Differentiable.apply_eq_apply_of_bounded :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] {f : E → F},
Differentiable ℂ f → Bornology.IsBounded (Set.range f) → ∀ (z w : E), f z = f w
**Liouville's theorem**: This theorem states that if a function `f` mapping from a space `E` to another space `F`, both spaces being complex normed additive commutative groups, is differentiable at every point, and the range of `f` is bounded, then the function `f` is a constant. In other words, for any two points `z` and `w` in the domain `E`, the value of `f` at `z` equals the value of `f` at `w`.
More concisely: If `f` is a complex differentiable and norm-bounded function from a complex normed additive commutative group to another, then `f` is constant.
|
Differentiable.exists_eq_const_of_bounded
theorem Differentiable.exists_eq_const_of_bounded :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] {f : E → F},
Differentiable ℂ f → Bornology.IsBounded (Set.range f) → ∃ c, f = Function.const E c
**Liouville's theorem**: This theorem states that if a function, mapping from a normed additive commutative group `E` equipped with a complex normed space structure to another similar group `F`, is complex differentiable at every point and its range is bounded (according to the bornology defined on `F`), then the function is essentially a constant function. In other words, there exists some constant `c` in `F` such that for every element in `E`, the function maps it to `c`.
More concisely: If a complex differentiable function from a complex normed space to another, with bounded range, is equal to its derivative at every point, then it is a constant function.
|
Complex.norm_deriv_le_of_forall_mem_sphere_norm_le
theorem Complex.norm_deriv_le_of_forall_mem_sphere_norm_le :
∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {c : ℂ} {R C : ℝ} {f : ℂ → F},
0 < R → DiffContOnCl ℂ f (Metric.ball c R) → (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) → ‖deriv f c‖ ≤ C / R
The theorem `Complex.norm_deriv_le_of_forall_mem_sphere_norm_le` states that if a complex-valued function `f` is differentiable on an open disc of radius `R > 0` with center `c`, and is also continuous on the closure of this disc, and if the norm of its values on the boundary circle of this disc are bounded above by a constant `C`, then the norm of the derivative of `f` at the center `c` is at most `C / R`. In other words, the rate of change of the function at the center is bounded by the ratio of the upper bound of function's values on the boundary and the radius of the disc.
More concisely: If a differentiable and continuous complex-valued function on an open disc is bounded on its boundary, then the norm of its derivative at the center is less than or equal to the supremum of its boundary values divided by the radius of the disc.
|