fderiv currying lemmas

Various lemmas related to fderiv on curried/uncurried functions.

theorem fderiv_uncurry {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (xy dxy : X × Y) (hf : DifferentiableAt 𝕜 (↿f) xy) : (fderiv 𝕜 (↿f) xy) dxy = (fderiv 𝕜 (fun (x : X) => f x xy.2) xy.1) dxy.1 + (fderiv 𝕜 (fun (x : Y) => f xy.1 x) xy.2) dxy.2

theorem fderiv_curry_fst {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X × Y → Z) (x : X) (y : Y) (h : DifferentiableAt 𝕜 f (x, y)) (dx : X) : (fderiv 𝕜 (fun (x' : X) => Function.curry f x' y) x) dx = (fderiv 𝕜 f (x, y)) (dx, 0)

theorem fderiv_curry_snd {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X × Y → Z) (x : X) (y : Y) (h : DifferentiableAt 𝕜 f (x, y)) (dy : Y) : (fderiv 𝕜 (Function.curry f x) y) dy = (fderiv 𝕜 f (x, y)) (0, dy)

theorem fderiv_uncurry_clm_comp {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (hf : Differentiable 𝕜 ↿f) : fderiv 𝕜 ↿f = fun (xy : X × Y) => (fderiv 𝕜 (fun (x : X) => f x xy.2) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y) + (fderiv 𝕜 (fun (x : Y) => f xy.1 x) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y)

theorem fderiv_wrt_prod_clm_comp {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X × Y → Z) (hf : Differentiable 𝕜 f) : fderiv 𝕜 f = fun (xy : X × Y) => (fderiv 𝕜 (fun (x' : X) => f (x', xy.2)) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y) + (fderiv 𝕜 (fun (y' : Y) => f (xy.1, y')) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y)

theorem fderiv_curry_clm_apply {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y →L[𝕜] Z) (y : Y) (x dx : X) (h : Differentiable 𝕜 f) : ((fderiv 𝕜 f x) dx) y = (fderiv 𝕜 (fun (x : X) => (f x) y) x) dx

theorem ContDiff.two_differentiable {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (hf : ContDiff 𝕜 2 ↿f) : Differentiable 𝕜 ↿f

Helper lemmas showing differentiability from ContDiff 𝕜 2 ↿f.

theorem ContDiff.uncurry {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x : X) (hf : ContDiff 𝕜 2 ↿f) : ContDiff 𝕜 2 (f x)

theorem ContDiff.two_fderiv_differentiable {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (hf : ContDiff 𝕜 2 ↿f) : Differentiable 𝕜 (fderiv 𝕜 ↿f)

theorem fderiv_uncurry_comp_fst {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (y : Y) (hf : Differentiable 𝕜 ↿f) : (fderiv 𝕜 fun (x' : X) => (↿f) (x', y)) = fun (x : X) => (fderiv 𝕜 (↿f) ((fun (x : X) => (x, y)) x)).comp (fderiv 𝕜 (fun (x : X) => (x, y)) x)

theorem fderiv_uncurry_comp_snd {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x : X) (hf : Differentiable 𝕜 ↿f) : (fderiv 𝕜 fun (y' : Y) => (↿f) (x, y')) = fun (y : Y) => (fderiv 𝕜 (↿f) ((fun (x_1 : Y) => (x, x_1)) y)).comp (fderiv 𝕜 (fun (x_1 : Y) => (x, x_1)) y)

theorem fderiv_curry_comp_fst {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x dx : X) (y : Y) (hf : Differentiable 𝕜 ↿f) : (fderiv 𝕜 (fun (x' : X) => f x' y) x) dx = (fderiv 𝕜 (↿f) ((fun (x : X) => (x, y)) x)) ((fderiv 𝕜 (fun (x : X) => (x, y)) x) dx)

theorem fderiv_curry_comp_snd {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x : X) (y dy : Y) (hf : Differentiable 𝕜 ↿f) : (fderiv 𝕜 (fun (y' : Y) => f x y') y) dy = (fderiv 𝕜 (↿f) ((fun (x_1 : Y) => (x, x_1)) y)) ((fderiv 𝕜 (fun (x_1 : Y) => (x, x_1)) y) dy)

theorem fderiv_inr_fst_clm {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] (x : X) (y : Y) : fderiv 𝕜 (fun (x_1 : Y) => (x, x_1)) y = ContinuousLinearMap.inr 𝕜 X Y

theorem fderiv_inl_snd_clm {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] (x : X) (y : Y) : fderiv 𝕜 (fun (x : X) => (x, y)) x = ContinuousLinearMap.inl 𝕜 X Y

theorem function_differentiableAt_fst {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x : X) (y : Y) (hf : Differentiable 𝕜 ↿f) : DifferentiableAt 𝕜 (fun (x' : X) => f x' y) x

theorem function_differentiableAt_snd {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x : X) (y : Y) (hf : Differentiable 𝕜 ↿f) : DifferentiableAt 𝕜 (fun (y' : Y) => f x y') y

theorem fderiv_uncurry_differentiable_fst {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (y : Y) (hf : ContDiff 𝕜 2 ↿f) : Differentiable 𝕜 (fderiv 𝕜 fun (x' : X) => (↿f) (x', y))

theorem fderiv_uncurry_differentiable_snd {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x : X) (hf : ContDiff 𝕜 2 ↿f) : Differentiable 𝕜 (fderiv 𝕜 fun (y' : Y) => (↿f) (x, y'))

theorem fderiv_uncurry_differentiable_fst_comp_snd {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x : X) (hf : ContDiff 𝕜 2 ↿f) : Differentiable 𝕜 fun (y' : Y) => fderiv 𝕜 (fun (x' : X) => (↿f) (x', y')) x

theorem fderiv_uncurry_differentiable_snd_comp_fst {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (y : Y) (hf : ContDiff 𝕜 2 ↿f) : Differentiable 𝕜 fun (x' : X) => fderiv 𝕜 (fun (y' : Y) => (↿f) (x', y')) y

theorem fderiv_curry_differentiableAt_fst_comp_snd {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x dx : X) (y : Y) (hf : ContDiff 𝕜 2 ↿f) : DifferentiableAt 𝕜 (fun (y' : Y) => (fderiv 𝕜 (fun (x' : X) => f x' y') x) dx) y

theorem fderiv_curry_differentiableAt_snd_comp_fst {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] (f : X → Y → Z) (x : X) (y dy : Y) (hf : ContDiff 𝕜 2 ↿f) : DifferentiableAt 𝕜 (fun (x' : X) => (fderiv 𝕜 (fun (y' : Y) => f x' y') y) dy) x

theorem fderiv_swap {𝕜 : Type} [NontriviallyNormedField 𝕜] {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] [IsRCLikeNormedField 𝕜] (f : X → Y → Z) (x dx : X) (y dy : Y) (hf : ContDiff 𝕜 2 ↿f) : (fderiv 𝕜 (fun (x' : X) => (fderiv 𝕜 (fun (y' : Y) => f x' y') y) dy) x) dx = (fderiv 𝕜 (fun (y' : Y) => (fderiv 𝕜 (fun (x' : X) => f x' y') x) dx) y) dy