Complex.hasSum_deriv_of_summable_norm
theorem Complex.hasSum_deriv_of_summable_norm :
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E]
{U : Set ℂ} {z : ℂ} {F : ι → ℂ → E} {u : ι → ℝ},
Summable u →
(∀ (i : ι), DifferentiableOn ℂ (F i) U) →
IsOpen U →
(∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i) →
z ∈ U → HasSum (fun i => deriv (F i) z) (deriv (fun w => ∑' (i : ι), F i w) z)
The theorem `Complex.hasSum_deriv_of_summable_norm` states that given a set `U` of complex numbers which is open, a summable function `u`, and a function `F` from an index set `ι` to functions from complex numbers to a normed additive commutative group `E`. If every function `F i` is differentiable on `U` and the norm of `F i w` is bounded by `u i` for each `w` in `U`, then for any `z` in `U`, the sum of the derivatives of `F i` at `z` is the derivative of the sum of the `F i` at `z`. In other words, under these conditions, differentiation and summation can be interchanged.
More concisely: If `U` is an open set of complex numbers, `u` is summable, `F : ι → (Complex → E)` is a family of differentiable functions with bounded derivatives on `U`, then the sum of the derivatives of `F i` is the derivative of the sum of `F i` at every point `z` in `U`.
|
Complex.differentiableOn_tsum_of_summable_norm
theorem Complex.differentiableOn_tsum_of_summable_norm :
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E]
{U : Set ℂ} {F : ι → ℂ → E} {u : ι → ℝ},
Summable u →
(∀ (i : ι), DifferentiableOn ℂ (F i) U) →
IsOpen U → (∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i) → DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
The theorem `Complex.differentiableOn_tsum_of_summable_norm` states that, given a set `U` in the complex plane, a series of complex-valued functions (indexed by `ι`) each of which is differentiable on `U`, and a real-valued sequence `u` such that the norm of each term in the series at any point in `U` is bounded by the corresponding term in `u` which is summable, then the sum of the series of functions is also differentiable on `U`. This means that if the terms in the infinite sum are uniformly bounded on `U` by a summable function and each term is differentiable on `U`, then the infinite sum is also differentiable on `U`.
More concisely: If each term of a complex-valued series of differentiable functions on a set U is pointwise bounded by a summable function, then the sum of the series is differentiable on U.
|
TendstoLocallyUniformlyOn.differentiableOn
theorem TendstoLocallyUniformlyOn.differentiableOn :
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E]
{U : Set ℂ} {φ : Filter ι} {F : ι → ℂ → E} {f : ℂ → E} [inst_3 : φ.NeBot],
TendstoLocallyUniformlyOn F f φ U →
(∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) → IsOpen U → DifferentiableOn ℂ f U
The theorem `TendstoLocallyUniformlyOn.differentiableOn` states that if we have a locally uniform limit of holomorphic functions (represented as `F : ι → ℂ → E`) on an open domain `U` of the complex plane (represented as `Set ℂ`), and each function in the family is differentiable, then the limit function `f` is also differentiable on the domain `U`. Here, `TendstoLocallyUniformlyOn F f φ U` asserts that the functions `F` converge locally uniformly to `f` on the domain `U` with respect to the filter `φ`, and `DifferentiableOn ℂ (F n) U` asserts that each function `F n` is differentiable on the domain `U`. Finally, `IsOpen U` confirms that `U` is an open set in the complex plane.
More concisely: If `F : ι → ℂ → E` is a family of differentiable holomorphic functions on the open set `U` of the complex plane, and `F` converges locally uniformly to `f` on `U`, then `f` is differentiable on `U`.
|