Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
theorem Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt :
โ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] [inst_2 : CompleteSpace E] {f : โ โ E}
{c : โ}, (โแถ (z : โ) in nhdsWithin c {c}แถ, DifferentiableAt โ f z) โ ContinuousAt f c โ AnalyticAt โ f c
This theorem, known as the weak version of the **Removable Singularity** theorem, states that for a complex function `f` from the complex numbers to a normed additive commutative group `E` (which also forms a complex normed space and is complete), if `f` is differentiable in the punctured neighborhood of a point 'c' (that is, the neighborhood of 'c', excluding 'c' itself), and is also continuous at this point 'c', then `f` is analytic at this point 'c'. In other words, `f` admits a power series expansion around 'c'.
More concisely: If a complex function `f` is differentiable and continuous at a point `c`, then `f` is analytic at `c`.
|
Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under
theorem Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under :
โ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] [inst_2 : CompleteSpace E] {f : โ โ E}
{c : โ},
(โแถ (z : โ) in nhdsWithin c {c}แถ, DifferentiableAt โ f z) โ
(Filter.IsBoundedUnder (fun x x_1 => x โค x_1) (nhdsWithin c {c}แถ) fun z => โf z - f cโ) โ
Filter.Tendsto f (nhdsWithin c {c}แถ) (nhds (limUnder (nhdsWithin c {c}แถ) f))
The **Removable singularity** theorem states that for a given function `f : โ โ E`, where `โ` is the set of complex numbers and `E` is a normed additive commutative group with a normed space over complex numbers and complete space, if this function is complex differentiable and bounded on a punctured neighborhood of a complex number `c`, then the function `f` has a limit at `c`. Specifically, all values `z` that are differentiable at `โ` in the punctured neighborhood of `c` are bounded under the norm โf z - f cโ. The theorem asserts the limit of the function `f` as `z` approaches `c` (excluding `c`) exists and can be found using `limUnder`.
More concisely: If a complex differentiable and bounded function `f` on a punctured neighborhood of a complex number `c` in a normed additive commutative group with a normed space over complex numbers and complete space has all its derivatives at `z โ c` bounded under the norm, then `f` has a limit at `c`.
|
Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO
theorem Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO :
โ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] [inst_2 : CompleteSpace E] {f : โ โ E}
{c : โ},
(โแถ (z : โ) in nhdsWithin c {c}แถ, DifferentiableAt โ f z) โ
((fun z => f z - f c) =o[nhdsWithin c {c}แถ] fun z => (z - c)โปยน) โ
Filter.Tendsto f (nhdsWithin c {c}แถ) (nhds (limUnder (nhdsWithin c {c}แถ) f))
This is the **Removable Singularity** theorem. It states that for a function `f` mapping from the complex numbers to a complete normed space `E`, if `f` is complex differentiable on a neighborhood of a complex number `c` excluding `c` itself, and if the difference between `f(z)` and `f(c)` is little-o of `(z - c)^-1` as `z` approaches `c`, then `f` has a limit at `c`. In other words, the function `f` approaches a certain value when `z` approaches `c`, despite `f` not being defined at `c`. This is a key concept in complex analysis, where such a point `c` is called a removable singularity of the function `f`.
More concisely: If a complex differentiable function `f` at a complex number `c` has `f(z) - f(c)` be little-o of `(z - c)^-1`, then `f` has a limit at `c`.
|
Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable
theorem Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable :
โ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] [inst_2 : CompleteSpace E] {U : Set โ},
IsOpen U โ
โ {c wโ : โ} {R : โ} {f : โ โ E},
Metric.closedBall c R โ U โ
DifferentiableOn โ f U โ
wโ โ Metric.ball c R โ
((2 * โReal.pi * Complex.I)โปยน โข โฎ (z : โ) in C(c, R), ((z - wโ) ^ 2)โปยน โข f z) = deriv f wโ
This theorem is known as the Cauchy formula for the derivative of a holomorphic function. It states that for any normed additive commutative group `E`, any normed space over `โ` with `E` as base, and any complete space `E`, given an open set `U` in the complex plane, complex numbers `c` and `wโ`, a real number `R`, and a function `f` from complex numbers to `E`, if the closed ball centered at `c` with radius `R` is a subset of `U` and `f` is differentiable on `U` and `wโ` is in the open ball centered at `c` with radius `R`, then the integral of `f z` divided by `(z - wโ)ยฒ` around the circle centered at `c` with radius `R`, scaled by the multiplicative inverse of `2ฯi`, equals the derivative of `f` at `wโ`. This is a crucial property of holomorphic functions and serves as the foundation for many results in complex analysis.
More concisely: For a holomorphic function `f` on an open set `U` in the complex plane, if `c` is a point in `U`, `R` is the radius of a disk containing `c` that is contained in `U`, and `wโ` is a point in the disk, then the derivative of `f` at `wโ` equals the value of the integral of `f(z)` times `(z - wโ)โปยน` over the circle of radius `R` around `c`, multiplied by `iฯโปยน`.
|
Complex.differentiableOn_update_limUnder_of_isLittleO
theorem Complex.differentiableOn_update_limUnder_of_isLittleO :
โ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] [inst_2 : CompleteSpace E] {f : โ โ E}
{s : Set โ} {c : โ},
s โ nhds c โ
DifferentiableOn โ f (s \ {c}) โ
((fun z => f z - f c) =o[nhdsWithin c {c}แถ] fun z => (z - c)โปยน) โ
DifferentiableOn โ (Function.update f c (limUnder (nhdsWithin c {c}แถ) f)) s
The theorem is known as the **Removable Singularity** theorem. It states that if `s` is a neighborhood of a complex number `c`, and if a function `f` mapping complex numbers to a complete normed additive group `E` is complex differentiable on `s` excluding `c`, and furthermore if the difference between `f(z)` and `f(c)` is much smaller than the reciprocal of `(z-c)` as `z` approaches `c` (formally, `(f z - f c) = o((z - c)โปยน)` as `z` tends to `c`), then `f` can be redefined at `c` to be the limit of `f` as `z` approaches `c` but is not equal to `c` (formally, `limUnder (nhdsWithin c {c}แถ) f`), and this redefined function is still complex differentiable on `s`.
More concisely: If a complex differentiable function `f` on a neighborhood `s` of a complex number `c`, with `f(z)` approaching `f(c)` faster than `1/(z-c)` as `z` approaches `c`, then `f` can be redefined at `c` as the limit of `f` and this new definition remains complex differentiable.
|
Complex.differentiableOn_update_limUnder_insert_of_isLittleO
theorem Complex.differentiableOn_update_limUnder_insert_of_isLittleO :
โ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] [inst_2 : CompleteSpace E] {f : โ โ E}
{s : Set โ} {c : โ},
s โ nhdsWithin c {c}แถ โ
DifferentiableOn โ f s โ
((fun z => f z - f c) =o[nhdsWithin c {c}แถ] fun z => (z - c)โปยน) โ
DifferentiableOn โ (Function.update f c (limUnder (nhdsWithin c {c}แถ) f)) (insert c s)
This theorem is known as the Removable Singularity theorem. It states that given a punctured neighborhood `s` of a complex number `c` and a function `f` from complex numbers to some normed additive commutative group `E`, if `f` is differentiable on `s` and the difference between `f(z)` and `f(c)` is little-o of `(z-c)^{-1}`, then `f` can be redefined to be equal to the limit under `๐[โ ] c` of `f` at `c`. The updated function is then complex differentiable on the set obtained by inserting `c` into `s`. This theorem is a result in complex analysis and provides a condition under which a singularity of a function can be "removed" by redefining the function at the singular point.
More concisely: Given a complex function `f` that is differentiable on a punctured neighborhood of `c`, if `f(z) - f(c)` is little-o of `(z-c)^{-1}`, then `f` can be redefined at `c` to be equal to its limit value, making the function complex differentiable at `c`.
|
Complex.differentiableOn_update_limUnder_of_bddAbove
theorem Complex.differentiableOn_update_limUnder_of_bddAbove :
โ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] [inst_2 : CompleteSpace E] {f : โ โ E}
{s : Set โ} {c : โ},
s โ nhds c โ
DifferentiableOn โ f (s \ {c}) โ
BddAbove (norm โ f '' (s \ {c})) โ
DifferentiableOn โ (Function.update f c (limUnder (nhdsWithin c {c}แถ) f)) s
The **Removable Singularity** theorem states that, given a neighborhood `s` of a complex number `c` and a function `f` from the complex numbers to a complete normed additive commutative group `E`, if `f` is complex differentiable and its norm is bounded on `s` excluding `c`, then `f`, when redefined to be equal to the limit under the "neighborhood within" filter of `f` at `c`, is complex differentiable on `s`. In other words, it allows us to "remove" a singularity at `c` by redefining the function to be equal to the limit of `f` nearby `c`, provided that `f` is complex differentiable and bounded around `c` but excluding `c` itself.
More concisely: Given a complex neighborhood `s` of a complex number `c`, if a complex differentiable function `f` from the complex numbers to a complete normed additive commutative group `E` is bounded on `s` excluding `c`, then `f` is complex differentiable on `s` when redefined to be equal to its limit at `c`.
|