iteratedFDerivWithin_inter
theorem iteratedFDerivWithin_inter :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s u : Set E}
{f : E β F} {x : E} {n : β}, u β nhds x β iteratedFDerivWithin π n f (s β© u) x = iteratedFDerivWithin π n f s x
This theorem states that for a nontrivially normed field `π`, normed additive commutative groups `E` and `F`, normed spaces `π E` and `π F`, a function `f` mapping `E` to `F`, a point `x` in `E`, a natural number `n`, and two sets `s` and `u` in `E`, if the set `u` is a neighborhood of the point `x` (i.e., `u` belongs to the neighborhood filter of `x`), then the `n`-th iterated FrΓ©chet derivative of `f` within the intersection of `s` and `u` at the point `x` is equivalent to the `n`-th iterated FrΓ©chet derivative of `f` within the set `s` at the point `x`. In other words, intersecting the set `s` with a neighborhood of `x` does not change the `n`-th iterated FrΓ©chet derivative of `f` at `x` within the set `s`.
More concisely: For a nontrivially normed field `π`, given normed spaces `π E` and `π F`, a continuously differentiable function `f : E β F`, a point `x` in `E`, a natural number `n`, and sets `s` and `u` in `E` with `u` being a neighborhood of `x`, the `n`-th iterated FrΓ©chet derivative of `f` at `x` within `s β© u` is equal to the `n`-th iterated FrΓ©chet derivative of `f` at `x` within `s`.
|
ContDiff.differentiable
theorem ContDiff.differentiable :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ}, ContDiff π n f β 1 β€ n β Differentiable π f
The theorem `ContDiff.differentiable` states that for any function `f` mapping from a normed space `E` to another normed space `F` over a nontrivially normed field `π`, if `f` is continuously differentiable `n` times for `n` equal to or greater than 1 (`C^n` with `n β₯ 1`), then `f` is differentiable at any point. In mathematical terms, if a function is `C^n` for `n β₯ 1`, then it is differentiable everywhere.
More concisely: A continuously differentiable function of class `C^n` with `n β₯ 1` from a normed space to another normed space is differentiable at every point.
|
ContDiffOn.contDiffAt
theorem ContDiffOn.contDiffAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ}, ContDiffOn π n f s β s β nhds x β ContDiffAt π n f x
This theorem states that if a function `f` of type `E β F` is continuously differentiable to any order `n` on a set `s` in a normed additive commutative group `E` equipped with a nontrivially normed field `π` (this set belongs to the normed space `π E`), and if the set `s` is a neighborhood of a point `x` (i.e., it contains an open set around `x`), then the function `f` is continuously differentiable to the order `n` at the point `x`. The spaces `E` and `F` are assumed to be normed additive commutative groups over the field `π` and equipped with the normed space structure.
In simpler terms, this theorem is a formal statement of the intuition that if a function is continuously differentiable everywhere in a certain neighborhood, then it is continuously differentiable at any particular point within that neighborhood.
More concisely: If a function `f : E β F` is continuously differentiable to order `n` on a neighborhood `s` of a point `x` in the normed additive commutative groups `E` and `F` over a nontrivially normed field `π`, then `f` is continuously differentiable to order `n` at `x`.
|
ContDiffOn.of_le
theorem ContDiffOn.of_le :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {m n : ββ}, ContDiffOn π n f s β m β€ n β ContDiffOn π m f s
This theorem states that for any non-trivially normed field `π`, a normed additive commutative group `E`, a normed space over `π` and `E`, another normed additive commutative group `F`, and another normed space over `π` and `F`, if a function `f` from `E` to `F` is `n` times continuously differentiable on a set `s` of `E`, and if `m` is less than or equal to `n`, then `f` is also `m` times continuously differentiable on `s`. Here, `π` is the domain of scalars, `E` and `F` are the domains of the function `f`, `n` and `m` are the orders of differentiation, and `s` is the set on which the function `f` is being considered.
More concisely: If `f` is `n` times continuously differentiable from a non-trivially normed field `π` into another non-trivially normed space over different normed additive commutative groups `E` and `F`, then `f` is also `m` times continuously differentiable on a set `s` for `m` less than or equal to `n`.
|
ContDiffWithinAt.congr_of_eventuallyEq
theorem ContDiffWithinAt.congr_of_eventuallyEq :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f fβ : E β F} {x : E} {n : ββ},
ContDiffWithinAt π n f s x β (nhdsWithin x s).EventuallyEq fβ f β fβ x = f x β ContDiffWithinAt π n fβ s x
The theorem `ContDiffWithinAt.congr_of_eventuallyEq` states that for every normed field `π`, every normed additive commutative group `E`, every normed space over `π` and `E`, every normed additive commutative group `F`, every normed space over `π` and `F`, every set of elements from `E` called `s`, every two functions `f` and `fβ` from `E` to `F`, every element `x` from `E`, and every natural number or infinity `n`, if the function `f` is continuously differentiable within the set `s` at the point `x` up to order `n`, and if function `fβ` eventually equals function `f` at a neighborhood within the set `s` around the point `x`, and if the value of `fβ` at `x` equals the value of `f` at `x`, then the function `fβ` is also continuously differentiable within the set `s` at the point `x` up to order `n`. This theorem is crucial when we want to determine the differentiability of a function that is equal to another function on a neighborhood.
More concisely: If a function is continuously differentiable within a set to order n at a point, and another function equals it eventually in a neighborhood of that point with the same value at the point, then the second function is also continuously differentiable within the set to order n at the point.
|
ContDiffWithinAt.of_le
theorem ContDiffWithinAt.of_le :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {m n : ββ}, ContDiffWithinAt π n f s x β m β€ n β ContDiffWithinAt π m f s x
This theorem, named `ContDiffWithinAt.of_le`, states that for any types `π` (which is a non-trivially normed field), `E` and `F` (both of which are normed additive commutative groups and normed spaces over `π`), a set `s` of type `E`, a function `f` from `E` to `F`, an element `x` of `E`, and two natural-number-or-infinity values `m` and `n`, if the function `f` has `n`-th order continuous differentiability at the point `x` within the set `s`, and if `m` is less than or equal to `n`, then the function `f` also has `m`-th order continuous differentiability at the point `x` within the set `s`. In simpler terms, it means that continuous differentiability of a certain order implies the continuous differentiability of any lesser order.
More concisely: If a function has `n`-th order continuous differentiability at a point in a set, then it also has `m`-th order continuous differentiability at that point for any `m` less than or equal to `n`.
|
contDiffWithinAt_univ
theorem contDiffWithinAt_univ :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} {n : ββ}, ContDiffWithinAt π n f Set.univ x β ContDiffAt π n f x
This theorem, named `contDiffWithinAt_univ`, states that for any nontrivially normed field `π`, any normed additive commutative group `E` and `F` over `π`, any function `f` from `E` to `F`, any point `x` in `E`, and any natural number or infinity `n`, the function `f` is continuously differentiable within the universal set at point `x` if and only if `f` is continuously differentiable at point `x`. In other words, if a function is continuously differentiable at a point in the whole space, it is also continuously differentiable at that point when restricting to any open subset, and vice versa.
More concisely: For any nontrivially normed field `π`, normed additive commutative groups `E` and `F` over `π`, function `f` from `E` to `F`, point `x` in `E`, and natural number or infinity `n`, `f` is continuously differentiable within the universal set at `x` if and only if it is continuously differentiable at `x`.
|
ContDiff.differentiable_iteratedFDeriv
theorem ContDiff.differentiable_iteratedFDeriv :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ} {m : β}, βm < n β ContDiff π n f β Differentiable π fun x => iteratedFDeriv π m f x
The theorem `ContDiff.differentiable_iteratedFDeriv` asserts that if a function `f` is `C^n` (meaning it is continuously differentiable up to `n` times), then its `m`-times iterated derivative is differentiable for `m < n`. Here, `iteratedFDeriv π m f` denotes the `m`-times iterated derivative of `f` with respect to the normed field `π`. The function `f` is a function from a normed vector space `E` to another normed vector space `F`, both over the same normed field `π`.
More concisely: If `f` is a `C^n` function from a normed vector space `E` to a normed vector space `F` over the same normed field `π`, then its `m`-times iterated derivative `iteratedFDeriv π m f` is differentiable for `m < n`.
|
ContDiffAt.differentiableAt
theorem ContDiffAt.differentiableAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} {n : ββ}, ContDiffAt π n f x β 1 β€ n β DifferentiableAt π f x
The theorem `ContDiffAt.differentiableAt` states that for any given function `f` from `E` to `F`, where `E` and `F` are normed additive commutative groups over a nontrivially normed field `π`, if the function `f` is `C^n` continuous at a point `x` in `E` for some `n β₯ 1` (meaning that all derivatives up to the `n`th exist and are continuous), then the function `f` is also differentiable at the point `x`. This theorem thereby links the concepts of differentiability and higher order continuous differentiability.
More concisely: If a function `f` from a normed additive commutative group `E` to another (`F`) is `C^n` continuous at a point `x` in `E` for some `n β₯ 1`, then `f` is differentiable at `x`.
|
contDiffAt_succ_iff_hasFDerivAt
theorem contDiffAt_succ_iff_hasFDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} {n : β},
ContDiffAt π (β(n + 1)) f x β β f', (β u β nhds x, β x β u, HasFDerivAt f (f' x) x) β§ ContDiffAt π (βn) f' x
The theorem `contDiffAt_succ_iff_hasFDerivAt` states that for a function `f` mapping from a normed vector space `E` over a non-trivially normed field `π` to another normed vector space `F` over the same field, the function is continuously differentiable at a point `x` in `E` to the `(n + 1)`-th order if and only if there exists a function `f'` and a neighborhood `u` of `x` such that `f'` is the derivative of `f` at any point within `u` and `f'` is continuously differentiable at `x` to the `n`-th order.
More concisely: A function `f : E β F` between normed vector spaces is continuously differentiable at `x` to order `n + 1` if and only if there exists a continuously differentiable function `f' : E β F` and a neighborhood `u` of `x` such that `f'` is the `(n + 1)`-th derivative of `f` on `u`.
|
HasFTaylorSeriesUpToOn.differentiableAt
theorem HasFTaylorSeriesUpToOn.differentiableAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ} {p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpToOn n f p s β 1 β€ n β s β nhds x β DifferentiableAt π f x
This theorem states that if a function has a Taylor series of order at least `1` on a neighborhood of a point `x`, then the function is differentiable at `x`. More specifically, given a non-trivial normed field `π`, an additive commutative group `E` equipped with a normed space over `π`, another additive commutative group `F` also equipped with a normed space over `π`, a set `s` of elements from `E`, a function `f` from `E` to `F`, a point `x` in `E`, a possibly infinite natural number `n`, and a Taylor series `p` of the function `f`, if the Taylor series `p` holds up to `n` for the function `f` on the set `s`, and `n` is at least `1`, and the set `s` is a neighborhood of `x`, then the function `f` is differentiable at `x` in the normed space.
More concisely: If a function has a Taylor series of order 1 or higher that holds on a neighborhood of a point, then the function is differentiable at that point.
|
contDiffOn_succ_iff_hasFDerivWithinAt
theorem contDiffOn_succ_iff_hasFDerivWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : β},
ContDiffOn π (β(n + 1)) f s β
β x β s,
β u β nhdsWithin x (insert x s), β f', (β x β u, HasFDerivWithinAt f (f' x) u x) β§ ContDiffOn π (βn) f' u
This theorem states that a function `f` is continuously differentiable `n + 1` times on a domain `s` if and only if, for each point `x` in `s`, there exists a neighborhood `u` within `s` and the point `x` (in the sense of topological spaces), and a function `f'`, such that `f` has its derivative `f'` within `u` at every point in `u` and the function `f'` is continuously differentiable `n` times within `u`. Here, `π` is a nontrivially normed field, `E` and `F` are normed spaces over the field `π`, and `f` is a function from `E` to `F`. In other words, this theorem is about the local property of higher-order differentiability in the context of normed spaces and topological spaces.
More concisely: A function `f : E β F` between normed spaces is continuously differentiable `n + 1` times on a domain `s` if and only if, for each point `x` in `s`, there exists a neighborhood `u` and a continuously differentiable `n`-times function `f' : u β F` such that `f` has derivative `f'` at every point in `u` within `s`.
|
ContDiff.of_le
theorem ContDiff.of_le :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{m n : ββ}, ContDiff π n f β m β€ n β ContDiff π m f
This theorem states that for any non-trivially normed field `π`, normed additive commutative group `E` and `F`, and the normed spaces `π E` and `π F`, if a function `f` from `E` to `F` is continuous and differentiable up to order `n`, and if `m` is less than or equal to `n`, then `f` is also continuous and differentiable up to order `m`. This is essentially saying that if a function is differentiable up to a certain order, it is also differentiable up to any lesser order.
More concisely: If `f` is a continuously differentiable up to order `n` function from the normed additive commutative group `E` to the normed space `πF` over the non-trivially normed field `π`, then `f` is also continuously differentiable up to order `m` for any `m` less than or equal to `n`.
|
iteratedFDerivWithin_univ
theorem iteratedFDerivWithin_univ :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : β}, iteratedFDerivWithin π n f Set.univ = iteratedFDeriv π n f
This theorem states that for any normed field π, normed additive commutative groups E and F, and normed spaces π over E and F, for any function `f` from E to F and any natural number `n`, the `n`-th iterated FrΓ©chet derivative of `f` within the universal set is equal to the `n`-th iterated FrΓ©chet derivative of `f`.
In other words, when taking the `n`-th iterated FrΓ©chet derivative of `f`, there is no difference whether we consider the derivative within the whole space (the universal set) or without any constraint.
More concisely: For any normed field π, normed additive commutative groups E and F, and normed spaces π over E and F, the `n`-th iterated FrΓ©chet derivative of a function `f` from E to F is independent of the choice of the universal set.
|
contDiffOn_of_continuousOn_differentiableOn
theorem contDiffOn_of_continuousOn_differentiableOn :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : ββ},
(β (m : β), βm β€ n β ContinuousOn (fun x => iteratedFDerivWithin π m f s x) s) β
(β (m : β), βm < n β DifferentiableOn π (fun x => iteratedFDerivWithin π m f s x) s) β ContDiffOn π n f s
This theorem, `contDiffOn_of_continuousOn_differentiableOn`, states that for any type `π` which is a non-trivially normed field, types `E` and `F` which are normed additive commutative groups and also normed spaces over `π`, a set `s` of type `E`, a function `f` from `E` to `F`, and an extended natural number `n`, if for every natural number `m`, the `m`-th iterated FrΓ©chet derivative of `f` within the set `s` is continuous on `s` whenever `m` is less than or equal to `n`, and is also differentiable on `s` whenever `m` is strictly less than `n`, then the function `f` is continuously differentiable `n` times on the set `s`. This means the function `f` has well-defined and continuous derivatives up to the `n`-th order within the set `s`.
More concisely: If a function between two normed spaces over a non-trivially normed field is continuously differentiable of order less than or equal to `n` and differentiable of order strictly less than `n` at each point in a set, then it is `n`-times continuously differentiable on that set.
|
HasFTaylorSeriesUpToOn.eq_ftaylor_series_of_uniqueDiffOn
theorem HasFTaylorSeriesUpToOn.eq_ftaylor_series_of_uniqueDiffOn :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ} {p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpToOn n f p s β
β {m : β}, βm β€ n β UniqueDiffOn π s β x β s β p x m = iteratedFDerivWithin π m f s x
This theorem, also known as `HasFTaylorSeriesUpToOn.eq_ftaylor_series_of_uniqueDiffOn`, states that for a given set `s` of elements of type `E` on which a function `f : E β F` has a Taylor series expansion up to a certain order `n`, any choice of `m`-th order iterated differential for `m β€ n` must be the same as the `m`-th order term in the Taylor series expansion of `f`, provided that the set `s` has unique differentiability and the point `x` is in the set `s`. Here, `π` is a non-trivially normed field, `E` and `F` are normed additive commutative groups, and they are also normed spaces over `π`. The Taylor series expansion is represented by `p : E β FormalMultilinearSeries π E F`.
More concisely: For a function `f : E β F` with a unique Taylor series expansion up to order `n` over a set `s` in normed groups `E` and `F` over a non-trivially normed field `π`, the `m`-th order differential (for `m β€ n`) at any point `x` in `s` equals the `m`-th term of the Taylor series expansion.
|
ContDiffOn.continuousOn
theorem ContDiffOn.continuousOn :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : ββ}, ContDiffOn π n f s β ContinuousOn f s
The theorem `ContDiffOn.continuousOn` states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F` (which are also normed spaces over `π`), a set `s` of elements of type `E`, a function `f` from `E` to `F`, and a natural number or infinity `n`, if the function `f` is continuously differentiable `n` times on the set `s`, then the function `f` is also continuous on the set `s`. The terms involved have the usual meanings from the field of analysis and topology.
More concisely: If a function between two normed spaces is continuously differentiable at every point in a set, then it is continuous on that set.
|
HasFTaylorSeriesUpToOn.congr
theorem HasFTaylorSeriesUpToOn.congr :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f fβ : E β F} {n : ββ} {p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpToOn n f p s β (β x β s, fβ x = f x) β HasFTaylorSeriesUpToOn n fβ p s
This theorem states that if two functions, `f` and `fβ`, are equal on a set `s` of elements of type `E` in a nontrivially normed field `π` with normed additive commutative groups `E` and `F` and normed spaces over `π`, then if `f` has a Taylor series up to `n` on `s`, `fβ` also has a Taylor series up to `n` on `s`. Here, `p` is the formal multilinear series generating the Taylor series. Essentially, this theorem is talking about the transferability of Taylor series representation between two functions that are equivalent over a specific set.
More concisely: If two functions from a nontrivially normed field to their respective normed spaces have equal restrictions to a set, and one of them has a Taylor series up to a certain order on that set, then the other function also has a Taylor series of the same order on that set.
|
ContDiffWithinAt.of_insert
theorem ContDiffWithinAt.of_insert :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ} {y : E}, ContDiffWithinAt π n f (insert y s) x β ContDiffWithinAt π n f s x
The theorem `ContDiffWithinAt.of_insert` states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F` which are also normed spaces over `π`, any set `s` of elements of `E`, any function `f` from `E` to `F`, any elements `x` and `y` of `E`, and any natural number or infinity `n`, if `f` is continuously differentiable within the set obtained by adding `y` to `s` at the point `x` at least `n` times, then `f` is also continuously differentiable within `s` at `x` at least `n` times. This theorem is actually just an alias for the forward direction of another theorem, `contDiffWithinAt_insert`.
More concisely: If a function between two normed spaces is continuously differentiable within a set at a point after adding an element, then it is also continuously differentiable at that point within the original set, a given number of times.
|
contDiffOn_univ
theorem contDiffOn_univ :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ}, ContDiffOn π n f Set.univ β ContDiff π n f
The theorem `contDiffOn_univ` states that for any nontrivially normed field `π`, normed additive commutative group `E`, normed space `E` over `π`, normed additive commutative group `F`, and normed space `F` over `π`, a function `f : E β F`, and a natural number `n` or infinity (`ββ`), the function `f` is continuously differentiable of order `n` on the universal set (i.e., the entire domain `E`) if and only if `f` is continuously differentiable of order `n` in general. This theorem essentially says that the condition of being continuously differentiable of a certain order on the entire domain is equivalent to being continuously differentiable of that order without specifying a subset of the domain.
More concisely: The theorem `contDiffOn_univ` in Lean 4 states that a function between two normed spaces is continuously differentiable of order `n` on the entire domain if and only if it is continuously differentiable of order `n` in the general sense.
|
ContDiffAt.congr_of_eventuallyEq
theorem ContDiffAt.congr_of_eventuallyEq :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f fβ : E β F}
{x : E} {n : ββ}, ContDiffAt π n f x β (nhds x).EventuallyEq fβ f β ContDiffAt π n fβ x
This theorem states that if a function `f` is continuously differentiable at a point `x` in a given normed vector space over non-trivially normed field `π`, and if there is another function `fβ` that is equal to `f` in the neighborhood of `x`, then `fβ` is also continuously differentiable at `x`. In other words, the property of being continuously differentiable at a certain point is preserved under changes to the function that are local to that point.
More concisely: If a continuously differentiable function `f` at a point `x` in a normed vector space over a non-trivially normed field is equal to a function `fβ` in a neighborhood of `x`, then `fβ` is also continuously differentiable at `x`.
|
contDiffOn_of_locally_contDiffOn
theorem contDiffOn_of_locally_contDiffOn :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : ββ}, (β x β s, β u, IsOpen u β§ x β u β§ ContDiffOn π n f (s β© u)) β ContDiffOn π n f s
This theorem states that if a function `f` is continuously differentiable to any order `n` in a neighborhood of each point `x` in a set `s`, then the function `f` is continuously differentiable to the order `n` on the entire set `s`. Here, `π` is a non-trivial normed field, `E` and `F` are normed additive commutative groups with `π` as their scalars, `s` is a set in `E`, and `n` is either a natural number or positive infinity, signifying the order of differentiation. The neighborhood of each point `x` in `s` is represented by an open set `u` such that `x` belongs to `u` and `u` intersects with `s`. The existence of such a `u` for each `x` in `s` is a prerequisite of the theorem. Continuous differentiability of `f` to the order `n` in `s β© u` and on `s` is expressed by `ContDiffOn π n f (s β© u)` and `ContDiffOn π n f s`, respectively.
More concisely: If a function `f : E β F` is continuously differentiable to order `n` in the neighborhood of every point in a set `s` β `E`, then `f` is continuously differentiable to order `n` on the entire set `s`.
|
hasFTaylorSeriesUpToOn_succ_iff_left
theorem hasFTaylorSeriesUpToOn_succ_iff_left :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {p : E β FormalMultilinearSeries π E F} {n : β},
HasFTaylorSeriesUpToOn (βn + 1) f p s β
HasFTaylorSeriesUpToOn (βn) f p s β§
(β x β s, HasFDerivWithinAt (fun y => p y n) (p x n.succ).curryLeft s x) β§
ContinuousOn (fun x => p x (n + 1)) s
The theorem `hasFTaylorSeriesUpToOn_succ_iff_left` states the following: Given a nontrivially normed field `π`, a normed additive commutative group `E`, a normed space structure on `E` over `π`, another normed additive commutative group `F`, a normed space structure on `F` over `π`, a set `s` of elements of type `E`, a function `f` from `E` to `F`, a function `p` that assigns to each element of `E` a formal multilinear series over `π`, `E`, and `F`, and a natural number `n`, the function `f` has a Taylor series up to order `n+1` at all points in the set `s` if and only if it has a Taylor series up to order `n` at all points in `s`, and the `(n+1)`-th term of the series is a derivative of the `n`-th term in `s`, and the `(n+1)`-th term of the series is continuous in `s`.
More concisely: Given a nontrivially normed field π, normed groups E and F with normed space structures, a set s of points in E, a function f from E to F with Taylor series up to order n on s, and a continuous (n+1)-th term, then f has a Taylor series up to order n+1 on s if and only if its (n+1)-th term is the derivative of the n-th term.
|
ContDiff.contDiffWithinAt
theorem ContDiff.contDiffWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ}, ContDiff π n f β ContDiffWithinAt π n f s x
This theorem states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F` (over `π`), a set `s` of `E`, a function `f` from `E` to `F`, a point `x` in `E`, and a number `n` (which could be a natural number or infinity), if the function `f` is continuously differentiable `n` times over the entire domain, then it's also continuously differentiable `n` times within the set `s` at the point `x`.
More concisely: If `f` is a continuously differentiable function of order `n` on the entire normed additive commutative group `E` over the non-trivially normed field `π`, then `f` is continuously differentiable of order `n` at every point `x` in any subset `s` of `E`.
|
Mathlib.Analysis.Calculus.ContDiff.Defs._auxLemma.23
theorem Mathlib.Analysis.Calculus.ContDiff.Defs._auxLemma.23 :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ}, ContDiff π n f = ContDiffOn π n f Set.univ
The theorem `Mathlib.Analysis.Calculus.ContDiff.Defs._auxLemma.23` states that for any nontrivially normed field `π`, normed add commutative group `E` and `F` with a normed space structure over `π`, and any function `f` from `E` to `F`, the function `f` being continuously differentiable of any order `n` (denoted as `ContDiff π n f`) is equivalent to the function `f` being continuously differentiable of order `n` on the universal set of `E` (denoted as `ContDiffOn π n f Set.univ`). The universal set in this context contains all elements of the type `E`. This implies that the property of being continuously differentiable of a particular order is a global property, i.e., it holds everywhere in the domain of the function.
More concisely: For any nontrivially normed field `π`, normed add commutative groups `E` and `F`, and continuously differentiable function `f` of order `n` from `E` to `F`, `ContDiff π n f` if and only if `ContDiffOn π n f Set.univ`.
|
ContDiffWithinAt.continuousWithinAt
theorem ContDiffWithinAt.continuousWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ}, ContDiffWithinAt π n f s x β ContinuousWithinAt f s x
This theorem states that for any nontrivially normed field `π` and normed additive commutative groups `E` and `F` that are also normed spaces over the field `π`, given a function `f` from `E` to `F`, a set `s` of `E`, a point `x` in `E`, and a natural number or infinity `n`, if the function `f` is continuously differentiable within the set `s` at the point `x` to the degree `n`, then the function `f` is also continuous at the point `x` within the set `s`. In other words, continuous differentiability within a set at a point implies continuity within the set at that point.
More concisely: If a continuously differentiable function between two normed spaces is given over a set in a nontrivially normed field, then it is continuous at any point within that set.
|
contDiffWithinAt_succ_iff_hasFDerivWithinAt'
theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt' :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : β},
ContDiffWithinAt π (β(n + 1)) f s x β
β u β nhdsWithin x (insert x s),
u β insert x s β§ β f', (β x β u, HasFDerivWithinAt f (f' x) s x) β§ ContDiffWithinAt π (βn) f' s x
This theorem states that for a function `f` from a normed vector space `E` to another normed vector space `F` over a nontrivially normed field `π`, the function is continuously differentiable of order `(n + 1)` within a set `s` at a point `x` if and only if there exists a neighborhood `u` within the set `s` (including `x`) of our point `x` such that:
1. `u` is a subset of the set `s` (including `x`),
2. There exists a function `f'` such that for all `x` in `u`, `f'` is the derivative of `f` within `s` at `x`,
3. This function `f'` is continuously differentiable of order `n` within `s` at `x`.
In other words, the theorem provides a condition for a function to be continuously differentiable of a certain order within a specific set, in terms of the existence of a derivative function that is continuously differentiable of one order less within the same set.
More concisely: A function `f` from a normed vector space `E` to another normed vector space `F` over a nontrivially normed field is continuously differentiable of order `(n + 1)` at a point `x` in a set `s` if and only if there exists a neighborhood `u` of `x` in `s` such that both `f` and its derivative `f'` within `s` at `x` are continuously differentiable of orders `n` and `n-1`, respectively.
|
contDiff_iff_contDiffAt
theorem contDiff_iff_contDiffAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ}, ContDiff π n f β β (x : E), ContDiffAt π n f x
This theorem states that a function `f` from a normed add commutative group `E` to another normed add commutative group `F`, both over a nontrivially normed field `π`, is continuously differentiable up to order `n` everywhere if and only if it is continuously differentiable up to order `n` at every point `x` in `E`. This result essentially means that global and pointwise continuous differentiability are equivalent for such functions.
More concisely: A function `f` from a normed add commutative group `E` to another normed add commutative group `F` over a nontrivially normed field `π` is continuously differentiable up to order `n` everywhere if and only if it is continuously differentiable up to order `n` at every point `x` in `E`.
|
contDiff_zero
theorem contDiff_zero :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F},
ContDiff π 0 f β Continuous f
This theorem, `contDiff_zero`, states that for all normed additive commutative groups `E` and `F`, over a non-trivially normed field `π`, and a function `f` mapping from `E` to `F`, the function `f` is continuously differentiable of order 0 if and only if `f` is a continuous function. The notation `ContDiff π 0 f` refers to the function `f` being continuously differentiable of order 0, while `Continuous f` refers to `f` being a continuous function.
More concisely: A function `f` from a normed additive commutative group `E` to another normed additive commutative group `F` over a non-trivially normed field is continuously differentiable of order 0 if and only if it is continuous.
|
ContDiffWithinAt.insert'
theorem ContDiffWithinAt.insert' :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ} {y : E}, ContDiffWithinAt π n f s x β ContDiffWithinAt π n f (insert y s) x
The theorem `ContDiffWithinAt.insert'` states that for any nontrivially normed field `π`, and any normed additive commutative group `E` and `F` which are also normed spaces over `π`, given a set `s` of elements of type `E`, a function `f` mapping `E` to `F`, an element `x` of `E`, a natural number `n` or infinity, and another element `y` of `E`, if the function `f` is continuously differentiable within the set `s` at the point `x` up to order `n`, then the function `f` is also continuously differentiable within the set obtained by inserting the element `y` into `s` at the point `x` up to the same order `n`.
More concisely: If a function is continuously differentiable up to order n at a point x in the set s of a normed space, then it remains continuously differentiable up to the same order at x in the set obtained by inserting an element y into s.
|
contDiffWithinAt_succ_iff_hasFDerivWithinAt
theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : β},
ContDiffWithinAt π (β(n + 1)) f s x β
β u β nhdsWithin x (insert x s),
β f', (β x β u, HasFDerivWithinAt f (f' x) u x) β§ ContDiffWithinAt π (βn) f' u x
The theorem `contDiffWithinAt_succ_iff_hasFDerivWithinAt` states that for any nontrivially normed field `π`, any normed additive commutative group `E` and `F` (which are both normed spaces over `π`), a set `s` of elements from `E`, a function `f` from `E` to `F`, an element `x` of `E`, and a natural number `n`, the function `f` is continuously differentiable within the set `s` at the point `x` to the degree `(n + 1)` if and only if there exists a set `u` in the neighborhood within `s` of `x`, such that there exists a function `f'`, for which every element in `u` has a FrΓ©chet derivative within `u` at that point, and the function `f'` is continuously differentiable within `u` at the degree `n`.
More concisely: A function between two normed spaces is continuously differentiable within a set to degree (n+1) if and only if there exists a smaller set where every element has a FrΓ©chet derivative and the derivative function is continuously differentiable to degree n.
|
ContDiff.contDiffOn
theorem ContDiff.contDiffOn :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : ββ}, ContDiff π n f β ContDiffOn π n f s
This theorem states that for any nontrivial normed field π, normed additive commutative groups E and F, and a set s of elements from E, if a function f from E to F is continuously differentiable up to an order n in the whole domain, then it is also continuously differentiable up to the same order on the subset s of its domain. The order of differentiation can be any natural number or infinity. The implication holds regardless of the specific types of the normed field and the normed additive commutative groups.
More concisely: For any nontrivial normed field π, if a continuously differentiable up to order n function f : E β F between Banach spaces E and F remains so when restricted to any subset s of its domain, where E and F are normed additive commutative groups.
|
ContDiffOn.congr
theorem ContDiffOn.congr :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f fβ : E β F} {n : ββ}, ContDiffOn π n f s β (β x β s, fβ x = f x) β ContDiffOn π n fβ s
The theorem `ContDiffOn.congr` states that for any non-trivially normed field `π`, normed additive commutative group `E`, and `F`, where `E` and `F` are normed spaces over `π`, if a function `f` from `E` to `F` is continuously differentiable on a set `s` of `E` up to a certain order `n`, and there exists another function `fβ` which is equal to `f` for all elements in the set `s`, then `fβ` is also continuously differentiable on `s` up to the same order `n`.
More concisely: If `f` is continuously differentiable of order `n` on `s` in `E` to `F`, and there exists `fβ` equal to `f` on `s`, then `fβ` is also continuously differentiable of order `n` on `s`.
|
ContDiffWithinAt.differentiableWithinAt
theorem ContDiffWithinAt.differentiableWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ}, ContDiffWithinAt π n f s x β 1 β€ n β DifferentiableWithinAt π f s x
This theorem states that for any nontrivially normed field `π`, normed additive commutative group `E` and `F`, and a function `f` from `E` to `F`, if the function `f` is continuously differentiable within a set `s` at a point `x` up to any order `n` that is greater than or equal to 1, then `f` is differentiable at the point `x` within the set `s`. This means that the function `f` admits a derivative at `x`, which may not be unique.
More concisely: If a continuously differentiable function `f` from a normed additive commutative group `E` to another normed additive commutitative group `F`, over a nontrivially normed field, is differentiable up to order `n` (`n >= 1`) at a point `x` within a set `s`, then `f` is differentiable at `x` within `s`.
|
ContDiffWithinAt.differentiable_within_at'
theorem ContDiffWithinAt.differentiable_within_at' :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ}, ContDiffWithinAt π n f s x β 1 β€ n β DifferentiableWithinAt π f (insert x s) x
This theorem states that if a function is continuously differentiable `n` times within a set at a specific point, with `n` being greater than or equal to 1, then the function is differentiable within that set at that point. Here, continuous differentiability `n` times (denoted as `C^n`) implies that the function and its first `n` derivatives are continuous. The function can be of any type mapping from a normed additive commutative group `E` to another normed additive commutative group `F`, both of which are vector spaces over a non-trivially normed field `π`. The set is a subset of the domain `E` and the point is an element of `E`.
More concisely: If a function is `C^n` differentiable at a point in a normed additive commutative groups, then it is differentiable at that point.
|
iteratedFDerivWithin_inter'
theorem iteratedFDerivWithin_inter' :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s u : Set E}
{f : E β F} {x : E} {n : β},
u β nhdsWithin x s β iteratedFDerivWithin π n f (s β© u) x = iteratedFDerivWithin π n f s x
This theorem, "iteratedFDerivWithin_inter'", states that for any non-trivially normed field `π`, normed additive commutative group `E`, normed space of `π` over `E`, normed additive commutative group `F`, normed space of `π` over `F`, sets `s` and `u` of type `E`, function `f` from `E` to `F`, a point `x` of `E` and a natural number `n`, if `u` is in the neighborhood within `s` at `x` (where the elements of this neighborhood are sets that contain the intersection of `s` and a neighborhood of `x`), then the `n`th iterated Frechet derivative of `f` within the intersection of `s` and `u` at `x` is equal to the `n`th iterated Frechet derivative of `f` within `s` at `x`. In simpler terms, the iterated derivative at a point within a set does not change if we further restrict the set to a neighborhood of the point.
More concisely: For any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, normed spaces of `π` over `E` and `F` respectively, set `s` in `E`, function `f` from `E` to `F`, point `x` in `E`, and natural number `n`, if `u` is in the neighborhood of `s` at `x`, then the `n`th iterated Frechet derivative of `f` within the intersection of `s` and `u` at `x` equals the `n`th iterated Frechet derivative of `f` within `s` at `x`.
|
hasFTaylorSeriesUpTo_succ_iff_right
theorem hasFTaylorSeriesUpTo_succ_iff_right :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{p : E β FormalMultilinearSeries π E F} {n : β},
HasFTaylorSeriesUpTo (β(n + 1)) f p β
(β (x : E), (p x 0).uncurry0 = f x) β§
(β (x : E), HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x) β§
HasFTaylorSeriesUpTo (βn) (fun x => (continuousMultilinearCurryFin1 π E F) (p x 1)) fun x => (p x).shift
The theorem `hasFTaylorSeriesUpTo_succ_iff_right` states that for any nontrivially normed field `π`, normed add commutative group `E` and `F` with a normed space structure over `π`, a function `f : E β F`, a formal multilinear series `p : E β FormalMultilinearSeries π E F`, and a natural number `n`, `p` is a Taylor series of `f` up to `n+1` if and only if the following conditions hold:
- For all `x` in `E`, the `0`-th term of the series `p` at `x` is equal to `f(x)`.
- For all `x` in `E`, the function that maps `y` to the `0`-th term of `p` at `y` has a derivative at `x` that is the `1`-st term of `p` at `x`.
- `p.shift` is a Taylor series up to `n` for the function that maps `x` to the `1`-th term of `p` at `x` (after suitable currying).
In simpler terms, a series is a Taylor series for a function up to a certain order if and only if its terms match the function's derivatives at each order, and the series obtained by shifting all terms one place to the right is a Taylor series for the derivative of the function, up to one order less.
More concisely: A formal multilinear series over a nontrivially normed field is a Taylor series up to a given order for a function if and only if its first term matches the function value, its derivatives up to that order match the function's derivatives at each point, and the shifted series is a Taylor series up to the preceding order for the derivative function.
|
Filter.EventuallyEq.iteratedFDerivWithin_eq
theorem Filter.EventuallyEq.iteratedFDerivWithin_eq :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f fβ : E β F} {x : E},
(nhdsWithin x s).EventuallyEq fβ f β
fβ x = f x β β (n : β), iteratedFDerivWithin π n fβ s x = iteratedFDerivWithin π n f s x
The given theorem states that, for any nontrivially normed field `π`, normed add-commutative group `E`, normed space of `π` over `E`, normed add-commutative group `F`, normed space of `π` over `F`, set `s` of `E`, two functions `f` and `fβ` from `E` to `F`, and any element `x` of `E`, if the two functions `fβ` and `f` coincide at `x` and within a neighborhood of `x` in the set `s`, then for any natural number `n`, the `n`-th iterated FrΓ©chet derivative of `fβ` at `x` within the set `s` is equal to the `n`-th iterated FrΓ©chet derivative of `f` at `x` within the same set. In simpler terms, it says that if two functions agree closely around a point and at the point itself, their `n`-th derivatives at that point also agree.
More concisely: If `f` and `fβ` are two normed functionals on a normed vector space `E` over a nontrivially normed field `π`, coinciding at a point `x` and in a neighborhood of `x` within a set `s`, then their `n`-th iterated FrΓ©chet derivatives at `x` within `s` are equal.
|
ContDiffWithinAt.congr
theorem ContDiffWithinAt.congr :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f fβ : E β F} {x : E} {n : ββ},
ContDiffWithinAt π n f s x β (β y β s, fβ y = f y) β fβ x = f x β ContDiffWithinAt π n fβ s x
This theorem states that, given a nontrivially normed field `π` and normed additive commutative groups `E` and `F` that are also normed spaces over `π`, for any set `s` of elements of type `E`, two functions `f` and `fβ` from `E` to `F`, a point `x` in `E`, and a natural number `n` or infinity, if the function `f` is continuously differentiable within the set `s` at the point `x` of order `n`, and for all points `y` in `s`, `fβ` at `y` is equal to `f` at `y`, and `fβ` at `x` is equal to `f` at `x`, then the function `fβ` is also continuously differentiable within the set `s` at the point `x` of order `n`. In other words, if two functions coincide on a set and at a particular point, and one of the functions is continuously differentiable at that point within the set, then the other function is also continuously differentiable at that point within the set.
More concisely: If two continuously differentiable functions of order `n` agree on a set `s` and at a point `x`, then they are equal in continuity and differentiability of order `n` at `x` within `s`.
|
HasFTaylorSeriesUpTo.contDiff
theorem HasFTaylorSeriesUpTo.contDiff :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ} {f' : E β FormalMultilinearSeries π E F}, HasFTaylorSeriesUpTo n f f' β ContDiff π n f
This theorem states that if a function `f` with domain `E` and codomain `F` has a Taylor series up to `n` (represented by `f'`), then `f` is `n` times continuously differentiable. Here, `π` is the underlying field which is assumed to be a non-trivially normed field, `E` and `F` are normed additive commutative groups with a normed space structure over `π`. The Taylor series is formalized as a multilinear series.
More concisely: If a function `f : E β F` over a non-trivially normed field `π` has a multilinear series representation `f'` up to order `n`, then `f` is `n` times continuously differentiable.
|
HasFTaylorSeriesUpTo.hasFDerivAt
theorem HasFTaylorSeriesUpTo.hasFDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ} {p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpTo n f p β
1 β€ n β β (x : E), HasFDerivAt f ((continuousMultilinearCurryFin1 π E F) (p x 1)) x
This theorem states that if a function has a Taylor series of at least order 1, then the term of order 1 in this series is a derivative of the function.
More specifically, for a function `f` mapping from a normed vector space `E` over a non-trivially normed field `π` to another normed vector space `F`, if `f` has a Taylor series `p` up to at least order 1, then at any point `x` in `E`, the function `f` has a derivative at `x` which matches the order 1 term of the Taylor series at `x`, after it is uncurried using `continuousMultilinearCurryFin1`.
More concisely: If a function `f` has a Taylor series of order 1 or higher, then the order 1 term of its Taylor series at a point `x` is equal to the derivative of `f` at `x`.
|
ContDiff.contDiffAt
theorem ContDiff.contDiffAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} {n : ββ}, ContDiff π n f β ContDiffAt π n f x
This theorem states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, and a function `f` mapping from `E` to `F`, if `f` is continuously differentiable up to order `n` (where `n` can be any natural number or infinity), then `f` is also continuously differentiable at a specific point `x` in `E`. This holds for all such `x` in `E`.
More concisely: If `f` is continuously differentiable up to order `n` on a non-trivially normed field `π` from normed additive commutative groups `E` to `F`, then `f` is continuously differentiable at every point `x` in `E`.
|
Set.EqOn.iteratedFDerivWithin
theorem Set.EqOn.iteratedFDerivWithin :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f fβ : E β F},
Set.EqOn fβ f s β β (n : β), Set.EqOn (iteratedFDerivWithin π n fβ s) (iteratedFDerivWithin π n f s) s
This theorem states that if two functions, namely `f` and `fβ`, are equal on a set `s` in a normed space over a non-trivially normed field `π`, then their iterated differentials (derivatives), as represented by `iteratedFDerivWithin`, are also equal on that same set `s` for any natural number `n`. This equivalently implies that if `f` and `fβ` coincide on the elements of `s`, their `n`-th derivatives also coincide on `s` for any `n`.
More concisely: If `f` and `fβ` are equal on a set `s` in a normed space over a non-trivially normed field, then their `n`-th iterated differentials `iteratedFDerivWithin f n x` and `iteratedFDerivWithin fβ n x` are equal for all `x β s` and `n β β`.
|
HasFTaylorSeriesUpToOn.hasFDerivAt
theorem HasFTaylorSeriesUpToOn.hasFDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ} {p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpToOn n f p s β
1 β€ n β s β nhds x β HasFDerivAt f ((continuousMultilinearCurryFin1 π E F) (p x 1)) x
The theorem `HasFTaylorSeriesUpToOn.hasFDerivAt` states that if a function `f` from a normed space `E` over a nontrivially normed field `π` to another normed space `F` over the same field has a Taylor series of order at least `1` in a neighborhood `s` of a point `x` in `E`, then the term of order `1` of this series is a derivative of `f` at `x`. In other words, if the function `f` can be expressed as a Taylor series in the neighborhood of `x`, then the first order term of this Taylor series describes the change in `f` near `x`, which is the derivative of `f` at `x`.
More concisely: If a function `f` from a normed space to another normed space has a Taylor series expansion in a neighborhood of a point `x` with a nonzero first order term, then the first order term is equal to the derivative of `f` at `x`.
|
ContDiff.continuous_iteratedFDeriv
theorem ContDiff.continuous_iteratedFDeriv :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ} {m : β}, βm β€ n β ContDiff π n f β Continuous fun x => iteratedFDeriv π m f x
This theorem states that for a function `f` that is `C^n` (i.e., the function `f` is n-times continuously differentiable), its `m`-times iterated derivative is continuous if `m` is less than or equal to `n`. This applies in the context of a nontrivially normed field `π`, and normed add commutative groups `E` and `F` that are normed spaces over `π`, with the function `f` mapping from `E` to `F`.
More concisely: If `f` is a `C^n` function from a normed space `E` to a normed space `F` over a nontrivially normed field `π`, then for `m` less than or equal to `n`, the `m`-th iterated derivative of `f` is a continuous function.
|
ContDiff.continuous_fderiv_apply
theorem ContDiff.continuous_fderiv_apply :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ}, ContDiff π n f β 1 β€ n β Continuous fun p => (fderiv π f p.1) p.2
The theorem `ContDiff.continuous_fderiv_apply` states that for a function f mapping from a normed space E to another normed space F, both over a nontrivially normed field π, if this function f is at least continuously differentiable (`C^1`), then its derivative function (which takes a pair consisting of a point and a vector, `(x, v)`, and maps it to the derivative of f at `x` applied to `v`) is continuous. Here, `fderiv π f` represents the derivative function of f. The continuity of the derivative applies when the degree of differentiability of the function f, denoted by `n`, is equal to or greater than 1.
More concisely: If `f` is a continuously differentiable function from a normed space `E` to another normed space `F` over a nontrivially normed field, then its derivative function `fderiv π f` is continuous.
|
contDiffOn_top
theorem contDiffOn_top :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F}, ContDiffOn π β€ f s β β (n : β), ContDiffOn π (βn) f s
The theorem `contDiffOn_top` states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, normed spaces over `π` of `E` and `F`, a set `s` of elements of type `E`, and a function `f` from `E` to `F`, the function `f` is continuously differentiable on the set `s` at all orders if and only if the function `f` is continuously differentiable on the set `s` at each natural number order.
More concisely: A function between two normed spaces is continuously differentiable on a set at all orders if and only if it is continuously differentiable at each natural number order on that set.
|
HasFTaylorSeriesUpToOn.of_le
theorem HasFTaylorSeriesUpToOn.of_le :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {m n : ββ} {p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpToOn n f p s β m β€ n β HasFTaylorSeriesUpToOn m f p s
This theorem, titled `HasFTaylorSeriesUpToOn.of_le`, states that for any nontrivially normed field `π`, normed additive commutative group `E`, normed space over `π` with base `E`, normed additive commutative group `F`, normed space over `π` with base `F`, set `s` of elements of type `E`, function `f` from `E` to `F`, and formal multilinear series `p` in variables of type `E` with coefficients in `F`, if `f` has a Taylor series up to a certain order `n` in the set `s`, then `f` also has a Taylor series up to any order `m` that is less than or equal to `n` in the set `s`. This is essentially saying that if a function has a Taylor series expansion up to a high order, it also has a Taylor series expansion up to any lower order.
More concisely: If a function has a Taylor series expansion up to order n in a set, it also has a Taylor series expansion up to any order less than or equal to n in that set.
|
iteratedFDerivWithin_congr
theorem iteratedFDerivWithin_congr :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f fβ : E β F} {x : E},
Set.EqOn fβ f s β x β s β β (n : β), iteratedFDerivWithin π n fβ s x = iteratedFDerivWithin π n f s x
This theorem, `iteratedFDerivWithin_congr`, states that if two functions `fβ` and `f` are equal on a set `s`, then their `n`-th iterated differentials within this set also coincide. More formally, for all elements `x` in `s` and for all natural numbers `n`, the `n`-th iterated differential of `fβ` at `x` within `s` is equal to the `n`-th iterated differential of `f` at `x` within `s`. This holds in the context where the types `π`, `E`, and `F` are endowed with the structures of a non-trivially normed field and normed commutative additive groups respectively, and where `E` and `F` are vector spaces over `π`.
More concisely: For functions `fβ` and `f` equal on set `s`, their `n`-th iterated differentials within `s` coincide, given that `π`, `E`, and `F` are non-trivially normed fields with `E` and `F` as vector spaces over `π`.
|
contDiff_top_iff_fderiv
theorem contDiff_top_iff_fderiv :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F},
ContDiff π β€ f β Differentiable π f β§ ContDiff π β€ fun y => fderiv π f y
The theorem `contDiff_top_iff_fderiv` states that a function `f` is infinitely continuously differentiable (denoted as `C^β`) if and only if it is differentiable and its derivative, as formulated through the `fderiv` function, is also infinitely continuously differentiable.
Here, `C^β` means the function is differentiable and all its derivatives are also differentiable. The function `f` is from a normed vector space `E` over a nontrivial normed field `π` to another normed vector space `F` over `π`. The derivative of `f` at a point `x` in `E`, given by `fderiv π f x`, is a continuous linear map from `E` to `F`.
More concisely: A function `f` from a normed vector space `E` to another normed vector space `F` is infinitely continuously differentiable if and only if it is differentiable and its derivative, as a continuous linear map, is infinitely differentiable.
|
hasFTaylorSeriesUpTo_top_iff'
theorem hasFTaylorSeriesUpTo_top_iff' :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpTo β€ f p β
(β (x : E), (p x 0).uncurry0 = f x) β§
β (m : β) (x : E), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x
The theorem `hasFTaylorSeriesUpTo_top_iff'` states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, and normed spaces over `π` for `E` and `F`, a function `f` from `E` to `F` has a Taylor series up to infinity if and only if the following conditions are met: (1) For every `x` in `E`, the uncurried zeroth term of the formal multilinear series `p` at `x` is equal to `f x`, and (2) for every natural number `m` and every `x` in `E`, the function `y` mapped to the `m`th term of the series `p` at `y` has a derivative at `x` that is equal to the left-curried `m+1`th term of the series `p` at `x`. In other words, the function `f` can be represented as an infinite Taylor series `p` if and only if each term in the series `p` either represents the function `f` at `x` or is the derivative of the preceding term in the series.
More concisely: A function from a normed additive commutative group to another normed space over a nontrivially normed field has a Taylor series up to infinity if and only if its uncurried zeroth term at each point is equal to the function value, and each term is the derivative of the preceding term at that point.
|
ContDiffWithinAt.mono_of_mem
theorem ContDiffWithinAt.mono_of_mem :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ},
ContDiffWithinAt π n f s x β β {t : Set E}, s β nhdsWithin x t β ContDiffWithinAt π n f t x
This theorem states that for a non-trivially normed field 'π', two normed vector spaces E and F over 'π', a function 'f' from E to F, a set 's' of elements from E, a point 'x' in E, and a natural number or infinity 'n', if the function 'f' is continuously differentiable 'n' times within the set 's' at the point 'x', then for any other set 't' such that 's' is in the neighborhood of 'x' within 't', the function 'f' is also continuously differentiable 'n' times within the set 't' at the point 'x'. Essentially, if 'f' is continuously differentiable in a neighborhood of 'x', it remains continuously differentiable when the neighborhood is expanded, provided the original set is still close to 'x'.
More concisely: If a continuously differentiable 'n' times function 'f' from one normed vector space to another over a non-trivially normed field has a neighborhood 's' of point 'x' where it is continuously differentiable 'n' times, then 'f' is continuously differentiable 'n' times at 'x' in any larger neighborhood 't' containing 's'.
|
hasFTaylorSeriesUpToOn_top_iff'
theorem hasFTaylorSeriesUpToOn_top_iff' :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpToOn β€ f p s β
(β x β s, (p x 0).uncurry0 = f x) β§
β (m : β), β x β s, HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft s x
This theorem states that, for any given types `π`, `E`, and `F` where `π` is a non-trivially normed field, `E` is a normed additive commutative group and also a normed space over `π`, and `F` is a normed additive commutative group and also a normed space over `π`, and given a set `s` of elements of type `E`, a function `f` from `E` to `F`, and a function `p` which assigns to each element of `E` a formal multilinear series over `π`, `E`, and `F`, it is the case that `f` has a Taylor series up to infinity on `s` if and only if for every `x` in `s`, the zeroth term of the multilinear series `p x` evaluated at zero is equal to `f x`, and for every natural number `m`, for every `x` in `s`, the `m`-th derivative within `s` at `x` of the function which assigns to `y` the `m`-th term of `p y` exists and is equal to the left currying of the `(m+1)`-th term of `p x`.
More concisely: Given a non-trivially normed field `π`, normed additive commutative groups and normed spaces `E` and `F` over `π`, a set `s` of elements in `E`, a function `f` from `E` to `F`, and a multilinear series `p`, `f` has a Taylor series up to infinity on `s` if and only if for all `x` in `s`, `p x` reduces to `f x` at order 0 and the `m`-th derivative of the function `y => p y` exists and equals the left currying of the `(m+1)`-th term of `p x` for all `x` in `s` and all `m` in `β`.
|
iteratedFDerivWithin_of_isOpen
theorem iteratedFDerivWithin_of_isOpen :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} (n : β), IsOpen s β Set.EqOn (iteratedFDerivWithin π n f s) (iteratedFDeriv π n f) s
This theorem states that in an open set of a topological space, the iterated derivative of a function within this set is identical to the global iterated derivative of the function. More formally, given a non-trivial normed field `π`, normed add commutative groups `E` and `F` which are also normed spaces over `π`, a set `s` in `E`, and a function `f` from `E` to `F`, for any natural number `n`, if the set `s` is open, the `n`-th iterated derivative of `f` within `s` is the same as the `n`-th iterated derivative of `f` on all of `s`.
More concisely: In an open subset of a normed space, the `n`-th iterated derivative of a function is equal to its global `n`-th iterated derivative for any natural number `n`.
|
contDiff_iff_ftaylorSeries
theorem contDiff_iff_ftaylorSeries :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ}, ContDiff π n f β HasFTaylorSeriesUpTo n f (ftaylorSeries π f)
The theorem `contDiff_iff_ftaylorSeries` states that for any non-trivially normed field π, normed additively commutative groups E and F, a function `f` mapping E to F, and an extended natural number `n`, a function `f` is continuously differentiable up to order `n` if and only if `f` has a formal Taylor series up to order `n`. This formal Taylor series is given by the function `ftaylorSeries π f`, which associates a formal Taylor series with every function operating on the normed space.
More concisely: A function from a non-trivially normed field-valued, additively commutative group to another such group is continuously differentiable up to order n if and only if it has a formal Taylor series of order n.
|
contDiff_succ_iff_fderiv
theorem contDiff_succ_iff_fderiv :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : β}, ContDiff π (β(n + 1)) f β Differentiable π f β§ ContDiff π βn fun y => fderiv π f y
The theorem `contDiff_succ_iff_fderiv` states that for all fields `π` with a topology and a norm, and for all normed additive commutative group `E` over `π`, and all normed additive commutative group `F` over `π`, and for all function `f` from `E` to `F`, and all natural numbers `n`, a function `f` is `π`-continuously differentiable for the `n + 1` times if and only if `f` is differentiable and its derivative (expressed with `fderiv`) is `π`-continuously differentiable `n` times. In terms of analysis, this theorem connects the continuous differentiability of a function and its derivative.
More concisely: A function between two normed spaces is `n` times continuously differentiable if and only if it is differentiable and its derivative is also `(n-1)` times continuously differentiable.
|
ContDiffAt.contDiffWithinAt
theorem ContDiffAt.contDiffWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ}, ContDiffAt π n f x β ContDiffWithinAt π n f s x
This theorem states that if a function `f`, which maps elements from a normed additive commutative group `E` to a normed additive commutative group `F` over a nontrivially normed field `π`, is continuously differentiable at a point `x` in `E` at a certain degree `n` (which can be a natural number or infinity), then the function `f` is also continuously differentiable within any set `s` of `E` at the same point `x` and at the same degree `n`.
More concisely: If a continuously differentiable function `f` of degree `n` from a normed additive commutative group `E` to another normed additive commutative group `F` over a nontrivially normed field is differentiable at a point `x` in `E`, then `f` is differentiable at `x` within any set `s` of `E`.
|
ContDiffWithinAt.contDiffAt
theorem ContDiffWithinAt.contDiffAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ}, ContDiffWithinAt π n f s x β s β nhds x β ContDiffAt π n f x
The theorem `ContDiffWithinAt.contDiffAt` states that for a given nontrivially normed field `π`, a normed additive commutative group `E`, a normed space over `π` and `E`, another normed additive commutative group `F`, and a normed space over `π` and `F`, if a function `f` from `E` to `F` is continuously differentiable within a set `s` at a point `x` for a given smoothness degree `n`, and if the set `s` is a neighborhood of `x` (that is, it contains an open set around `x`), then the function `f` is also continuously differentiable at that point `x`. The smoothness degree `n` can be a natural number or infinity (`ββ`). This theorem links the concept of continuous differentiability within a neighborhood of a point and at the point itself.
More concisely: If a function between two normed spaces is continuously differentiable within a neighborhood of a point with some smoothness degree, then it is continuously differentiable at that point.
|
contDiff_succ_iff_hasFDerivAt
theorem contDiff_succ_iff_hasFDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : β}, ContDiff π (β(n + 1)) f β β f', ContDiff π (βn) f' β§ β (x : E), HasFDerivAt f (f' x) x
The theorem `contDiff_succ_iff_hasFDerivAt` states that for any function `f` mapping from a normed vector space `E` to another normed vector space `F`, both over a non-trivially normed field `π`, and any natural number `n`, the function `f` is `C^(n+1)` continuously differentiable if and only if there exists a function `f'` which is `C^n` continuously differentiable and at every point `x` in `E`, `f'` at `x` is the derivative of `f` at `x`. In mathematical terms, a function is `(n+1)` times continuously differentiable if and only if it has an `n` times continuously differentiable derivative.
More concisely: A function `f` from a normed vector space `E` to another normed vector space `F` over a non-trivially normed field is `C^{n+1}` continuously differentiable if and only if there exists a `C^n` continuously differentiable function `f'` such that `f'` is the derivative of `f` at every point in `E`.
|
contDiffOn_congr
theorem contDiffOn_congr :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f fβ : E β F} {n : ββ}, (β x β s, fβ x = f x) β (ContDiffOn π n fβ s β ContDiffOn π n f s)
This theorem states that for any nontrivial normed field `π`, normed additive commutative group `E`, normed space over `π` for `E`, another normed additive commutative group `F`, and another normed space over `π` for `F`, given a set `s` of elements of type `E`, two functions `f` and `fβ` from `E` to `F`, and any `n` in ββ (which represents either a natural number or infinity), if for every element `x` in set `s`, `fβ x` equals `f x`, then the function `fβ` is continuously differentiable on set `s` to order `n` if and only if the function `f` is continuously differentiable on set `s` to order `n`. In simpler terms, if two functions agree on a set, their continuous differentiability on that set is also the same.
More concisely: If two functions agree on a set in a normed vector space, then they have the same continuous differentiability order on that set.
|
contDiffOn_top_iff_fderivWithin
theorem contDiffOn_top_iff_fderivWithin :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F},
UniqueDiffOn π s β
(ContDiffOn π β€ f s β DifferentiableOn π f s β§ ContDiffOn π β€ (fun y => fderivWithin π f s y) s)
This theorem states that for a function `f` mapping from a normed space `E` over a non-trivially normed field `π` to another normed space `F`, it is infinitely continuously differentiable (`C^β`) within a set `s` in `E` if and only if two conditions are met: the function is differentiable within `s` and its derivative function (expressed using `fderivWithin`) is also infinitely continuously differentiable within `s`, provided `s` has unique derivatives. This is true for all `π`, `E`, `F`, `s`, and `f` that meet the prerequisites.
More concisely: A function `f` from a normed space `E` to another normed space `F` over a non-trivially normed field is infinitely continuously differentiable within a set `s` if and only if it is differentiable there and its derivative `f'` is also infinitely continuously differentiable within `s`, given that `s` has unique derivatives.
|
ContDiffOn.ftaylorSeriesWithin
theorem ContDiffOn.ftaylorSeriesWithin :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : ββ},
ContDiffOn π n f s β UniqueDiffOn π s β HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin π f s) s
This theorem states that for a function `f` that is continuously differentiable up to order `n` within a set `s` of unique differentiability, the function admits the formal Taylor series `ftaylorSeriesWithin π f s` up to order `n` in `s`. Here, `π` is a normed field, `E` and `F` are normed additive commutative groups over `π`, and `n` can be any natural number or infinity. The theorem therefore provides a relationship between the notions of differentiability and the existence of a Taylor series for a function within a particular set.
More concisely: For a continuously differentiable up to order n function f from a normed additive commutative group E into another normed additive commutative group F over a normed field π, there exists a formal Taylor series ftaylorSeriesWithin π f s up to order n in the set s of unique differentiability.
|
contDiffOn_succ_iff_fderivWithin
theorem contDiffOn_succ_iff_fderivWithin :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : β},
UniqueDiffOn π s β
(ContDiffOn π (β(n + 1)) f s β DifferentiableOn π f s β§ ContDiffOn π (βn) (fun y => fderivWithin π f s y) s)
The theorem `contDiffOn_succ_iff_fderivWithin` states that for any normed field `π`, normed add commutative groups `E` and `F` with `π` as their scalar field, a set `s` of elements of type `E`, a function `f` from `E` to `F`, and a natural number `n`, if the set `s` has a unique derivative at each of its points (`UniqueDiffOn π s`), then the function `f` is continuously differentiable to order `(n + 1)` on the set `s` (expressed as `ContDiffOn π (β(n + 1)) f s`) if and only if `f` is differentiable on `s` (`DifferentiableOn π f s`) and the derivative of `f` within `s` (expressed with `fderivWithin π f s y`) is continuously differentiable to order `n` on `s` (`ContDiffOn π (βn) (fun y => fderivWithin π f s y) s`).
More concisely: A function between two normed spaces is continuously differentiable to order (n+1) on a set with unique derivatives if and only if it is differentiable and its derivative within the set is continuously differentiable to order n.
|
hasFTaylorSeriesUpToOn_univ_iff
theorem hasFTaylorSeriesUpToOn_univ_iff :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ} {p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpToOn n f p Set.univ β HasFTaylorSeriesUpTo n f p
The theorem `hasFTaylorSeriesUpToOn_univ_iff` states that for any nontrivially normed field `π`, any normed addition-commutative group `E` and `F` that are also normed spaces over `π`, any function `f` mapping from `E` to `F`, any infinite natural number `n`, and any formal multilinear series `p` from `E` to `F`, the function `f` has a Taylor series up to `n` with respect to the series `p` on the universal set of `E` if and only if `f` has a Taylor series up to `n` with respect to the series `p`.
In mathematical terms, if we let `π` represent our field, `E` and `F` represent our normed vector spaces, `f` represent our function from `E` to `F`, `n` represent the degree of our series, and `p` represent our formal multilinear series, the theorem states that `f` has a Taylor series of degree `n` represented by `p` on the entire space `E` if and only if `f` has a Taylor series of degree `n` represented by `p`.
More concisely: For any nontrivially normed field `π`, normed addition-commutative groups `E` and `F` over `π`, function `f` from `E` to `F`, infinite natural number `n`, and formal multilinear series `p` from `E` to `F`, `f` has a Taylor series up to degree `n` with respect to `p` on the universal set of `E` if and only if `f` has a Taylor series up to degree `n` with respect to `p`.
|
contDiffOn_succ_iff_fderiv_of_isOpen
theorem contDiffOn_succ_iff_fderiv_of_isOpen :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : β},
IsOpen s β (ContDiffOn π (β(n + 1)) f s β DifferentiableOn π f s β§ ContDiffOn π (βn) (fun y => fderiv π f y) s)
The theorem `contDiffOn_succ_iff_fderiv_of_isOpen` states that for any field `π` with a nontrivial norm, any normed additive commutative group `E` and `F` with a normed space over `π`, any set `s` of `E`, any function `f` from `E` to `F`, and any natural number `n`, if `s` is an open set, then the function `f` is continuously differentiable to the `(n + 1)`th degree on `s` if and only if `f` is differentiable on `s` and its derivative (expressed with `fderiv`) is continuously differentiable to the `n`th degree on `s`.
More concisely: For a function `f` from a normed additive commutative group `E` to another normed space `F` over a nontrivial normed field `π`, `s` being an open set of `E`, `f` is continuously differentiable to the `(n + 1)`th degree on `s` if and only if `f` is differentiable on `s` and its `n`th derivative is continuously differentiable on `s`.
|
iteratedFDerivWithin_inter_open
theorem iteratedFDerivWithin_inter_open :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s u : Set E}
{f : E β F} {x : E} {n : β},
IsOpen u β x β u β iteratedFDerivWithin π n f (s β© u) x = iteratedFDerivWithin π n f s x
This theorem states that for any nontrivially normed field `π`, normed additive commutative group `E`, normed vector space over `π` of `E`, another normed additive commutative group `F`, another normed vector space over `π` of `F`, sets `s` and `u` in `E`, a function `f` from `E` to `F`, a point `x` in `E`, and a natural number `n`, if the set `u` is open and `x` is an element of `u`, then the `n`-th iterated FrΓ©chet derivative of `f` within the intersection of `s` and `u` at the point `x` is equal to the `n`-th iterated FrΓ©chet derivative of `f` within the set `s` at the point `x`. In simpler terms, the theorem asserts that the iterated derivative at a point within a set is unaffected if the set is intersected with an open set containing the point.
More concisely: For any normed field `π`, normed additive commutative groups `E` and `F`, normed vector spaces over `π` of `E` and `F`, sets `s` and `u` in `E` with `u` open, and a function `f` from `E` to `F`, the `n`-th iterated Frechet derivative of `f` at `x` in `s β© u` equals the `n`-th iterated Frechet derivative of `f` at `x` in `s`.
|
contDiff_iff_continuous_differentiable
theorem contDiff_iff_continuous_differentiable :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ},
ContDiff π n f β
(β (m : β), βm β€ n β Continuous fun x => iteratedFDeriv π m f x) β§
β (m : β), βm < n β Differentiable π fun x => iteratedFDeriv π m f x
The theorem `contDiff_iff_continuous_differentiable` states that for any non-trivially normed field `π`, normed additive commutative group `E`, normed space `E` over `π`, normed additive commutative group `F`, normed space `F` over `π`, function `f` from `E` to `F`, and positive extended natural number `n`, the function `f` is continuously differentiable `n` times if and only if for all natural numbers `m`, the `m`-times iterated derivative of `f` is continuous whenever `m` is less than or equal to `n`, and the function that maps `x` to the `m`-times iterated derivative of `f` at `x` is differentiable whenever `m` is less than `n`.
More concisely: A function between two normed spaces is continuously differentiable up to order n if and only if all its iterated derivatives of order less than or equal to n exist and are continuous, and the function mapping x to the iterated derivative of order m at x is differentiable for all m < n.
|
ContDiff.continuous
theorem ContDiff.continuous :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ}, ContDiff π n f β Continuous f
This theorem states that for any nontrivially normed field π and normed additive commutative groups E and F that are also normed spaces over π, if a function `f` from E to F is continuously differentiable up to any order `n`, then `f` is also a continuous function.
More concisely: A continuously differentiable up to any order function between two normed spaces over a nontrivially normed field is continuous.
|
ContDiffOn.mono
theorem ContDiffOn.mono :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : ββ}, ContDiffOn π n f s β β {t : Set E}, t β s β ContDiffOn π n f t
The theorem `ContDiffOn.mono` states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, and normed spaces over `π` for `E` and `F`, if a function `f` from `E` to `F` is continuously differentiable on a set `s` up to order `n`, then it is also continuously differentiable on any subset `t` of `s` up to the same order. In mathematical terms, if $f : E \to F$ is $C^n$ on a set $s \subseteq E$, then for any $t \subseteq s$, $f$ is also $C^n$ on $t$.
More concisely: If a function is continuously differentiable up to order n on a set, then it is also continuously differentiable up to the same order on any subset of that set.
|
ContDiffOn.differentiableOn
theorem ContDiffOn.differentiableOn :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {n : ββ}, ContDiffOn π n f s β 1 β€ n β DifferentiableOn π f s
The theorem `ContDiffOn.differentiableOn` states that if a function `f`, which maps from a normed vector space `E` over a non-trivially normed field `π` to another normed vector space `F` over the same field, is `C^n` continuous on a set `s` of `E` for `n` equal to or greater than 1 (`1 β€ n`), then it is differentiable on `s`. Here `C^n` continuity implies that the function is differentiable `n` times and all those derivatives are continuous. Hence, in more simple terms, it states that if a function is smooth enough (at least once differentiable and that derivative is continuous) on a set, then it is differentiable on that set.
More concisely: If a function between normed vector spaces is `C^1` continuous on a set, then it is differentiable on that set.
|
contDiffOn_top_iff_fderiv_of_isOpen
theorem contDiffOn_top_iff_fderiv_of_isOpen :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F},
IsOpen s β (ContDiffOn π β€ f s β DifferentiableOn π f s β§ ContDiffOn π β€ (fun y => fderiv π f y) s)
The theorem `contDiffOn_top_iff_fderiv_of_isOpen` states that for any field `π` with a norm, any normed additive commutative group `E` over `π`, and any normed additive commutative group `F` over `π`, given an open set `s` in `E` and a function `f` from `E` to `F`, the function `f` is infinitely continuously differentiable (`C^β`) on `s` if and only if it is differentiable on `s` and its derivative (expressed with `fderiv`) is also infinitely continuously differentiable (`C^β`) on `s`.
More concisely: A function between two normed spaces is infinitely continuously differentiable on an open set if and only if it is differentiable on that set and its derivative is also infinitely continuously differentiable on that set.
|
ContDiffWithinAt.mono
theorem ContDiffWithinAt.mono :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E}
{f : E β F} {x : E} {n : ββ}, ContDiffWithinAt π n f s x β β {t : Set E}, t β s β ContDiffWithinAt π n f t x
This theorem states that if a function `f` is continuously differentiable within a set `s` at a point `x`, to any order `n` over a nontrivial normed field `π`, then the function `f` is also continuously differentiable within any subset `t` of `s` at the same point `x`, to the same order `n`. Here, `E` and `F` are normed additively commutative groups under the field `π`, and `f` is a function from `E` to `F`.
More concisely: If a continuously differentiable function `f : E -> F` of order `n` over a normed field `π` at a point `x` in a set `s`, then `f` is also continuously differentiable of order `n` at `x` in any subset `t` of `s`.
|
ContDiffAt.continuousAt
theorem ContDiffAt.continuousAt :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} {n : ββ}, ContDiffAt π n f x β ContinuousAt f x
The theorem `ContDiffAt.continuousAt` states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, and function `f` mapping from `E` to `F`, if the function `f` is continuously differentiable at a point `x` of order `n`, then `f` is also continuous at the point `x`. In other words, continuous differentiability at a point implies continuity at that point.
More concisely: If a function `f` is continuously differentiable of order `n` at a point `x`, then it is continuous at `x` in the non-trivially normed fields `π`, for normed additive commutative groups `E` and `F`.
|