LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

`AnalyticOn.iterated_deriv` theorem AnalyticOn.iterated_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} [inst_3 : CompleteSpace F], AnalyticOn 𝕜 f s → ∀ (n : ℕ), AnalyticOn 𝕜 (deriv^[n] f) s The theorem `AnalyticOn.iterated_deriv` states that for any nontrivially normed field `𝕜` and a normed additive commutative group `F` over `𝕜`, if a function `f` is analytic on a set `s`, then all of its successive derivatives are also analytic on the same set. This holds true for any natural number `n`, which represents the order of the derivative, and is assumed that `F` is a complete space. More concisely: For any nontrivially normed field `𝕜` and a complete, normed additive commutative group `F` over `𝕜`, if a function `f` is analytic on a set `s` in `F`, then all its derivatives up to order `n` are also analytic on `s`.
`AnalyticAt.differentiableWithinAt` theorem AnalyticAt.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, AnalyticAt 𝕜 f x → DifferentiableWithinAt 𝕜 f s x The theorem `AnalyticAt.differentiableWithinAt` states that for any non-trivially normed field `𝕜` and normed add commutative group `E` and `F` with normed space structures over `𝕜`, if a function `f` from `E` to `F` is analytic at a point `x`, then `f` is differentiable at that point `x` within any set `s` of `E`. Here, being analytic means `f` admits a convergent power series expansion around `x`, and being differentiable means `f` admits a derivative at `x` within `s`. More concisely: If a function `f` is analytic at a point `x` in the normed spaces `E` and `F` over a non-trivially normed field `𝕜`, then `f` is differentiable at `x` within any neighborhood `s` of `x` in `E`.
`CPolynomialOn.contDiffOn` theorem CPolynomialOn.contDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, CPolynomialOn 𝕜 f s → ∀ {n : ℕ∞}, ContDiffOn 𝕜 n f s This theorem states that for any nontrivially normed field `𝕜`, normed add commutative groups `E` and `F`, and a normed space over `𝕜` on both `E` and `F`, if a function `f` from `E` to `F` is continuously polynomial on a set `s` in `E`, then the function `f` is infinitely differentiable on the set `s` for any natural number `n` or infinity `ℕ∞`. In mathematical terms, if $f : E \to F$ is a polynomial function, it possesses derivatives of all orders on set `s`. More concisely: For any nontrivially normed field `𝕜`, if a polynomial function `f` from a normed space `E` over `𝕜` to another normed space `F` is continuous on a set `s` in `E`, then `f` has derivatives of all orders on `s`.
`HasFiniteFPowerSeriesOnBall.fderiv'` theorem HasFiniteFPowerSeriesOnBall.fderiv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E}, HasFiniteFPowerSeriesOnBall f p x n r → HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r This theorem states that if a function has a finite power series within a ball in a normed space, then its derivative also has a finite power series within the same ball. More specifically, the theorem says that given a non-trivially normed field `𝕜`, normed additive commutative groups `E` and `F` with `E` and `F` also being normed spaces over `𝕜`, a formal multilinear series `p`, an extended nonnegative real number `r`, a natural number `n`, a function `f` from `E` to `F`, and a point `x` in `E`, if the function `f` has a finite power series on the ball of radius `r` centered at `x` and of degree `< n`, then the derivative of `f` (computed using `fderiv 𝕜 f`) also has a finite power series on the same ball, with the degree of the power series being `< n - 1`. More concisely: If a function `f` from a normed space `E` to another normed space `F` over a non-trivially normed field `𝕜` has a finite power series with degree less than `n` on the ball of radius `r` centered at `x` in `E`, then its derivative also has a finite power series with degree less than `n-1` on the same ball.
`CPolynomialOn.deriv` theorem CPolynomialOn.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜}, CPolynomialOn 𝕜 f s → CPolynomialOn 𝕜 (deriv f) s This theorem states that if a function is continuously polynomial on a certain set 's', then its derivative is also continuously polynomial on the same set. The function and its derivative are defined over a non-trivially normed field '𝕜' and their ranges lie in a normed add commutative group 'F' that is also a normed space over '𝕜'. The term "continuously polynomial" means that the function (or its derivative) behaves like a polynomial around each point in the set 's'. More concisely: If a function and its derivative are continuously polynomial over a non-trivially normed field and have ranges in a normed add commutative group that is also a normed space, then the derivative is continuously polynomial.
`AnalyticOn.contDiffOn` theorem AnalyticOn.contDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} [inst_5 : CompleteSpace F], AnalyticOn 𝕜 f s → ∀ {n : ℕ∞}, ContDiffOn 𝕜 n f s The theorem `AnalyticOn.contDiffOn` states that for any nontrivially normed field `𝕜`, if a function `f` from a normed add-commutative group `E` to another normed add-commutative group `F` (both over `𝕜`) is analytic on a set `s` of `E`, and `F` is a complete space, then `f` is infinitely differentiable on `s`. In other words, an analytic function is infinitely differentiable. More concisely: If a function between two complete normed add-commutative groups over a nontrivially normed field is analytic on a set, then it is infinitely differentiable on that set.
`CPolynomialOn.iterated_deriv` theorem CPolynomialOn.iterated_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜}, CPolynomialOn 𝕜 f s → ∀ (n : ℕ), CPolynomialOn 𝕜 (deriv^[n] f) s The theorem `CPolynomialOn.iterated_deriv` states that for any non-trivially normed field `𝕜` and any normed adding commutative group `F` that forms a normed space over `𝕜`, if a function `f` from `𝕜` to `F` is continuously polynomial on a set `s` (i.e., it is continuously polynomial at every point of `s`), then all of its `n`-th order derivatives are also continuously polynomial on the same set `s`. This holds for all natural numbers `n`, indicating that the theorem applies to all orders of derivatives. More concisely: If a continuously polynomial function from a non-trivially normed field to a normed adding commutative group is defined on a set, then all its derivatives of any order are also continuously polynomial on that set.
`AnalyticOn.differentiableOn` theorem AnalyticOn.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, AnalyticOn 𝕜 f s → DifferentiableOn 𝕜 f s The theorem `AnalyticOn.differentiableOn` states that for any nontrivially normed field `𝕜`, normed add commutative groups `E` and `F`, and a function `f` from `E` to `F`, if `f` is analytic on a set `s` of `E`, then `f` is also differentiable on the same set `s`. In other words, in the context of these algebraic structures, being analytic implies being differentiable. More concisely: If `f` is an analytic function from a normed additive commutative group `E` to another normed additive commutative group `F` over a nontrivially normed field, then `f` is differentiable on the domain where it is analytic.
`HasFiniteFPowerSeriesOnBall.fderiv` theorem HasFiniteFPowerSeriesOnBall.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E}, HasFiniteFPowerSeriesOnBall f p x (n + 1) r → HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r The theorem `HasFiniteFPowerSeriesOnBall.fderiv` states that if a function `f` has a finite power series representation within a ball in a non-trivially normed field `𝕜`, then its derivative also has a finite power series within the same ball. More specifically, if the function `f` from a normed add commutative group `E` to another such group `F` has a finite power series representation given by the formal multilinear series `p` at a point `x` with radius `r` up to the `(n + 1)`-th term, then the derivative of `f`, computed using `fderiv`, has a finite power series representation given by the derivative of the series `p` up to the `n`-th term, within the same ball. More concisely: If a function `f` with a finite power series representation within a ball in a non-trivially normed field has a derivative, then its derivative also has a finite power series representation within the same ball, given by the derivative of the series up to the same degree.
`HasFPowerSeriesAt.hasFDerivAt` theorem HasFPowerSeriesAt.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E}, HasFPowerSeriesAt f p x → HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x This theorem states that for any non-trivially normed field `𝕜`, normed additive commutative groups `E` and `F`, and a function `f` mapping `E` to `F`, if `f` has a formal power series expansion at a point `x` in `E`, then `f` also has a derivative at `x`. The derivative is the continuous linear map given by applying the continuous multilinear curry function to the first term of the power series, effectively obtaining the linear term of the power series as the derivative. More concisely: If `f` is a function from a normed additive commutative group `E` to another normed additive commutative group `F` over a non-trivially normed field, and `f` has a formal power series expansion at a point `x` in `E`, then `f` has a derivative at `x` given by the continuous linear map that is the application of the multilinear curry function to the first term of `f`'s power series.
`CPolynomialOn.fderiv` theorem CPolynomialOn.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, CPolynomialOn 𝕜 f s → CPolynomialOn 𝕜 (fderiv 𝕜 f) s The theorem `CPolynomialOn.fderiv` states that for any field `𝕜` which is non-trivially normed, and for any normed add-commutative groups `E` and `F` with a normed space structure over `𝕜`, if a function `f` from `E` to `F` is continuously polynomial on a set `s` in `E`, then its Fréchet derivative is also continuously polynomial on the same set `s`. This means that the higher-order behavior of the function - as captured by its derivative - also exhibits a polynomial relationship across all points in the set `s`. More concisely: If `f` is a continuously polynomial function from a normed add-commutative group `E` to another normed add-commutative group `F` over a non-trivially normed field `𝕜`, and `s` is a subset of `E`, then the Fréchet derivative of `f` on `s` is also continuously polynomial.
`AnalyticOn.deriv` theorem AnalyticOn.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} [inst_3 : CompleteSpace F], AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (deriv f) s The theorem "AnalyticOn.deriv" states that for any non-trivially normed field `𝕜` and space `F` that is both a normed additive commutative group and a normed space over `𝕜`, if a function `f` from `𝕜` to `F` is analytic on a set `s` of `𝕜`, and `F` is a complete space, then the derivative of `f` is also analytic on the set `s`. In simpler terms, the theorem says that the derivative of a function that is analytic at all points in a certain set, is also analytic at all points in that set. More concisely: If `𝕜` is a non-trivially normed field, `F` is a complete, normed additive commutative group and normed space over `𝕜`, and `f` is an analytic function from `𝕜` to `F` on a set `s`, then the derivative of `f` is analytic on `s`.
`HasFPowerSeriesOnBall.fderiv` theorem HasFPowerSeriesOnBall.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [inst_5 : CompleteSpace F], HasFPowerSeriesOnBall f p x r → HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x r This theorem states that if a function `f` from a normed space `E` to another normed space `F` over a non-trivially normed field `𝕜` has a power series representation within a ball of radius `r` (an extended non-negative real number) centered at a point `x` in `E`, then its derivative also has a power series representation within the same ball. Both power series are formal multilinear series with coefficients in the field `𝕜`, and the power series for the derivative of `f` is obtained by taking the derivative of each term in the power series for `f`. This is true assuming that the normed space `F` is complete. More concisely: If `f` is a function from a complete normed space `E` to another normed space `F` over a non-trivially normed field `𝕜` with a power series representation in a ball of radius `r` centered at `x` in `E`, then `f`'s derivative also has a power series representation within the same ball, obtained by differentiating each term of `f`'s power series.
`AnalyticOn.iteratedFDeriv` theorem AnalyticOn.iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} [inst_5 : CompleteSpace F], AnalyticOn 𝕜 f s → ∀ (n : ℕ), AnalyticOn 𝕜 (iteratedFDeriv 𝕜 n f) s The theorem `AnalyticOn.iteratedFDeriv` states that for any non-trivial normed field `𝕜`, normed additive commutative groups `E` and `F` that also form normed spaces over `𝕜`, and a complete space `F`, if a function `f` mapping from `E` to `F` is analytic on a set `s` in `E`, then the successive Fréchet derivatives of `f` are also analytic on the same set `s`, for all natural numbers `n`. In simpler terms, if a function is analytic at every point of a set, then its repeated derivatives are also analytic at every point of the same set. More concisely: If `f` is an analytic function from a normed space `E` to a Banach space `F` over a non-trivial normed field `𝕜`, then the successive Fréchet derivatives of `f` are also analytic on the domain of `f`.
`CPolynomialOn.iteratedFDeriv` theorem CPolynomialOn.iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, CPolynomialOn 𝕜 f s → ∀ (n : ℕ), CPolynomialOn 𝕜 (iteratedFDeriv 𝕜 n f) s The theorem `CPolynomialOn.iteratedFDeriv` states that if a function `f` is continuously polynomial on a set `s`, then its successive Fréchet derivatives are also continuously polynomial on the same set `s`. Here, the Fréchet derivative is a generalization of the derivative concept in calculus, suitable for functions between Banach spaces (normed vector spaces that are also complete metric spaces). This is true for any natural number `n`, indicating that the property holds for the `n`th derivative of the function. This theorem is defined on a non-trivially normed field `𝕜`, normed additive commutative group `E` and `F` where `E` and `F` are vector spaces over the field `𝕜`. More concisely: If a function `f` is continuously polynomial on a set `s` in the normed vector spaces `E` and `F` over a non-trivially normed field `𝕜`, then its Fréchet derivatives of any order are also continuously polynomial on `s`.
`AnalyticOn.fderiv` theorem AnalyticOn.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} [inst_5 : CompleteSpace F], AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (fderiv 𝕜 f) s The theorem 'AnalyticOn.fderiv' states that if a function `f`, which maps from a normed additive commutative group `E` to another such group `F` over a non-trivially normed field `𝕜`, is analytic on a set `s` of `E` (that is, `f` is analytic at every point in `s`), then its Fréchet derivative (denoted as `fderiv 𝕜 f`) is also analytic on the same set `s`. This conclusion holds under the assumption that `F` is a complete space. More concisely: If `f: E → F` is an analytic function from a normed additive commutative group `E` to a complete normed additive commutative group `F` over a non-trivially normed field, then its Fréchet derivative `fderiv 𝕜 f` is also an analytic function on `E`.