difference_quotients_converge_uniformly
theorem difference_quotients_converge_uniformly :
∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3} [inst_1 : RCLike 𝕜]
[inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{f : ι → E → G} {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} {x : E},
TendstoUniformlyOnFilter f' g' l (nhds x) →
(∀ᶠ (n : ι × E) in l ×ˢ nhds x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2) →
(∀ᶠ (y : E) in nhds x, Filter.Tendsto (fun n => f n y) l (nhds (g y))) →
TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l
(nhds x)
The theorem `difference_quotients_converge_uniformly` states that, given a sequence of functions `f_n` converging pointwise to a function `g` and their derivatives `(f_n)'` converging uniformly to a derivative `h`, then for a fixed value `y`, the difference quotients `(‖z - y‖⁻¹) * (f_n(z) - f_n(y))` also converge uniformly to `(‖z - y‖⁻¹) * (g(z) - g(y))`. In other words, if the function values and their derivatives both converge (in their respective senses), then the rate of change of the function values also converges uniformly.
More concisely: Given a pointwise convergent sequence of differentiable functions `f_n` with uniformly convergent derivatives to `g` and `h` respectively, the difference quotients `(f_n(z) - f_n(y)) / ‖z - y‖` converge uniformly to `(g(z) - g(y)) / ‖z - y‖`.
|
hasFDerivAt_of_tendstoUniformlyOn
theorem hasFDerivAt_of_tendstoUniformlyOn :
∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3} [inst_1 : RCLike 𝕜]
[inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{f : ι → E → G} {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} [inst_5 : l.NeBot] {s : Set E},
IsOpen s →
TendstoUniformlyOn f' g' l s →
(∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) →
(∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → ∀ x ∈ s, HasFDerivAt g (g' x) x
This theorem states that, for a sequence of functions `f` and their derivatives `f'`, if these derivatives converge uniformly on an open set `s` to a limit function `g'`, and each function `f_n` has `f'_n` as its derivative at each point in `s`, then the derivative of the limit function `g` at every point in `s` is `g'`. Furthermore, it is required that for each point in `s`, the function values `f_n(x)` tend towards the limit `g(x)` as `n` tends to infinity. This theorem formalizes the interchange of the order of differentiation and limit in the case of uniform convergence of the derivatives.
More concisely: If a sequence of differentiable functions `f_n : X → ℝ` on an open set `X` converges uniformly to a limit function `g : X → ℝ`, and the derivatives `f'_n` of `f_n` converge uniformly to a limit function `g'`, then `g` is differentiable with derivative `g'` on `X`.
|
uniformCauchySeqOnFilter_of_fderiv
theorem uniformCauchySeqOnFilter_of_fderiv :
∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3} [inst_1 : RCLike 𝕜]
[inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{f : ι → E → G} {f' : ι → E → E →L[𝕜] G} {x : E},
UniformCauchySeqOnFilter f' l (nhds x) →
(∀ᶠ (n : ι × E) in l ×ˢ nhds x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2) →
Cauchy (Filter.map (fun n => f n x) l) → UniformCauchySeqOnFilter f l (nhds x)
The theorem `uniformCauchySeqOnFilter_of_fderiv` states that, if you have a sequence of real or complex functions (denoted by `f`) which are eventually differentiable on a neighborhood of some point `x`, and these functions are Cauchy at `x` (meaning that the sequence of values `f n x` forms a Cauchy sequence), and their derivatives form a uniformly Cauchy sequence on a neighborhood of `x`, then the original sequence of functions `f` also forms a uniformly Cauchy sequence in a neighborhood of `x`. This theorem generalizes the classic result about the convergence of a sequence of functions under the assumption of uniform convergence of the derivatives.
More concisely: If a sequence of real or complex functions, each eventually differentiable at a point, has Cauchy values at that point and their derivatives form a uniformly Cauchy sequence, then the original sequence is uniformly Cauchy near that point.
|
hasDerivAt_of_tendsto_locally_uniformly_on'
theorem hasDerivAt_of_tendsto_locally_uniformly_on' :
∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : RCLike 𝕜] {G : Type u_3} [inst_1 : NormedAddCommGroup G]
[inst_2 : NormedSpace 𝕜 G] {f : ι → 𝕜 → G} {g g' : 𝕜 → G} {x : 𝕜} [inst_3 : l.NeBot] {s : Set 𝕜},
IsOpen s →
TendstoLocallyUniformlyOn (deriv ∘ f) g' l s →
(∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s) →
(∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasDerivAt g (g' x) x
This theorem, `hasDerivAt_of_tendsto_locally_uniformly_on'`, is a variant of `hasDerivAt_of_tendstoLocallyUniformlyOn` but with assumptions stated in terms of `DifferentiableOn` instead of `HasDerivAt`. This is beneficial for proofs in complex analysis where holomorphicity is assumed but the derivative is not known in advance. The theorem states that for any filter `l` of type `ι` and any normed space `G` over a ring `𝕜`, if we have a family of functions `f : ι → 𝕜 → G` and two other functions `g, g' : 𝕜 → G`, then if a set `s` in `𝕜` is open and the composition `deriv ∘ f` tends uniformly locally on `s` to `g'` under `l` and all `f n` are differentiable on `s` for almost all `n` in `l`, and for any `x` in `s`, `f n x` tends to `g x` as `n` goes to `l`, then `g` has the derivative `g' x` at `x`.
More concisely: If a family of differentiable functions `f : ι → ℝ → G` on an open set `s` in a ring `𝕜` satisfies `deriv ∘ f` uniformly locally converges to `g'` and `f` is differentiable on `s` for almost all indices `n` in `ι` with `lim (n→l) (f n x) = g x` for all `x` in `s`, then `g` is differentiable at `x` with derivative `g' x`.
|
hasFDerivAt_of_tendsto_locally_uniformly_on'
theorem hasFDerivAt_of_tendsto_locally_uniformly_on' :
∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3} [inst_1 : RCLike 𝕜]
[inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{f : ι → E → G} {g : E → G} {g' : E → E →L[𝕜] G} {x : E} [inst_5 : l.NeBot] {s : Set E},
IsOpen s →
TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s →
(∀ (n : ι), DifferentiableOn 𝕜 (f n) s) →
(∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasFDerivAt g (g' x) x
The theorem `hasFDerivAt_of_tendsto_locally_uniformly_on'` states that for a family of functions `{f n : E → G}` indexed by a type `ι` and a function `g : E → G`, if the derivative of each function `f n` exists and is uniformly convergent to a function `g'` on an open set `s` within a filter `l`, and for each point `x` in `s`, if the functions `{f n}` converge to `g` as `n` tends to the filter `l`, then `g` has a derivative at each point `x` in `s`, and the derivative is `g'`. In other words, if each function in a family is differentiable on a set, and their derivatives and function values both converge pointwise, then the limit function is also differentiable with the specified derivative.
More concisely: If a family of differentiable functions on an open set converges uniformly to a limit function pointwise, then the limit function is differentiable and has the same derivative as the converging functions.
|
cauchy_map_of_uniformCauchySeqOn_fderiv
theorem cauchy_map_of_uniformCauchySeqOn_fderiv :
∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3} [inst_1 : RCLike 𝕜]
[inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{f : ι → E → G} {f' : ι → E → E →L[𝕜] G} {s : Set E},
IsOpen s →
IsPreconnected s →
UniformCauchySeqOn f' l s →
(∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y) →
∀ {x₀ x : E},
x₀ ∈ s → x ∈ s → Cauchy (Filter.map (fun n => f n x₀) l) → Cauchy (Filter.map (fun n => f n x) l)
The theorem states that if you have a sequence of functions between real or complex normed spaces that are differentiable on a preconnected open set, and if the sequence of these functions at a certain point forms a Cauchy sequence and their derivatives form a uniformly Cauchy sequence on the set, then the sequence of these functions at any point in the set will also form a Cauchy sequence. In other words, the Cauchy property of the sequence of functions at a certain point in the set, and the uniform Cauchy property of their derivatives over the set, extends to the Cauchy property of the sequence of functions at any point in the set.
More concisely: If a sequence of differentiable functions between real or complex normed spaces is point-wise Cauchy at a point and uniformly Cauchy in their derivatives on an open set, then the sequence is Cauchy at any point in the set.
|
UniformCauchySeqOnFilter.one_smulRight
theorem UniformCauchySeqOnFilter.one_smulRight :
∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : RCLike 𝕜] {G : Type u_3} [inst_1 : NormedAddCommGroup G]
[inst_2 : NormedSpace 𝕜 G] {f' : ι → 𝕜 → G} {l' : Filter 𝕜},
UniformCauchySeqOnFilter f' l l' →
UniformCauchySeqOnFilter (fun n z => ContinuousLinearMap.smulRight 1 (f' n z)) l l'
This theorem states that if a sequence of derivatives (represented by `f'`) converges uniformly, then the corresponding sequence of Fréchet derivatives will also converge uniformly. In the context of this theorem, uniform convergence is defined in terms of the `UniformCauchySeqOnFilter` predicate, which states that for every point in the uniformity of the codomain space, every filter (which can be thought of as a generalized sequence) eventually reaches a point where all pairwise differences are within that point. The Fréchet derivatives are obtained by applying the `ContinuousLinearMap.smulRight 1` operation to each element of the original sequence. This operation essentially scales the derivative by a scalar (in this case 1), yielding the Fréchet derivative.
More concisely: If a sequence of functions `f'_i` converges uniformly, then the sequence of Fréchet derivatives `ContinuousLinearMap.smulRight 1 (f'_i)` converges uniformly.
|
hasFDerivAt_of_tendstoUniformlyOnFilter
theorem hasFDerivAt_of_tendstoUniformlyOnFilter :
∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3} [inst_1 : RCLike 𝕜]
[inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{f : ι → E → G} {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} {x : E} [inst_5 : l.NeBot],
TendstoUniformlyOnFilter f' g' l (nhds x) →
(∀ᶠ (n : ι × E) in l ×ˢ nhds x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2) →
(∀ᶠ (y : E) in nhds x, Filter.Tendsto (fun n => f n y) l (nhds (g y))) → HasFDerivAt g (g' x) x
This theorem, `hasFDerivAt_of_tendstoUniformlyOnFilter`, states that under certain conditions, the derivative of the limit of a sequence of functions is equal to the limit of the derivatives of the functions. Specifically, here are the conditions:
* The sequence of derivatives, denoted as `f'`, converges uniformly on a neighborhood of a point `x` to a function `g'`. This means that for any given level of proximity (measured in the target space), there is a point in the sequence beyond which all function values are at least that close to the limit function, regardless of where in the domain (within the neighborhood of `x`) you evaluate it.
* For every pair `(y, n)` where `y` is sufficiently close to `x` and `n` is sufficiently large, `f' n` is the derivative of `f n`. This is saying that within the neighborhood of `x`, each function `f n` in the sequence has `f' n` as its derivative.
* The sequence of functions `f n` converges pointwise to a function `g` on a neighborhood of `x`. This means that for each point in the domain within the neighborhood of `x`, the function values of `f n` converge to the value of `g` at that point.
When these conditions are satisfied, the theorem asserts that `g' x` is the derivative of `g` at `x`.
More concisely: If a sequence of differentiable functions converges uniformly on a neighborhood of a point to a limit function, and the derivatives of the sequence of functions converge uniformly to a limit function on that neighborhood, then the limit function is differentiable at that point and its derivative is equal to the limit of the derivatives.
|
hasFDerivAt_of_tendstoUniformly
theorem hasFDerivAt_of_tendstoUniformly :
∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3} [inst_1 : RCLike 𝕜]
[inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{f : ι → E → G} {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} [inst_5 : l.NeBot],
TendstoUniformly f' g' l →
(∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x) →
(∀ (x : E), Filter.Tendsto (fun n => f n x) l (nhds (g x))) → ∀ (x : E), HasFDerivAt g (g' x) x
The theorem `hasFDerivAt_of_tendstoUniformly` states that if a sequence of functions `f n` has derivatives `f' n` at every point `x` (in the sense of `HasFDerivAt`), and these derivatives converge uniformly to a limit function `g'` as `n` tends to infinity, then the limit of the function `f n` itself (in the Filter sense of limit) is a function `g` that has `g'` as its derivative at every point `x`.
In mathematical notation, the theorem states that if `(d/dx) f_n(x) = f'_n(x)` for all `n` and `x`, and `f'_n(x)` converges uniformly to `g'(x)`, then the limit of `f_n(x)` as `n` goes to infinity is a function `g(x)` such that `(d/dx) g(x) = g'(x)`.
More concisely: If a sequence of differentiable functions `f_n : ℝ → ℝ` with derivatives `f'_n` converges uniformly to a limit function `g'`, then the pointwise limit `g` of `f_n` is a differentiable function with derivative `g'`.
|
uniformCauchySeqOn_ball_of_fderiv
theorem uniformCauchySeqOn_ball_of_fderiv :
∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3} [inst_1 : RCLike 𝕜]
[inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{f : ι → E → G} {f' : ι → E → E →L[𝕜] G} {x : E} {r : ℝ},
UniformCauchySeqOn f' l (Metric.ball x r) →
(∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y) →
Cauchy (Filter.map (fun n => f n x) l) → UniformCauchySeqOn f l (Metric.ball x r)
This theorem, a variant of the second fundamental theorem of calculus (FTC-2), states that if you have a sequence of functions that map from real or complex normed spaces and are differentiable on a ball centered at a point `x`, and if these functions form a Cauchy sequence _at_ `x`, and their derivatives are uniformly Cauchy on the ball, then the functions themselves form a uniform Cauchy sequence on the ball. This condition of working within a ball is typically used when dealing with power series and Dirichlet series. The theorem could be generalized to work with any connected, bounded, open set by replacing the ball, and replacing uniform convergence with local uniform convergence.
More concisely: If a sequence of differentiable functions on a ball around a point with uniformly Cauchy derivatives forms a Cauchy sequence at the point, then the functions themselves form a uniformly Cauchy sequence on the ball. (A variant of the second fundamental theorem of calculus)
|