Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong, Tomáš Skřivan, Joseph Tooby-Smith
-/
module
public import Mathlib.Analysis.Calculus.FDeriv.Symmetricfderiv currying lemmas
Various lemmas related to fderiv on curried/uncurried functions.
@[expose] public section𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zxy:X × Ydxy:X × Yhf:DifferentiableAt 𝕜 (↿f) xyhx:(fun x => f x xy.2) = ↿f ∘ fun x' => (x', xy.2)hy:(fun x => f xy.1 x) = ↿f ∘ fun y' => (xy.1, y')⊢ dxy =
((fderiv 𝕜 (fun x' => x') xy.1).prod (fderiv 𝕜 (fun x' => xy.2) xy.1)) dxy.1 +
((fderiv 𝕜 (fun y' => xy.1) xy.2).prod (fderiv 𝕜 (fun y' => y') xy.2)) dxy.2
All goals completed! 🐙𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zx:Xy:Yh:DifferentiableAt 𝕜 f (x, y)dx:Xh1:f = ↿(Function.curry f)⊢ (fderiv 𝕜 (fun x' => Function.curry f x' y) x) dx =
(fderiv 𝕜 (fun x_1 => Function.curry f x_1 (x, y).2) (x, y).1) (dx, 0).1 +
(fderiv 𝕜 (fun x_1 => Function.curry f (x, y).1 x_1) (x, y).2) (dx, 0).2𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zx:Xy:Yh:DifferentiableAt 𝕜 f (x, y)dx:Xh1:f = ↿(Function.curry f)⊢ DifferentiableAt 𝕜 ↿(Function.curry f) (x, y)
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zx:Xy:Yh:DifferentiableAt 𝕜 f (x, y)dx:Xh1:f = ↿(Function.curry f)⊢ DifferentiableAt 𝕜 ↿(Function.curry f) (x, y)
All goals completed! 🐙𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zx:Xy:Yh:DifferentiableAt 𝕜 f (x, y)dy:Yh1:f = ↿(Function.curry f)⊢ (fderiv 𝕜 (Function.curry f x) y) dy =
(fderiv 𝕜 (fun x_1 => Function.curry f x_1 (x, y).2) (x, y).1) (0, dy).1 +
(fderiv 𝕜 (fun x_1 => Function.curry f (x, y).1 x_1) (x, y).2) (0, dy).2𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zx:Xy:Yh:DifferentiableAt 𝕜 f (x, y)dy:Yh1:f = ↿(Function.curry f)⊢ DifferentiableAt 𝕜 ↿(Function.curry f) (x, y)
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zx:Xy:Yh:DifferentiableAt 𝕜 f (x, y)dy:Yh1:f = ↿(Function.curry f)⊢ (fderiv 𝕜 (Function.curry f x) y) dy = (fderiv 𝕜 (fun x_1 => f (x, x_1)) y) dy𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zx:Xy:Yh:DifferentiableAt 𝕜 f (x, y)dy:Yh1:f = ↿(Function.curry f)⊢ DifferentiableAt 𝕜 ↿(Function.curry f) (x, y)
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zx:Xy:Yh:DifferentiableAt 𝕜 f (x, y)dy:Yh1:f = ↿(Function.curry f)⊢ DifferentiableAt 𝕜 ↿(Function.curry f) (x, y)
All goals completed! 🐙𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zhf:Differentiable 𝕜 ↿fxy:X × Ydxy:X × Y⊢ (fderiv 𝕜 (fun x => f x xy.2) xy.1) dxy.1 + (fderiv 𝕜 (fun x => f xy.1 x) xy.2) dxy.2 =
(fderiv 𝕜 (fun x => f x xy.2) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun x => f xy.1 x) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
dxy𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zhf:Differentiable 𝕜 ↿fxy:X × Ydxy:X × Y⊢ DifferentiableAt 𝕜 (↿f) xy
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zhf:Differentiable 𝕜 ↿fxy:X × Ydxy:X × Y⊢ DifferentiableAt 𝕜 (↿f) xy
All goals completed! 🐙lemma fderiv_wrt_prod {f : X × Y → Z} {xy} (hf : DifferentiableAt 𝕜 f xy) :
fderiv 𝕜 f xy
=
(fderiv 𝕜 (fun x' => f (x',xy.2)) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
+
(fderiv 𝕜 (fun y' => f (xy.1,y')) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) := 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zxy:X × Yhf:DifferentiableAt 𝕜 f xy⊢ fderiv 𝕜 f xy =
fderiv 𝕜 (fun x' => f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zxy:X × Yhf:DifferentiableAt 𝕜 f xy⊢ ∀ (x : X × Y),
(fderiv 𝕜 f xy) x =
(fderiv 𝕜 (fun x' => f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
x; 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X × Y → Zxy:X × Yhf:DifferentiableAt 𝕜 f xydx:Xdy:Y⊢ (fderiv 𝕜 f xy) (dx, dy) =
(fderiv 𝕜 (fun x' => f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(dx, dy)
All goals completed! 🐙lemma fderiv_wrt_prod_clm_comp (f : X × Y → Z) (hf : Differentiable 𝕜 f) :
fderiv 𝕜 f
=
fun xy =>
(fderiv 𝕜 (fun x' => f (x',xy.2)) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
+
(fderiv 𝕜 (fun y' => f (xy.1,y')) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) :=
fderiv_uncurry_clm_comp (fun x y => f (x,y)) hf𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y →L[𝕜] Zy:Yx:Xdx:Xh:Differentiable 𝕜 f⊢ ((fderiv 𝕜 f x) dx) y = (f x ∘SL fderiv 𝕜 (fun x => y) x + (fderiv 𝕜 f x).flip y) dx𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y →L[𝕜] Zy:Yx:Xdx:Xh:Differentiable 𝕜 f⊢ DifferentiableAt 𝕜 f x𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y →L[𝕜] Zy:Yx:Xdx:Xh:Differentiable 𝕜 f⊢ DifferentiableAt 𝕜 (fun x => y) x 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y →L[𝕜] Zy:Yx:Xdx:Xh:Differentiable 𝕜 f⊢ ((fderiv 𝕜 f x) dx) y = (f x ∘SL fderiv 𝕜 (fun x => y) x + (fderiv 𝕜 f x).flip y) dx𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y →L[𝕜] Zy:Yx:Xdx:Xh:Differentiable 𝕜 f⊢ DifferentiableAt 𝕜 f x𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y →L[𝕜] Zy:Yx:Xdx:Xh:Differentiable 𝕜 f⊢ DifferentiableAt 𝕜 (fun x => y) x first | All goals completed! 🐙 | All goals completed! 🐙𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => ↿f (x', y)) = ↿f ∘ fun x => (x, y)x:X⊢ DifferentiableAt 𝕜 ↿f (x, y)𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => ↿f (x', y)) = ↿f ∘ fun x => (x, y)x:X⊢ DifferentiableAt 𝕜 (fun x => (x, y)) x
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => ↿f (x', y)) = ↿f ∘ fun x => (x, y)x:X⊢ DifferentiableAt 𝕜 ↿f (x, y) All goals completed! 🐙
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => ↿f (x', y)) = ↿f ∘ fun x => (x, y)x:X⊢ DifferentiableAt 𝕜 (fun x => (x, y)) x All goals completed! 🐙𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => ↿f (x, y')) = ↿f ∘ fun x_1 => (x, x_1)y:Y⊢ DifferentiableAt 𝕜 ↿f (x, y)𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => ↿f (x, y')) = ↿f ∘ fun x_1 => (x, x_1)y:Y⊢ DifferentiableAt 𝕜 (fun x_1 => (x, x_1)) y
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => ↿f (x, y')) = ↿f ∘ fun x_1 => (x, x_1)y:Y⊢ DifferentiableAt 𝕜 ↿f (x, y) All goals completed! 🐙
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => ↿f (x, y')) = ↿f ∘ fun x_1 => (x, x_1)y:Y⊢ DifferentiableAt 𝕜 (fun x_1 => (x, x_1)) y All goals completed! 🐙𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xdx:Xy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ (fderiv 𝕜 ↿f (x, y) ∘SL fderiv 𝕜 (fun x => (x, y)) x) dx =
(fderiv 𝕜 (↿f) ((fun x => (x, y)) x)) ((fderiv 𝕜 (fun x => (x, y)) x) dx)𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xdx:Xy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ DifferentiableAt 𝕜 ↿f (x, y)𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xdx:Xy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ DifferentiableAt 𝕜 (fun x => (x, y)) x
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xdx:Xy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ DifferentiableAt 𝕜 ↿f (x, y)𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xdx:Xy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ DifferentiableAt 𝕜 (fun x => (x, y)) x
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xdx:Xy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ DifferentiableAt 𝕜 ↿f (x, y) All goals completed! 🐙
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xdx:Xy:Yhf:Differentiable 𝕜 ↿fhl:∀ (y : Y), (fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ DifferentiableAt 𝕜 (fun x => (x, y)) x All goals completed! 🐙𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Ydy:Yhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ (fderiv 𝕜 ↿f (x, y) ∘SL fderiv 𝕜 (fun x_1 => (x, x_1)) y) dy =
(fderiv 𝕜 (↿f) ((fun x_1 => (x, x_1)) y)) ((fderiv 𝕜 (fun x_1 => (x, x_1)) y) dy)𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Ydy:Yhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ DifferentiableAt 𝕜 ↿f (x, y)𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Ydy:Yhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ DifferentiableAt 𝕜 (fun x_1 => (x, x_1)) y
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Ydy:Yhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ DifferentiableAt 𝕜 ↿f (x, y)𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Ydy:Yhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ DifferentiableAt 𝕜 (fun x_1 => (x, x_1)) y
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Ydy:Yhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ DifferentiableAt 𝕜 ↿f (x, y) All goals completed! 🐙
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Ydy:Yhf:Differentiable 𝕜 ↿fhl:∀ (x : X), (fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ DifferentiableAt 𝕜 (fun x_1 => (x, x_1)) y All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ DifferentiableAt 𝕜 (↿f ∘ fun x => (x, y)) x
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ Differentiable 𝕜 (↿f ∘ fun x => (x, y))
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ Differentiable 𝕜 ↿f𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ Differentiable 𝕜 fun x => (x, y) 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ Differentiable 𝕜 ↿f𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun x' => f x' y) = ↿f ∘ fun x => (x, y)⊢ Differentiable 𝕜 fun x => (x, y) All goals completed! 🐙𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ DifferentiableAt 𝕜 (↿f ∘ fun x_1 => (x, x_1)) y
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ Differentiable 𝕜 (↿f ∘ fun x_1 => (x, x_1))
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ Differentiable 𝕜 ↿f𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ Differentiable 𝕜 fun x_1 => (x, x_1) 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ Differentiable 𝕜 ↿f𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Yhf:Differentiable 𝕜 ↿fhl:(fun y' => f x y') = ↿f ∘ fun x_1 => (x, x_1)⊢ Differentiable 𝕜 fun x_1 => (x, x_1) All goals completed! 🐙@[fun_prop]
lemma fderiv_uncurry_differentiable_fst (f : X → Y → Z) (y : Y) (hf : ContDiff 𝕜 2 ↿f) :
Differentiable 𝕜 (fderiv 𝕜 fun x' => (↿f) (x', y)) := 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zy:Yhf:ContDiff 𝕜 2 ↿f⊢ Differentiable 𝕜 (fderiv 𝕜 fun x' => ↿f (x', y))
All goals completed! 🐙@[fun_prop]
lemma fderiv_uncurry_differentiable_snd (f : X → Y → Z) (x : X) (hf : ContDiff 𝕜 2 ↿f) :
Differentiable 𝕜 (fderiv 𝕜 fun y' => (↿f) (x, y')) := 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xhf:ContDiff 𝕜 2 ↿f⊢ Differentiable 𝕜 (fderiv 𝕜 fun y' => ↿f (x, y'))
All goals completed! 🐙@[fun_prop]
lemma fderiv_uncurry_differentiable_fst_comp_snd (f : X → Y → Z) (x : X) (hf : ContDiff 𝕜 2 ↿f) :
Differentiable 𝕜 (fun y' => fderiv 𝕜 (fun x' => (↿f) (x', y')) x) := 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xhf:ContDiff 𝕜 2 ↿f⊢ Differentiable 𝕜 fun y' => fderiv 𝕜 (fun x' => ↿f (x', y')) x
All goals completed! 🐙@[fun_prop]
lemma fderiv_uncurry_differentiable_fst_comp_snd_apply (f : X → Y → Z) (x δx : X)
(hf : ContDiff 𝕜 2 ↿f) :
Differentiable 𝕜 (fun y' => fderiv 𝕜 (fun x' => (↿f) (x', y')) x δx) := 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xδx:Xhf:ContDiff 𝕜 2 ↿f⊢ Differentiable 𝕜 fun y' => (fderiv 𝕜 (fun x' => ↿f (x', y')) x) δx
All goals completed! 🐙@[fun_prop]
lemma fderiv_uncurry_differentiable_snd_comp_fst (f : X → Y → Z) (y : Y) (hf : ContDiff 𝕜 2 ↿f) :
Differentiable 𝕜 (fun x' => fderiv 𝕜 (fun y' => (↿f) (x', y')) y) := 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zy:Yhf:ContDiff 𝕜 2 ↿f⊢ Differentiable 𝕜 fun x' => fderiv 𝕜 (fun y' => ↿f (x', y')) y
All goals completed! 🐙@[fun_prop]
lemma fderiv_uncurry_differentiable_snd_comp_fst_apply (f : X → Y → Z) (y δy : Y)
(hf : ContDiff 𝕜 2 ↿f) :
Differentiable 𝕜 (fun x' => fderiv 𝕜 (fun y' => (↿f) (x', y')) y δy) := 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zy:Yδy:Yhf:ContDiff 𝕜 2 ↿f⊢ Differentiable 𝕜 fun x' => (fderiv 𝕜 (fun y' => ↿f (x', y')) y) δy
All goals completed! 🐙@[fun_prop]
lemma fderiv_curry_differentiableAt_fst_comp_snd (f : X → Y → Z) (x dx : X) (y : Y)
(hf : ContDiff 𝕜 2 ↿f) :
DifferentiableAt 𝕜 (fun y' => (fderiv 𝕜 (fun x' => f x' y') x) dx) y := 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xdx:Xy:Yhf:ContDiff 𝕜 2 ↿f⊢ DifferentiableAt 𝕜 (fun y' => (fderiv 𝕜 (fun x' => f x' y') x) dx) y
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xdx:Xy:Yhf:ContDiff 𝕜 2 ↿f⊢ Differentiable 𝕜 fun y' => (fderiv 𝕜 (fun x' => f x' y') x) dx
All goals completed! 🐙lemma fderiv_curry_differentiableAt_snd_comp_fst (f : X → Y → Z) (x : X) (y dy : Y)
(hf : ContDiff 𝕜 2 ↿f) :
DifferentiableAt 𝕜 (fun x' => (fderiv 𝕜 (fun y' => f x' y') y) dy) x := 𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿f⊢ DifferentiableAt 𝕜 (fun x' => (fderiv 𝕜 (fun y' => f x' y') y) dy) x
𝕜:Type u_1inst✝⁶:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace 𝕜 Xinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace 𝕜 Yinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace 𝕜 Zf:X → Y → Zx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿f⊢ Differentiable 𝕜 fun x' => (fderiv 𝕜 (fun y' => f x' y') y) dy
All goals completed! 🐙𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(fderiv 𝕜
(fun x =>
(fderiv 𝕜 (fun x' => ↿f (x', y)) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(0, dy))
x)
dx =
(fderiv 𝕜
(fun x_1 =>
(fderiv 𝕜 (fun x' => ↿f (x', x_1)) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) x_1 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(dx, 0))
y)
dy⊢ (fderiv 𝕜 (fun x' => (fderiv 𝕜 (fun y' => f x' y') y) dy) x) dx =
(fderiv 𝕜 (fun y' => (fderiv 𝕜 (fun x' => f x' y') x) dx) y) dy𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(fderiv 𝕜
(fun x =>
(fderiv 𝕜 (fun x' => ↿f (x', y)) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(0, dy))
x)
dx =
((fderiv 𝕜
(fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y)
y)
dy)
(dx, 0)⊢ Differentiable 𝕜 fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:((fderiv 𝕜
(fun x' =>
fderiv 𝕜 (fun x' => ↿f (x', y)) x' ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x', y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y)
x)
dx)
(0, dy) =
((fderiv 𝕜
(fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y)
y)
dy)
(dx, 0)⊢ Differentiable 𝕜 fun x' =>
fderiv 𝕜 (fun x' => ↿f (x', y)) x' ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x', y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(dx, 0))
(0, dy) =
(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(0, dy))
(dx, 0)⊢ Differentiable 𝕜 ↿f𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:((fderiv 𝕜 (fderiv 𝕜 ↿f) (x, y)) (dx, 0)) (0, dy) = ((fderiv 𝕜 (fderiv 𝕜 ↿f) (x, y)) (0, dy)) (dx, 0)⊢ Differentiable 𝕜 (fderiv 𝕜 ↿f)
𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(fderiv 𝕜 (fun x => (fderiv 𝕜 (fun y' => ↿f (x, y')) y) dy) x) dx =
(fderiv 𝕜 (fun x_1 => (fderiv 𝕜 (fun x' => ↿f (x', x_1)) x) dx) y) dy⊢ (fderiv 𝕜 (fun x' => (fderiv 𝕜 (fun y' => f x' y') y) dy) x) dx =
(fderiv 𝕜 (fun y' => (fderiv 𝕜 (fun x' => f x' y') x) dx) y) dy𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(fderiv 𝕜
(fun x =>
(fderiv 𝕜 (fun x' => ↿f (x', y)) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(0, dy))
x)
dx =
((fderiv 𝕜
(fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y)
y)
dy)
(dx, 0)⊢ Differentiable 𝕜 fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:((fderiv 𝕜
(fun x' =>
fderiv 𝕜 (fun x' => ↿f (x', y)) x' ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x', y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y)
x)
dx)
(0, dy) =
((fderiv 𝕜
(fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y)
y)
dy)
(dx, 0)⊢ Differentiable 𝕜 fun x' =>
fderiv 𝕜 (fun x' => ↿f (x', y)) x' ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x', y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(dx, 0))
(0, dy) =
(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(0, dy))
(dx, 0)⊢ Differentiable 𝕜 ↿f𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:((fderiv 𝕜 (fderiv 𝕜 ↿f) (x, y)) (dx, 0)) (0, dy) = ((fderiv 𝕜 (fderiv 𝕜 ↿f) (x, y)) (0, dy)) (dx, 0)⊢ Differentiable 𝕜 (fderiv 𝕜 ↿f)
𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(fderiv 𝕜
(fun x =>
(fderiv 𝕜 (fun x' => ↿f (x', y)) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(0, dy))
x)
dx =
((fderiv 𝕜
(fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y)
y)
dy)
(dx, 0)⊢ Differentiable 𝕜 fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:((fderiv 𝕜
(fun x' =>
fderiv 𝕜 (fun x' => ↿f (x', y)) x' ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x', y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y)
x)
dx)
(0, dy) =
((fderiv 𝕜
(fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y)
y)
dy)
(dx, 0)⊢ Differentiable 𝕜 fun x' =>
fderiv 𝕜 (fun x' => ↿f (x', y)) x' ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x', y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(dx, 0))
(0, dy) =
(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(0, dy))
(dx, 0)⊢ Differentiable 𝕜 ↿f𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:((fderiv 𝕜 (fderiv 𝕜 ↿f) (x, y)) (dx, 0)) (0, dy) = ((fderiv 𝕜 (fderiv 𝕜 ↿f) (x, y)) (0, dy)) (dx, 0)⊢ Differentiable 𝕜 (fderiv 𝕜 ↿f)
/- Start of differentiability conditions. -/
𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(fderiv 𝕜
(fun x =>
(fderiv 𝕜 (fun x' => ↿f (x', y)) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(0, dy))
x)
dx =
((fderiv 𝕜
(fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y)
y)
dy)
(dx, 0)⊢ Differentiable 𝕜 fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y All goals completed! 🐙
𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:((fderiv 𝕜
(fun x' =>
fderiv 𝕜 (fun x' => ↿f (x', y)) x' ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x', y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y)
x)
dx)
(0, dy) =
((fderiv 𝕜
(fun y' =>
fderiv 𝕜 (fun x' => ↿f (x', y')) x ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x, y')) y' ∘SL ContinuousLinearMap.snd 𝕜 X Y)
y)
dy)
(dx, 0)⊢ Differentiable 𝕜 fun x' =>
fderiv 𝕜 (fun x' => ↿f (x', y)) x' ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => ↿f (x', y')) y ∘SL ContinuousLinearMap.snd 𝕜 X Y All goals completed! 🐙
𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(dx, 0))
(0, dy) =
(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(0, dy))
(dx, 0)⊢ Differentiable 𝕜 ↿f exact hf.differentiable (𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(dx, 0))
(0, dy) =
(((fun xy =>
fderiv 𝕜 (fun x' => fderiv 𝕜 ↿f (x', xy.2)) xy.1 ∘SL ContinuousLinearMap.fst 𝕜 X Y +
fderiv 𝕜 (fun y' => fderiv 𝕜 ↿f (xy.1, y')) xy.2 ∘SL ContinuousLinearMap.snd 𝕜 X Y)
(x, y))
(0, dy))
(dx, 0)⊢ 2 ≠ 0 All goals completed! 🐙)
𝕜:Type u_1inst✝⁷:NontriviallyNormedField 𝕜X:Type u_2Y:Type u_3Z:Type u_4inst✝⁶:NormedAddCommGroup Xinst✝⁵:NormedSpace 𝕜 Xinst✝⁴:NormedAddCommGroup Yinst✝³:NormedSpace 𝕜 Yinst✝²:NormedAddCommGroup Zinst✝¹:NormedSpace 𝕜 Zinst✝:IsRCLikeNormedField 𝕜f:X → Y → Zx:Xdx:Xy:Ydy:Yhf:ContDiff 𝕜 2 ↿fhf':IsSymmSndFDerivAt 𝕜 ↿f (x, y)h:((fderiv 𝕜 (fderiv 𝕜 ↿f) (x, y)) (dx, 0)) (0, dy) = ((fderiv 𝕜 (fderiv 𝕜 ↿f) (x, y)) (0, dy)) (dx, 0)⊢ Differentiable 𝕜 (fderiv 𝕜 ↿f) All goals completed! 🐙