LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Calculus.Deriv.Comp

`HasDerivAt.scomp` theorem HasDerivAt.scomp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [inst_6 : IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F}, HasDerivAt g₁ g₁' (h x) → HasDerivAt h h' x → HasDerivAt (g₁ ∘ h) (h' • g₁') x The theorem `HasDerivAt.scomp` is a statement of the chain rule in calculus. This theorem states that for any two functions `h` and `g₁` with derivatives `h'` and `g₁'` respectively, if `h` has its derivative `h'` at a point `x` and `g₁` has its derivative `g₁'` at the point `h(x)`, then the derivative of the composition of `g₁` and `h`, that is `(g₁ ∘ h)`, at the point `x` is `h' • g₁'`. Here, '•' denotes scalar multiplication in the appropriate normed vector space. This holds when `𝕜` and `𝕜'` are non-trivially normed fields, `F` is a normed add-commutative group and a vector space over `𝕜` and `𝕜'`, and when `𝕜'` is a normed algebra over `𝕜`. More concisely: The chain rule in calculus states that for functions `h` and `g₁` with derivatives `h'` and `g₁'` respectively, the derivative of their composition `(g₁ ∘ h)` at a point `x` is `h'(x) * g₁'(h(x))`.
`HasDerivAt.comp_hasFDerivAt` theorem HasDerivAt.comp_hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E), HasDerivAt h₂ h₂' (f x) → HasFDerivAt f f' x → HasFDerivAt (h₂ ∘ f) (h₂' • f') x This theorem states that if a function `h₂` has a derivative `h₂'` at the point `f(x)` and a function `f` has a continuous linear map `f'` as a derivative at the point `x`, then the composition of `h₂` and `f` has a derivative at the point `x` which is the scalar product of `h₂'` and `f'`. In more mathematical terms, if `h₂` is differentiable at `f(x)` and `f` is differentiable at `x`, then `(h₂ ∘ f)` is differentiable at `x`, and the derivative is given by `h₂' • f'`. More concisely: If functions `f` and `h₂` are differentiable at points `x` and `f(x)` respectively, then their composition `h₂ ∘ f` is differentiable at `x`, and its derivative is equal to the scalar product of `h₂'` and `f'`, where `h₂'` is the derivative of `h₂` and `f'` is the derivative of `f`.
`HasFDerivAt.comp_hasDerivAt` theorem HasFDerivAt.comp_hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E}, HasFDerivAt l l' (f x) → HasDerivAt f f' x → HasDerivAt (l ∘ f) (l' f') x The theorem `HasFDerivAt.comp_hasDerivAt` states that for any two functions `l : F → E` and `f : 𝕜 → F` over a nontrivially normed field `𝕜`, if `l` has a Fréchet derivative `l'` at the point `f(x)`, and `f` has a derivative `f'` at `x`, then the composition function `l ∘ f` has a derivative at `x` equal to the application of the Fréchet derivative `l'` to the derivative `f'`. This encapsulates the chain rule in calculus. More concisely: If functions `l : F → E` over a nontrivially normed field `𝕜`, `l` has Fréchet derivative `l'` at `f(x)`, and `f : 𝕜 → F` has derivative `f'` at `x`, then `l ∘ f` has a derivative at `x` equal to `l' (f' (x))`.
`HasStrictDerivAt.comp` theorem HasStrictDerivAt.comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'}, HasStrictDerivAt h₂ h₂' (h x) → HasStrictDerivAt h h' x → HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x The theorem `HasStrictDerivAt.comp` states that if a function `h₂` has a strict derivative `h₂'` at the point `h(x)` and a function `h` has a strict derivative `h'` at the point `x`, in the context of nontrivially normed fields, then the composition of the two functions `(h₂ ∘ h)` has a strict derivative at the point `x` which is the product of the derivatives `h₂'` and `h'`. This captures the chain rule concept in calculus. More concisely: If `h` and `h₂` are functions with strict derivatives at a point `x` in a nontrivially normed field, then `(h₂ ∘ h)'(x) = h₂'(h(x)) h'(x)`.*
`HasDerivAt.comp` theorem HasDerivAt.comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'}, HasDerivAt h₂ h₂' (h x) → HasDerivAt h h' x → HasDerivAt (h₂ ∘ h) (h₂' * h') x This theorem is the chain rule from calculus, stated in the context of normed algebra. Specifically, it states that if a function `h₂` has derivative `h₂'` at the point `h(x)`, and a function `h` has derivative `h'` at the point `x`, then the derivative of the composition of `h₂` and `h` at the point `x` is `h₂' * h'`. This theorem holds for any nontrivially normed field `𝕜` and `𝕜'`, where `𝕜'` is a normed algebra over `𝕜`. More concisely: If `h : ℝ → 𝕜` and `h₂ : ℝ → 𝕜'` are differentiable at `x ∈ ℝ` with derivatives `h'` and `h₂'` respectively, then the derivative of `h₂ ∘ h` at `x` is `h₂' h'`.*
`HasDerivAt.comp_hasFDerivWithinAt` theorem HasDerivAt.comp_hasFDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s : Set E} (x : E), HasDerivAt h₂ h₂' (f x) → HasFDerivWithinAt f f' s x → HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x This theorem states that if a function `h₂` has a derivative `h₂'` at the point `f(x)`, and another function `f` has a Fréchet derivative `f'` within a set `s` at the point `x`, then the composition of the functions `h₂ ∘ f` also has a Fréchet derivative `h₂' • f'` within the set `s` at the same point `x`. Here, `𝕜` and `𝕜'` are types representing non-trivially normed fields, and `E` is a type representing an additive commutative group that is also a normed space over `𝕜`. The operator `•` denotes scalar multiplication, and `∘` denotes function composition. More concisely: If functions `f : E → E` and `h₂ : 𝕜 → 𝕜'` have derivatives `f' : E → E` and `h₂' : 𝕜 → 𝕜'` respectively at points `x : E` and `y : 𝕜` with `y = f(x)`, then the composition `h₂ ∘ f` has a Fréchet derivative `h₂' • f'` at point `x`.
`HasFDerivWithinAt.comp_hasDerivWithinAt` theorem HasFDerivWithinAt.comp_hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F} {f' : F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {l' : F →L[𝕜] E} {t : Set F}, HasFDerivWithinAt l l' t (f x) → HasDerivWithinAt f f' s x → Set.MapsTo f s t → HasDerivWithinAt (l ∘ f) (l' f') s x The theorem `HasFDerivWithinAt.comp_hasDerivWithinAt` states that for a composition of two functions, `l : F → E` and `f : 𝕜 → F`, if `l` has a Fréchet derivative `l'` within a set `t` at the point `f(x)`, `f` has a derivative `f'` within a set `s` at the point `x`, and `f` maps `s` into `t`, then the composition `l ∘ f` has a derivative within the set `s` at the point `x` equal to the application of the Fréchet derivative `l'` to the derivative `f'`. This theorem is crucial in multi-variable calculus and the analysis of composed functions. More concisely: If functions `l : F -> E` and `f : ℝ^n -> F` have derivatives within sets `t` and `s`, respectively, at points `f(x)` and `x`, and `f(s)` is contained in `t`, then `l ∘ f` has a derivative equal to `l'(f'(x))` at `x`.
`HasDerivWithinAt.scomp` theorem HasDerivWithinAt.scomp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [inst_6 : IsScalarTower 𝕜 𝕜' F] {t' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F}, HasDerivWithinAt g₁ g₁' t' (h x) → HasDerivWithinAt h h' s x → Set.MapsTo h s t' → HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x The theorem `HasDerivWithinAt.scomp` states that for all types `𝕜` and `𝕜'` equipped with normed fields properties, and a type `F` equipped with normed add comm group and normed space properties, given a point `x` of type `𝕜`, sets `s` of type `𝕜` and `t'` of type `𝕜'`, functions `h : 𝕜 → 𝕜'` and `g₁ : 𝕜' → F`, and elements `h'` of type `𝕜'` and `g₁'` of type `F`. If `g₁` has a derivative `g₁'` at the point `h(x)` within set `t'`, `h` has a derivative `h'` at the point `x` within set `s`, and the image of set `s` under the function `h` is contained in set `t'`, then the composite function `(g₁ ∘ h)` has a derivative `(h' • g₁')` at point `x` within set `s`. Here, `•` denotes the scalar multiplication operation. More concisely: If `h` is a function from a normed space `𝕜` to another normed space `𝕜'`, `g₁` is a function from `𝕜'` to a normed vector space `F` with derivative `g₁'` at `h(x)`, `h` has derivative `h'` at `x` with image of `s` in `t'`, then `(g₁ ∘ h)` has derivative `(h' • g₁')` at `x`.
`HasDerivAt.comp_hasDerivWithinAt` theorem HasDerivAt.comp_hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'}, HasDerivAt h₂ h₂' (h x) → HasDerivWithinAt h h' s x → HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x The theorem `HasDerivAt.comp_hasDerivWithinAt` states that given two functions `h` and `h₂` and their respective derivatives `h'` and `h₂'` at a point `x`, within a subset `s`, where the field `𝕜` is a non-trivially normed field, and `𝕜'` is another non-trivially normed field under a normed algebra over `𝕜`. If the function `h₂` has a derivative at `h(x)`, and the function `h` has a derivative within the subset `s` at point `x`, then the composition of `h₂` and `h` also has a derivative within the subset `s` at point `x`, and the derivative is the product of `h₂'` and `h'`. This theorem essentially states the chain rule for derivatives within a subset. More concisely: Given functions `h: 𝕜 → 𝕜'`, `h₂: 𝕜' → 𝕜''`, `h', h₂'` their respective derivatives, if `h` is differentiable at `x`, `h₂` is differentiable at `h(x)`, and `𝕜`, `𝕜'`, `𝕜''` are non-trivially normed fields under normed algebra over `𝕜`, then `h₂ ∘ h` is differentiable at `x` with derivative `h₂'(h(x)) * h'(x)`.
`HasDerivWithinAt.comp` theorem HasDerivWithinAt.comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'}, HasDerivWithinAt h₂ h₂' s' (h x) → HasDerivWithinAt h h' s x → Set.MapsTo h s s' → HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x This theorem states that, given two types `𝕜` and `𝕜'` which are nontrivially normed fields, a point `x` in `𝕜`, subsets `s` of `𝕜` and `s'` of `𝕜'`, and two functions `h` and `h₂` mapping `𝕜` to `𝕜'` and `𝕜'` to `𝕜'` respectively, with corresponding derivatives `h'` and `h₂'`, if `h₂` has derivative `h₂'` at the image of `x` under `h` within `s'` and `h` has derivative `h'` at `x` within `s`, and furthermore if the image of `s` under `h` is contained in `s'` (i.e., `h` maps `s` into `s'`), then the composition of `h₂` and `h` has the derivative `h₂' * h'` at `x` within `s`. This theorem essentially formalizes the chain rule of calculus in the context of derivatives within specific subsets of the domain. More concisely: Given nontrivially normed fields `𝕜` and `𝕜'`, functions `h: 𝕜 → 𝕜'` and `h₂: 𝕜' → 𝕜'` with derivatives `h'` and `h₂'`, if `h₂' * h'` is the derivative of `h₂ ∘ h` at `x` within `s` and `h(s) ⊆ s'`, then `h₂'` is the derivative of `h₂ ∘ h` at `x` within `s`.
`HasStrictDerivAt.comp_hasStrictFDerivAt` theorem HasStrictDerivAt.comp_hasStrictFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜'] {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E), HasStrictDerivAt h₂ h₂' (f x) → HasStrictFDerivAt f f' x → HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x The theorem `HasStrictDerivAt.comp_hasStrictFDerivAt` states that if a function `h₂` has a strict derivative `h₂'` at the point `f(x)` (in the sense of strict differentiability), and another function `f` has strict Frechet derivative `f'` at point `x`, then the composed function `(h₂ ∘ f)` has a strict Frechet derivative of `(h₂' • f')` at the point `x`. In simpler terms, this theorem is about the chain rule in differential calculus, which describes the derivative of a composition of functions. More concisely: If `f` is strictly Frechet differentiable at `x` and `h₂` is strictly differentiable at `f(x)`, then the composed function `h₂ ∘ f` is strictly Frechet differentiable at `x` with derivative `(h₂' • f')`.
`HasDerivAtFilter.scomp` theorem HasDerivAtFilter.scomp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {L : Filter 𝕜} {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [inst_6 : IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {L' : Filter 𝕜'}, HasDerivAtFilter g₁ g₁' (h x) L' → HasDerivAtFilter h h' x L → Filter.Tendsto h L L' → HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L This theorem, `HasDerivAtFilter.scomp`, states that given two functions `h` and `g₁` on the types `𝕜` and `𝕜'` respectively, with known derivatives at a point `x` for `h` and at `h x` for `g₁` as `x` approaches along the filter `L` and `h x` approaches along the filter `L'` respectively, if `h` converges from filter `L` to `L'` as `x` approaches, then the derivative of the composition of `g₁` and `h` at the point `x` along the filter `L` exists and is equal to the derivative of `h` at `x` scaled by the derivative of `g₁` at `h x`. This states a version of the chain rule for derivatives in the context of normed spaces and filters. More concisely: Given functions `h: 𝕜 → 𝕜'` and `g₁: 𝕜' → ℝ` with derivatives at `x` along filters `L` and `L'`, respectively, and assuming `h` converges from `L` to `L'`, the derivative of `g₁ ∘ h` at `x` along `L` exists and equals the derivative of `h` at `x` multiplied by the derivative of `g₁` at `h x`.