LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Calculus.FDeriv.Comp

fderivWithin.comp₃

theorem fderivWithin.comp₃ : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G'] [inst_8 : NormedSpace π•œ G'] {f : E β†’ F} (x : E) {s : Set E} {g' : G β†’ G'} {g : F β†’ G} {t : Set F} {u : Set G} {y : F} {y' : G}, DifferentiableWithinAt π•œ g' u y' β†’ DifferentiableWithinAt π•œ g t y β†’ DifferentiableWithinAt π•œ f s x β†’ Set.MapsTo g t u β†’ Set.MapsTo f s t β†’ g y = y' β†’ f x = y β†’ UniqueDiffWithinAt π•œ s x β†’ fderivWithin π•œ (g' ∘ g ∘ f) s x = (fderivWithin π•œ g' u y').comp ((fderivWithin π•œ g t y).comp (fderivWithin π•œ f s x))

The theorem `fderivWithin.comp₃` states that, for a given set of types (`π•œ`, `E`, `F`, `G`, `G'`), functions (`f`, `g`, `g'`), sets (`s`, `t`, `u`), and points (`x`, `y`, `y'`), if the functions `f`, `g`, and `g'` are differentiable at `x`, `y`, and `y'` within their respective sets, the images of `f` and `g` are contained in `t` and `u` respectively, and `f(x)` is equal to `y` and `g(y)` is equal to `y'`, and the point `x` has a unique tangent line within the set `s`, then the derivative of the composition of `g'`, `g`, and `f` at point `x` within the set `s` is equal to the composition of the derivatives of `g'`, `g`, and `f` at their respective points within their respective sets.

More concisely: If functions `f: E -> F`, `g: F -> G`, `g': E -> G'`, `x ∈ s`, `y = f(x) ∈ t`, `y' = g(y) ∈ u`, and `x` has a unique tangent line within `s`, then `(d(g' ∘ g ∘ f)(x) = d(g' ∘ g)(y) ∘ d(f)(x)`) within `s`.

DifferentiableAt.comp_differentiableWithinAt

theorem DifferentiableAt.comp_differentiableWithinAt : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {f : E β†’ F} (x : E) {s : Set E} {g : F β†’ G}, DifferentiableAt π•œ g (f x) β†’ DifferentiableWithinAt π•œ f s x β†’ DifferentiableWithinAt π•œ (g ∘ f) s x

The theorem `DifferentiableAt.comp_differentiableWithinAt` states that for any types `π•œ`, `E`, `F`, and `G` where `π•œ` is a nontrivially normed field, `E`, `F`, `G` are normed add commutative groups and normed spaces over `π•œ`, given a function `f` from `E` to `F`, a set `s` of `E`, a function `g` from `F` to `G`, and a point `x` in `E`, if `g` is differentiable at the point `f(x)`, and `f` is differentiable within the set `s` at the point `x`, then the composite function `g ∘ f` is differentiable within the set `s` at the point `x`. In other words, the differentiability of `g` at `f(x)` and `f` within `s` at `x` guarantees the differentiability of the composite function `g ∘ f` within `s` at `x`.

More concisely: If `f: E -> F` is differentiable within `s βŠ† E` at `x ∈ E` and `g: F -> G` is differentiable at `f(x)`, then `g ∘ f` is differentiable at `x`.

HasFDerivAtFilter.comp

theorem HasFDerivAtFilter.comp : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {L : Filter E} {g : F β†’ G} {g' : F β†’L[π•œ] G} {L' : Filter F}, HasFDerivAtFilter g g' (f x) L' β†’ HasFDerivAtFilter f f' x L β†’ Filter.Tendsto f L L' β†’ HasFDerivAtFilter (g ∘ f) (g'.comp f') x L

The `HasFDerivAtFilter.comp` theorem states that for two functions `f : E β†’ F` and `g : F β†’ G` defined over normed spaces `E`, `F`, and `G` over a nontrivially normed field `π•œ`, if `f` has a derivative `f'` at point `x` with respect to filter `L` and `g` has a derivative `g'` at `f(x)` with respect to filter `L'`, and if `f` tends to `L'` under filter `L`, then the composite function `g ∘ f` has a derivative `ContinuousLinearMap.comp g' f'` at point `x` with respect to filter `L`. This is a formal statement of the chain rule in the language of filters.

More concisely: If functions `f : E β†’ F` and `g : F β†’ G` have derivatives at points `x` and `f(x)` with respect to filters `L` and `L'`, respectively, and `f(x)` tends to `L'` under `L`, then the composite function `g ∘ f` has a derivative `g' ∘ f'` at `x` with respect to `L`.

Differentiable.comp

theorem Differentiable.comp : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {f : E β†’ F} {g : F β†’ G}, Differentiable π•œ g β†’ Differentiable π•œ f β†’ Differentiable π•œ (g ∘ f)

The theorem `Differentiable.comp` states that given any Nontrivially Normed Field `π•œ` and three Normed Spaces `E`, `F`, and `G`, if a function `f` from `E` to `F` is differentiable at every point and a function `g` from `F` to `G` is also differentiable at every point, then the composition of `g` and `f` (i.e., `g ∘ f`) is differentiable at every point as well. In other words, the composition of two differentiable functions is also differentiable.

More concisely: Given any Nontrivially Normed Field π•œ and Normed Spaces E, F, and G, if functions f : E β†’ F and g : F β†’ G are differentiable at every point, then their composition g ∘ f is differentiable at every point.

HasStrictFDerivAt.comp

theorem HasStrictFDerivAt.comp : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {g : F β†’ G} {g' : F β†’L[π•œ] G}, HasStrictFDerivAt g g' (f x) β†’ HasStrictFDerivAt f f' x β†’ HasStrictFDerivAt (fun x => g (f x)) (g'.comp f') x

This theorem states the chain rule for derivatives in the sense of strict differentiability. Given a nontrivially normed field `π•œ`, normed add commutative groups `E`, `F`, and `G`, and normed spaces over `π•œ` for `E`, `F`, and `G`; if `f : E β†’ F` is strictly differentiable at a point `x` with derivative `f' : E β†’L[π•œ] F`, and `g : F β†’ G` is strictly differentiable at `f(x)` with derivative `g' : F β†’L[π•œ] G`, then the composed function `(fun x => g (f x))` is also strictly differentiable at `x` and its derivative is the continuous linear map `ContinuousLinearMap.comp g' f'`.

More concisely: If functions `f : E β†’ F` and `g : F β†’ G` are strictly differentiable at points `x` and `f(x)`, respectively, then the composition `g ∘ f` is strictly differentiable at `x` with derivative `g' ∘ f'`.

HasFDerivAt.comp

theorem HasFDerivAt.comp : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {g : F β†’ G} {g' : F β†’L[π•œ] G}, HasFDerivAt g g' (f x) β†’ HasFDerivAt f f' x β†’ HasFDerivAt (g ∘ f) (g'.comp f') x

This theorem is a formalization of the chain rule in calculus. It states that if a function `f` from `E` to `F` has a derivative `f'` at a point `x` in `E`, and a function `g` from `F` to `G` has a derivative `g'` at the point `f x` in `F`, then the composition function `(g ∘ f)` has a derivative `(ContinuousLinearMap.comp g' f')` at `x`. Here, `π•œ`, `E`, `F`, and `G` are normed spaces over a nontrivially normed field, which is a field equipped with a norm that satisfies certain properties. The derivative is a continuous linear map, which is a linear map between normed spaces that is also continuous.

More concisely: If `f: E β†’ F` and `g: F β†’ G` are continuously differentiable functions between normed spaces, then `(g ∘ f)` is continuously differentiable and `(g ∘ f)'.x = g'.(f x) ∘ f'.x` for all `x ∈ E`.

DifferentiableWithinAt.comp

theorem DifferentiableWithinAt.comp : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {f : E β†’ F} (x : E) {s : Set E} {g : F β†’ G} {t : Set F}, DifferentiableWithinAt π•œ g t (f x) β†’ DifferentiableWithinAt π•œ f s x β†’ Set.MapsTo f s t β†’ DifferentiableWithinAt π•œ (g ∘ f) s x

The theorem `DifferentiableWithinAt.comp` states that if a function `g` is differentiable at the point `f(x)` within a set `t`, and a function `f` is differentiable at the point `x` within a set `s`, and if `f` maps every point of `s` into `t`, then the composition function `g ∘ f` is also differentiable at the point `x` within the set `s`. Here `π•œ`, `E`, `F` and `G` denote the types involved, while `NontriviallyNormedField π•œ`, `NormedAddCommGroup E`, `NormedSpace π•œ E`, `NormedAddCommGroup F`, `NormedSpace π•œ F`, `NormedAddCommGroup G` and `NormedSpace π•œ G` are structures capturing the required properties of these types. This theorem essentially encapsulates the chain rule from calculus in the context of differentiable functions within specified sets.

More concisely: If functions `f: E β†’ F` and `g: F β†’ G` are differentiable at points `x ∈ E` and `f(x) ∈ T βŠ† F` respectively, and `f(s) βŠ† t` for all `s ∈ s ∈ S βŠ† E`, then the composition `g ∘ f: E β†’ G` is differentiable at `x`.

DifferentiableOn.comp

theorem DifferentiableOn.comp : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {f : E β†’ F} {s : Set E} {g : F β†’ G} {t : Set F}, DifferentiableOn π•œ g t β†’ DifferentiableOn π•œ f s β†’ Set.MapsTo f s t β†’ DifferentiableOn π•œ (g ∘ f) s

This theorem, `DifferentiableOn.comp`, states that for any non-trivially normed field `π•œ`, normed additive commutative groups `E`, `F`, and `G`, and normed vector spaces over `π•œ` of `E`, `F`, and `G`, if a function `g` from `F` to `G` is differentiable on a set `t`, a function `f` from `E` to `F` is differentiable on a set `s`, and the image of `s` under `f` is contained in `t`, then the composite function `g ∘ f` is differentiable on the set `s`. In other words, the composition of two differentiable functions is differentiable provided the image of the first function is contained in the domain of the second function.

More concisely: If `f: E β†’ F` is differentiable on `s βŠ† E`, `g: F β†’ G` is differentiable on `t βŠ† F`, and `s βŠ† f⁻¹(t)`, then `g ∘ f` is differentiable on `s`.

HasFDerivAt.comp_hasFDerivWithinAt

theorem HasFDerivAt.comp_hasFDerivWithinAt : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {f : E β†’ F} {f' : E β†’L[π•œ] F} (x : E) {s : Set E} {g : F β†’ G} {g' : F β†’L[π•œ] G}, HasFDerivAt g g' (f x) β†’ HasFDerivWithinAt f f' s x β†’ HasFDerivWithinAt (g ∘ f) (g'.comp f') s x

This theorem states that if a function `g` has a derivative `g'` at the point `f(x)`, and another function `f` has a derivative `f'` within a set `s` at the point `x`, then the composition of the functions `g` and `f` has a derivative with respect to `x` within the set `s` at the point `x`. Specifically, this derivative is a linear map defined as the composition of the linear maps `g'` and `f'`. This property underpins the chain rule in calculus in the context of functions between normed vector spaces over a non-trivially normed field `π•œ`.

More concisely: If functions `f` and `g` are differentiable at points `x` with derivatives `f'` and `g'` respectively, then the composition `g ∘ f` is differentiable at `x` with derivative `(g ∘ f)'(x) = g'(f(x)) ∘ f'(x)`.

DifferentiableAt.comp

theorem DifferentiableAt.comp : βˆ€ {π•œ : Type u_1} [inst : NontriviallyNormedField π•œ] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π•œ E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π•œ F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π•œ G] {f : E β†’ F} (x : E) {g : F β†’ G}, DifferentiableAt π•œ g (f x) β†’ DifferentiableAt π•œ f x β†’ DifferentiableAt π•œ (g ∘ f) x

The theorem `DifferentiableAt.comp` states that for any non-trivial normed field `π•œ`, if `f` is a function from a normed space `E` over `π•œ` to another normed space `F` over `π•œ`, and `g` is a function from `F` to yet another normed space `G` over `π•œ`, then if `g` is differentiable at the point `f(x)`, and if `f` is also differentiable at the point `x`, then the function obtained by composing `g` and `f` (i.e., `g ∘ f`) is also differentiable at the point `x`. This theorem encapsulates the chain rule from calculus.

More concisely: If `f:` X β†’ Y is differentiable at `x ∈ X` and `g:` Y β†’ Z is differentiable at `y = f(x)`, then the composition `g ∘ f:` X β†’ Z is differentiable at `x`.