DifferentiableAt.prod
theorem DifferentiableAt.prod :
∀ {𝕜 : 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} {f₂ : E → G},
DifferentiableAt 𝕜 f₁ x → DifferentiableAt 𝕜 f₂ x → DifferentiableAt 𝕜 (fun x => (f₁ x, f₂ x)) x
The theorem `DifferentiableAt.prod` states that, for any non-trivially normed field `𝕜`, normed additive commutative group and `𝕜`-normed space structures on types `E`, `F`, and `G`, if functions `f₁ : E → F` and `f₂ : E → G` are both differentiable at a point `x` in `E`, then the function that maps `x` to the tuple `(f₁ x, f₂ x)` is also differentiable at `x`. In other words, the differentiability of individual functions implies the differentiability of their product function at the same point.
More concisely: If `f₁ : E → F` and `f₂ : E → G` are differentiable at `x` in the `𝕜`-normed spaces `E`, `F`, and `G`, then the function `(f₁, f₂) : E → F × G` is differentiable at `x`.
|
DifferentiableWithinAt.prod
theorem DifferentiableWithinAt.prod :
∀ {𝕜 : 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}
{f₂ : E → G},
DifferentiableWithinAt 𝕜 f₁ s x →
DifferentiableWithinAt 𝕜 f₂ s x → DifferentiableWithinAt 𝕜 (fun x => (f₁ x, f₂ x)) s x
This theorem, `DifferentiableWithinAt.prod`, states that given a type `𝕜` which is a non-trivially normed field, types `E`, `F`, and `G` that are normed add commutative groups and normed spaces over `𝕜`, and two functions `f₁` and `f₂` from `E` to `F` and `G` respectively, if both `f₁` and `f₂` are differentiable at a point `x` within a set `s` (of type `Set E`), then the function mapping `x` to the pair `(f₁ x, f₂ x)` is also differentiable at the same point `x` within the same set `s`. Essentially, it ensures the differentiability of the product of two functions when both of the functions are differentiable at a specific point within a particular set.
More concisely: If `f₁: E → F` and `f₂: E → G` are differentiable at `x ∈ E` within `s ⊆ E`, then the function `(x ↦ (f₁ x, f₂ x))` from `E` to `F × G` is differentiable at `x` within `s`.
|
HasFDerivAt.prod
theorem HasFDerivAt.prod :
∀ {𝕜 : 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}
{f₂ : E → G} {f₂' : E →L[𝕜] G},
HasFDerivAt f₁ f₁' x → HasFDerivAt f₂ f₂' x → HasFDerivAt (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') x
The theorem `HasFDerivAt.prod` states that for any type `𝕜` that is a nontrivially normed field, types `E`, `F`, and `G` that are normed spaces over `𝕜`, and functions `f₁: E → F`, `f₂: E → G` with continuous linear maps `f₁'`, `f₂'` as their derivatives at a point `x` in `E`, if both `f₁` and `f₂` have derivatives at `x`, then the function mapping `x` to the pair `(f₁ x, f₂ x)` also has a derivative at `x`, which is the continuous linear map from `E` to the product space `F × G` that is the product of `f₁'` and `f₂'`. This theorem essentially asserts that the derivative of a pair of functions is the pair of their derivatives.
More concisely: Given a nontrivially normed field `𝕜` and normed spaces `E`, `F`, and `G` over `𝕜`, if `f₁: E → F` and `f₂: E → G` are functions with continuous linear derivatives `f₁'` and `f₂'` at a point `x` in `E`, then the function mapping `x` to `(f₁ x, f₂ x)` has a derivative at `x`, which is the product of `f₁'` and `f₂'`.
|
differentiableAt_snd
theorem differentiableAt_snd :
∀ {𝕜 : 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] {p : E × F},
DifferentiableAt 𝕜 Prod.snd p
This theorem states that for any non-trivial normed field `𝕜`, any normed additive commutative group `E`, any normed vector space over `𝕜` of `E`, any normed additive commutative group `F`, and any normed vector space over `𝕜` of `F`, the second projection function `Prod.snd` is differentiable at any point `p` in the product space `E × F`. In mathematical terms, if `p` belongs to the Cartesian product of sets `E` and `F`, the function `Prod.snd` that projects `p` onto the second coordinate (`F`) admits a derivative at `p`.
More concisely: The second projection of a product of two normed vector spaces over a non-trivial normed field is differentiable at any point in the product space.
|
hasFDerivAtFilter_fst
theorem hasFDerivAtFilter_fst :
∀ {𝕜 : 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] {p : E × F}
{L : Filter (E × F)}, HasFDerivAtFilter Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p L
This theorem, `hasFDerivAtFilter_fst`, states that for any nontrivially normed field `𝕜`, normed additive commutative group `E`, normed space over `𝕜` of `E`, normed additive commutative group `F`, normed space over `𝕜` of `F`, a pair `p` of elements from `E` and `F`, and a filter `L` on the cartesian product of `E` and `F`, the function `Prod.fst` (which projects an element of the cartesian product of `E` and `F` to `E`) has a Fréchet derivative at `p` with respect to `L`, and this derivative is the continuous linear map `ContinuousLinearMap.fst 𝕜 E F` (which is essentially the same projection, but considered as a continuous linear map).
More concisely: The function `Prod.fst` from the cartesian product of two normed spaces over a nontrivially normed field, evaluated at a point `p`, has a Fréchet derivative equal to the continuous linear map `ContinuousLinearMap.fst` with respect to any filter on `p`.
|
differentiableWithinAt_pi
theorem differentiableWithinAt_pi :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7}
[inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
DifferentiableWithinAt 𝕜 Φ s x ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => Φ x i) s x
The theorem `differentiableWithinAt_pi` states that for a given point `x` in a set `s` of type `E`, a function `Φ` from `E` to a finite indexed type `F'` is differentiable at `x` within the set `s` with respect to a nontrivially normed field `𝕜` if and only if, for each index `i`, the function formed by applying `Φ` at `x` and then selecting the `i`th element is also differentiable at `x` within the set `s` with respect to `𝕜`. Here `DifferentiableWithinAt 𝕜 Φ s x` and `DifferentiableWithinAt 𝕜 (fun x => Φ x i) s x` both checking the existence of a derivative at the point `x` within the set `s`.
More concisely: A function `Φ` from a set `s` to a finite indexed type `F'` over a nontrivially normed field `𝕜` is differentiable at a point `x` within `s` if and only if the function formed by selecting the `i`th component of `Φ(x)` for each index `i` is also differentiable at `x` within `s`.
|
differentiableAt_fst
theorem differentiableAt_fst :
∀ {𝕜 : 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] {p : E × F},
DifferentiableAt 𝕜 Prod.fst p
The theorem `differentiableAt_fst` states that for any point `p` in the product space of two normed spaces `E` and `F` over a nontrivially normed field `𝕜`, the projection function `Prod.fst` that maps a pair to its first element is differentiable at `p`. In other words, it claims the existence of a derivative for the first projection function at any point of the product space.
More concisely: The projection function `Prod.fst` from the product of two normed spaces is differentiable at any point in the product space.
|
hasFDerivAtFilter_pi'
theorem hasFDerivAtFilter_pi' :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {x : E} {L : Filter E} {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7}
[inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}
{Φ' : E →L[𝕜] (i : ι) → F' i},
HasFDerivAtFilter Φ Φ' x L ↔
∀ (i : ι), HasFDerivAtFilter (fun x => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') x L
The theorem `hasFDerivAtFilter_pi'` establishes an equivalence for the existence of a derivative of a function at a point under a certain filter condition. Specifically, it states that for a function `Φ : E → (i : ι) → F' i`, where `E` is a normed additively commutative group over a nontrivially normed field `𝕜`, the function `Φ' : E →L[𝕜] (i : ι) → F' i` is the derivative of `Φ` at a point `x` under a filter `L` if and only if for all `i : ι`, the function `fun x => Φ x i` has a derivative at `x` under the filter `L` with respect to the composition of the projection map at `i` and `Φ'`. The projection map comes from the family of topological modules `F' i` which are defined as normed additively commutative groups over `𝕜`.
More concisely: The theorem `hasFDerivAtFilter_pi` states that a function `Φ : E → (i : ι) → F' i` has a derivative `Φ' : E →L[𝕜] (i : ι) → F' i` at a point `x` under a filter `L` if and only if for all `i : ι`, the function `fun x => Φ x i` has a derivative at `x` with respect to the composition of `Φ'` and the projection map at `i`, under filter `L`.
|
HasStrictFDerivAt.prod
theorem HasStrictFDerivAt.prod :
∀ {𝕜 : 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}
{f₂ : E → G} {f₂' : E →L[𝕜] G},
HasStrictFDerivAt f₁ f₁' x →
HasStrictFDerivAt f₂ f₂' x → HasStrictFDerivAt (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') x
This theorem states that given a nontrivial normed field `𝕜` and normed spaces `E`, `F`, and `G`, if a function `f₁` from `E` to `F` and a function `f₂` from `E` to `G` both have strict Frechet derivatives at a point `x` in `E`, then the function mapping `x` to the tuple `(f₁ x, f₂ x)` also has a strict Frechet derivative at `x`. The derivative of the tuple function is given by the continuous linear map that maps `x` to the tuple of the derivatives of `f₁` and `f₂` at `x`.
More concisely: Given a normed field `𝕜` and normed spaces `E`, `F`, and `G`, if functions `f₁: E → F` and `f₂: E → G` have strict Frechet derivatives at a point `x` in `E`, then the function mapping `x` to the tuple `(f₁ x, f₂ x)` from `E` to `F × G` has a strict Frechet derivative at `x`, given by the continuous linear map that maps `x` to the tuple of the derivatives of `f₁` and `f₂` at `x`.
|
differentiable_snd
theorem differentiable_snd :
∀ {𝕜 : 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],
Differentiable 𝕜 Prod.snd
The theorem `differentiable_snd` states that for any nontrivially normed field `𝕜` and any normed additive commutative groups `E` and `F` that are also normed spaces over `𝕜`, the function `Prod.snd` is differentiable at any point. In other words, the second projection function, which takes a pair and returns its second component, is differentiable everywhere when considered as a function between these normed spaces.
More concisely: The second projection function on the product of two normed spaces over a nontrivially normed field is differentiable.
|
HasFDerivWithinAt.prod
theorem HasFDerivWithinAt.prod :
∀ {𝕜 : 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} {f₂ : E → G} {f₂' : E →L[𝕜] G},
HasFDerivWithinAt f₁ f₁' s x →
HasFDerivWithinAt f₂ f₂' s x → HasFDerivWithinAt (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') s x
The theorem `HasFDerivWithinAt.prod` states that for any non-trivially normed field `𝕜`, normed additive commutative groups `E`, `F`, and `G`, along with normed spaces over `𝕜` for `E`, `F`, and `G`, given two functions `f₁ : E → F` and `f₂ : E → G` and their respective derivative functions `f₁' : E →L[𝕜] F` and `f₂' : E →L[𝕜] G`, as well as a point `x` in `E` and a set `s` of `E`. If `f₁` has derivative `f₁'` at `x` within `s` and `f₂` has derivative `f₂'` at `x` within `s`, then the function mapping `x` to the pair `(f₁ x, f₂ x)` also has a derivative at `x` within `s`, which is the product of `f₁'` and `f₂'` under the continuous linear map.
More concisely: If functions `f₁ : E → F` and `f₂ : E → G` with derivatives `f₁' : E →L[𝕜] F` and `f₂' : E →L[𝕜] G`, respectively, have derivatives at `x` within `s` in the normed spaces `E`, `F`, and `G` over a non-trivially normed field `𝕜`, then the function `(\x : E) => (f₁ x, f₂ x) : E → F × G` has a derivative at `x` within `s` equal to the product of `f₁'` and `f₂'` under the continuous linear map.
|
differentiable_fst
theorem differentiable_fst :
∀ {𝕜 : 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],
Differentiable 𝕜 Prod.fst
The theorem `differentiable_fst` states that for any non-trivially normed field `𝕜`, and any types `E` and `F` that form normed additive commutative groups and normed spaces over `𝕜`, the projection function `Prod.fst` is differentiable at all points. In other words, if we consider pairs of elements from `E` and `F`, the function that takes a pair and returns its first element is differentiable with respect to the field `𝕜`.
More concisely: For any non-trivially normed field `𝕜` and normed additive commutative groups and normed spaces `E` and `F` over `𝕜`, the projection function `Prod.fst` from `E × F` to `E` is differentiable.
|
hasFDerivAtFilter_snd
theorem hasFDerivAtFilter_snd :
∀ {𝕜 : 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] {p : E × F}
{L : Filter (E × F)}, HasFDerivAtFilter Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p L
This theorem states that for any nontrivially normed field `𝕜`, any normed add commutative group `E`, and any normed add commutative group `F`, the function `Prod.snd` has a derivative at a point `p` in the product space `E × F` with respect to a filter `L`. The derivative is given by the continuous linear map `ContinuousLinearMap.snd 𝕜 E F`. In mathematical terms, if `𝕜` is a nontrivially normed field and `E` and `F` are normed add commutative groups, then the function `Prod.snd : E × F → F` has a Fréchet derivative at any point in `E × F`, and the derivative is the continuous linear map `ContinuousLinearMap.snd 𝕜 E F`.
More concisely: For any nontrivially normed field `𝕜` and normed add commutative groups `E` and `F`, the function `Prod.snd : E × F → F` has a Fréchet derivative at every point in `E × F` as the continuous linear map `ContinuousLinearMap.snd 𝕜 E F`.
|