LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Calculus.SmoothSeries

`hasDerivAt_tsum_of_isPreconnected` theorem hasDerivAt_tsum_of_isPreconnected : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : CompleteSpace F] {u : α → ℝ} [inst_3 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F} {t : Set 𝕜} {y₀ y : 𝕜}, Summable u → IsOpen t → IsPreconnected t → (∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y) → (∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n) → y₀ ∈ t → (Summable fun n => g n y₀) → y ∈ t → HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y This theorem states that, given a series of functions, `∑' n, f n x`, defined on a preconnected open set, if the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series itself is differentiable on the set and its derivative is the sum of the derivatives. More specifically, let `u` be a summable function, `t` an open and preconnected set, `g` and `g'` functions such that for every `n` and `y` in `t`, `g n` has the derivative `g' n y` at `y` and the norm of `g' n y` is less or equal to `u n`. If `y₀` is in `t` and the series `∑' n, g n y₀` is summable, then for any `y` in `t`, the derivative at `y` of the function `z ↦ ∑' n, g n z` is `∑' n, g' n y`. More concisely: If `u` is summable, `t` is an open and preconnected set, `g n` is differentiable with summable derivatives on `t`, `y₀` is in `t`, and the series `∑' n, g n y₀` is summable, then the function `z ↦ ∑' n, g n z` is differentiable on `t` with derivative `∑' n, g' n y`.
`iteratedFDeriv_tsum` theorem iteratedFDeriv_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] [inst_5 : NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞}, (∀ (i : α), ContDiff 𝕜 N (f i)) → (∀ (k : ℕ), ↑k ≤ N → Summable (v k)) → (∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) → ∀ {k : ℕ}, ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x This theorem states that if you have a series of smooth functions where the successive derivatives have summable uniform bounds, then the k-th derivative of the sum of these functions is equal to the sum of the k-th derivatives of the individual functions. This is under the condition that the k-th derivative of each function in the series is continuously differentiable up to order N and the norm of the k-th derivative of each function is less than or equal to some summable function v_k. The sum in this context is an infinite sum. More concisely: If {f\_n : ℝ → ℝ} is a sequence of smooth functions with uniformly summable sup-norms of their derivatives up to order k, then the k-th derivative of the infinite sum Σ_(n=1)^∞ f\_n is equal to the infinite sum Σ_(n=1)^∞ (the k-th derivative of f\_n).
`contDiff_tsum` theorem contDiff_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] [inst_5 : NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞}, (∀ (i : α), ContDiff 𝕜 N (f i)) → (∀ (k : ℕ), ↑k ≤ N → Summable (v k)) → (∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) → ContDiff 𝕜 N fun x => ∑' (i : α), f i x The theorem `contDiff_tsum` states that for a series of functions represented as `∑' i, f i x`, if each individual function `f i` is `C^N` differentiable and there exists a uniform summable upper bound on the `k`-th derivative for every `k ≤ N`, then the entire series is also `C^N` differentiable. In other words, the differentiability properties of the individual functions and the summability of their derivatives' upper bounds ensure the differentiability of the whole series. The theorem is applicable in the context of a real or complex-like field `𝕜`, normed additive commutative groups `E` and `F`, where `F` is also complete, and `E` and `F` are both normed vector spaces over `𝕜`. The functions `f` map from type `α` to a function from `E` to `F`. The functions `v` map from natural numbers to functions from `α` to real numbers. The differentiability is with respect to `N`, which can be a finite natural number or infinity. More concisely: If each function in a uniformly summable series of `C^N` differentiable functions from `α` to the continuous functions from a normed vector space `E` to a Banach space `F` over a real or complex field, has an upper bound on their `k`-th derivatives that is uniformly summable for all `k ≤ N`, then the sum is also `C^N` differentiable.
`hasFDerivAt_tsum_of_isPreconnected` theorem hasFDerivAt_tsum_of_isPreconnected : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] {u : α → ℝ} [inst_5 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set E} {x₀ x : E}, Summable u → IsOpen s → IsPreconnected s → (∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) → (∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n) → x₀ ∈ s → (Summable fun n => f n x₀) → x ∈ s → HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x This theorem states that for a series of functions `∑' n, f n x` defined over a preconnected open set, if the series converges at a point, and all the functions in the series are differentiable with a summable upper bound on the derivatives, then the series itself is differentiable on the set and its derivative is the sum of the derivatives. Further, the theorem specifies that this holds for all types of `𝕜` that behave like real numbers (`RCLike 𝕜`), and for all types `E` and `F` that form a normed additive commutative group and a normed vector space over `𝕜`. The theorem also requires the space `F` to be complete. The functions `f` and `f'` map from `α` and `E` to `F` and from `α` and `E` to a continuous linear map from `E` to `F`, respectively. The set `s` is a set of elements of type `E`, and `x₀` and `x` are elements of `E`. This theorem is proven under the assumptions that `u` is summable, `s` is an open and preconnected set, the derivative of `f` at `x` for every `x` in `s` is `f'`, the norm of `f'` at `x` for every `x` in `s` is less than or equal to `u`, `x₀` is an element of `s`, the series of `f` at `x₀` is summable, and `x` is an element of `s`. More concisely: If `∑' n, f n` is a series of differentiable functions over an open and preconnected set `s` with summable upper bound on derivatives, and the functions and their derivatives are all continuous linear maps, then `∑' n, f n` is differentiable on `s` and its derivative is the sum of the derivatives.
`summable_of_summable_hasDerivAt` theorem summable_of_summable_hasDerivAt : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : CompleteSpace F] {u : α → ℝ} [inst_3 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F} {y₀ : 𝕜}, Summable u → (∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y) → (∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n) → (Summable fun n => g n y₀) → ∀ (y : 𝕜), Summable fun n => g n y This theorem states that for a series of functions `∑' n, f n x`, if the series converges at a certain point, and each function in the series is differentiable with a summable upper bound on the derivatives, then the series will converge for all values. More formally, let `u : α → ℝ`, `g, g' : α → 𝕜 → F`,`y₀ : 𝕜` be given such that `u` is summable, each `g n` has derivative `g' n y` at every `y : 𝕜`, and the norm of `g' n y` is less than or equal to `u n` for all `n : α` and `y : 𝕜`. If the series `∑' n, g n y₀` is summable at `y₀`, then for all `y : 𝕜`, the series `∑' n, g n y` is summable. More concisely: If a series of differentiable functions with summable upper bounds on derivatives converges at a point, then it converges absolutely for all points.
`summable_of_summable_hasFDerivAt_of_isPreconnected` theorem summable_of_summable_hasFDerivAt_of_isPreconnected : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] {u : α → ℝ} [inst_5 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set E} {x₀ x : E}, Summable u → IsOpen s → IsPreconnected s → (∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) → (∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n) → x₀ ∈ s → (Summable fun x => f x x₀) → x ∈ s → Summable fun n => f n x This theorem states that for any series of functions, denoted as `∑' n, f n x`, defined on a preconnected open set, if the series converges at a particular point, and all functions in the series are differentiable with a summable bound on their derivatives, then the series will converge at every point within the set. More specifically, given a type `α`, scalars of type `𝕜`, a normed additive commutative group `E`, and a complete space `F` with norms, along with a function `u : α → ℝ`, a family of functions `f : α → E → F`, a derivative function `f' : α → E → E →L[𝕜] F`, and a set `s : Set E`, if `u` is summable, `s` is an open and preconnected set, each function `f n` has a derivative `f' n x` at each point `x` in `s`, and the norm of each `f' n x` is bounded by `u n`, then if the series `∑' n, f n x` converges at a point `x₀` in `s`, it will also converge for any other point `x` in `s`. More concisely: If a series of differentiable functions with summable bounds on their derivatives converges at a point in a preconnected open set, then it converges at every point within that set.
`differentiable_tsum` theorem differentiable_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] {u : α → ℝ} [inst_5 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F}, Summable u → (∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) → (∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) → Differentiable 𝕜 fun y => ∑' (n : α), f n y This theorem states that given a series of functions, denoted by `∑' n, f n x`, if all functions in the series are differentiable with a summable bound on their derivatives, then the series is differentiable. The theorem takes into account that the series may not be pointwise convergent. However, in the case that there is no pointwise convergence, the series evaluates to zero everywhere, thus maintaining the accuracy of the theorem. More concisely: If each function in a series `∑' n, f n x` is differentiable and the series of derivatives is absolutely convergent, then the series is differentiable.
`differentiable_tsum'` theorem differentiable_tsum' : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : CompleteSpace F] {u : α → ℝ} [inst_3 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F}, Summable u → (∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y) → (∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n) → Differentiable 𝕜 fun z => ∑' (n : α), g n z This theorem states that given a series of functions represented as `∑' n, f n x`, if all functions in the series are differentiable with a summable bound on the derivatives, then the series itself is differentiable. This holds even if there is no pointwise convergence of the series because, in such cases, the series would be zero everywhere. In mathematical terms, for all functions `g` and `g'` from `α` and `𝕜` to `F`, if the sum of `u`, a function from `α` to `ℝ`, is finite (Summable `u`), and for all `n` in `α` and `y` in `𝕜`, function `g n` has derivative `g' n y` at `y` (`HasDerivAt (g n) (g' n y) y`), and the norm of `g' n y` is less than or equal to `u n` (`‖g' n y‖ ≤ u n`), then the function `z => ∑' (n : α), g n z` is differentiable. More concisely: If `∑' (n : α), g n` is a series of differentiable functions from `α` to `F` with derivatives bounded by a summable function `u`, then `∑' (n : α), g n` is itself differentiable.
`summable_of_summable_hasFDerivAt` theorem summable_of_summable_hasFDerivAt : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] {u : α → ℝ} [inst_5 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {x₀ : E}, Summable u → (∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) → (∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) → (Summable fun n => f n x₀) → ∀ (x : E), Summable fun n => f n x The theorem `summable_of_summable_hasFDerivAt` states that given a series of functions `∑' n, f n x` indexed by a type `α`, under certain conditions, if the series converges at a single point `x₀` in the domain, then the series converges for all points in the domain. The conditions are: - There exists a real-valued function `u` on the index set `α` such that `u` is summable. - Each function `f n` in the series is differentiable at every point in the domain, with derivative `f' n x`. - The norm of the derivative `f' n x` is bounded above by `u n` for each `n` and `x`. - The series `∑' n, f n x` is summable at the point `x₀`. If these conditions hold, then for any `x` in the domain, the series `∑' n, f n x` is also summable. This theorem can be used in the analysis of convergent series of functions, particularly in the context of power series or Fourier series. More concisely: Given a series of differentiable functions `∑' n, f n x` indexed by a type `α`, if it is summable at a point `x₀`, has a bounded derivative norm `∥f' n x∥ ≤ u n`, and `u` is summable, then the series is summable for all `x` in the domain.
`contDiff_tsum_of_eventually` theorem contDiff_tsum_of_eventually : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] [inst_5 : NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞}, (∀ (i : α), ContDiff 𝕜 N (f i)) → (∀ (k : ℕ), ↑k ≤ N → Summable (v k)) → (∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in Filter.cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) → ContDiff 𝕜 N fun x => ∑' (i : α), f i x The theorem `contDiff_tsum_of_eventually` states that if we consider an infinite series of functions, denoted as `∑' i, f i x`, where each individual function `f i` is of the class `C^N` (meaning it has continuous derivatives up to the `N`-th order), and there exists a uniformly summable upper bound on the `k`-th derivative for each `k ≤ N`, except maybe for a finite number of functions `i`, then the series of functions retains the `C^N` property. The uniform summable upper bounds are represented by the series `v k`, and the condition of the upper bound for each `k` derivative is required to hold for all `i` except for a finite number of them. This is captured by the use of `Filter.cofinite`, which refers to the set of those `i` for which the condition holds, with only a finite number of exceptions. The theorem concludes that, under these conditions, the function represented by the series `∑' (i : α), f i x` is also of class `C^N`. More concisely: If each function in an infinite series of `C^N` functions with uniformly summable upper bounds on their derivatives up to order `N`, except for a finite number of functions, then the sum of these functions is also a `C^N` function.
`summable_of_summable_hasDerivAt_of_isPreconnected` theorem summable_of_summable_hasDerivAt_of_isPreconnected : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : CompleteSpace F] {u : α → ℝ} [inst_3 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F} {t : Set 𝕜} {y₀ y : 𝕜}, Summable u → IsOpen t → IsPreconnected t → (∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y) → (∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n) → y₀ ∈ t → (Summable fun x => g x y₀) → y ∈ t → Summable fun n => g n y This theorem states that given a series of functions `∑' n, f n x` on a preconnected open set `t` in some normed space, if the series converges at a particular point `y₀` within `t`, and each function in the series is differentiable with its derivative within a summable bound, then the series of functions converges for any point `y` within `t`. In more precise terms, for each function `g n` in the series and its corresponding derivative `g' n`, the norm of `g' n y` is less than or equal to some summable series `u`. The theorem thus asserts the everywhere convergence of the series under these conditions. More concisely: Given a series of differentiable functions `∑' n, f n : X → ℝ` on an open set `X` in a normed space, if the series converges at a point `y₀` and the norms of their derivatives are summable at `y₀`, then the series converges for all `y` in `X`.
`hasDerivAt_tsum` theorem hasDerivAt_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : CompleteSpace F] {u : α → ℝ} [inst_3 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F} {y₀ : 𝕜}, Summable u → (∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y) → (∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n) → (Summable fun n => g n y₀) → ∀ (y : 𝕜), HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y This theorem states that for a series of functions expressed as `∑' n, f n x`, if the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series itself is differentiable. Furthermore, the derivative of the series is the sum of the derivatives of the individual functions. In more detail, given a series of functions `g n` from type `α` to `𝕜 → F`, if the series `∑' n, g n x` converges at a point `y₀`, each function `g n` is differentiable at any point `y` with derivative `g' n y`, and the norm of each derivative is bounded by a corresponding summable sequence `u n`, then the derivative of `∑' n, g n z` at any point `y` exists and is given by `∑' n, g' n y`. More concisely: If a series of differentiable functions `g n : α → ℝ → F` with summable bounds on their derivatives converges pointwise, then the series of their derivatives also converges and is the derivative of the original series.
`iteratedFDeriv_tsum_apply` theorem iteratedFDeriv_tsum_apply : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] [inst_5 : NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞}, (∀ (i : α), ContDiff 𝕜 N (f i)) → (∀ (k : ℕ), ↑k ≤ N → Summable (v k)) → (∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) → ∀ {k : ℕ}, ↑k ≤ N → ∀ (x : E), iteratedFDeriv 𝕜 k (fun y => ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x This theorem states that if we have a series of smooth functions, where the uniform bounds on their successive derivatives are summable, then the $k$th iterated derivative of the infinite sum of these functions equals the infinite sum of the $k$th iterated derivatives of the individual functions. Here, $k$ is a non-negative integer that is less than or equal to a given value $N$. This result holds for all points in the domain of the functions. The functions map from a normed vector space $E$ over a field $\mathbb{K}$, which behaves like real numbers, to another normed vector space $F$ over the same field, and $F$ is also assumed to be complete. More concisely: If $N$ is a non-negative integer, and $f\_i$ is a sequence of smooth functions from a complete normed vector space $E$ to another normed vector space $F$ over the same field, such that the uniform bounds on their derivatives up to order $N$ are summable, then the $k$th iterated derivative of the infinite sum of the $f\_i$'s equals the infinite sum of the $k$th iterated derivatives of the $f\_i$'s for all $k \leq N$ and all points in the domain of the functions.
`hasFDerivAt_tsum` theorem hasFDerivAt_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] {u : α → ℝ} [inst_5 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {x₀ : E}, Summable u → (∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) → (∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) → (Summable fun n => f n x₀) → ∀ (x : E), HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x The theorem `hasFDerivAt_tsum` states that for a series of functions, denoted as `∑' n, f n x`, if the series converges at a point, and each function in the series is differentiable with a summable bound on the derivatives, then the entire series is differentiable. Moreover, the derivative of the series at a point is the sum of the derivatives of the individual functions at that point. In formal terms, given a sequence of functions `f : α → E → F` and their derivatives `f'`, if for each `n : α` and `x : E`, `f n x` is differentiable with derivative `f' n x`, and the norms of the derivatives are bounded by a summable sequence `u`, then the derivative of the series at any point `x` is the sum of the derivatives at `x`. More concisely: If each function in a differentiable, summable series of functions from `α` to `F` with summable bounds on their derivatives is differentiable at a point `x`, then the series is differentiable at `x` and its derivative is the sum of the derivatives of the individual functions at `x`.