Differentiability criteria

The derivative fderiv 𝕜 f is totalized: it is 0 where f is not differentiable. So a nonzero derivative certifies differentiability, as differentiableAt_of_deriv_ne_zero does for functions of one variable. Likewise, two differentiable independent linear combinations of two scalar functions recover both functions as differentiable.

Main results

• TauCeti.differentiableAt_of_fderiv_ne_zero: a function is differentiable wherever its derivative does not vanish.
• TauCeti.differentiableAt_and_of_differentiableAt_comb: if two combinations a F + b G and c F + d G with a d - b c ≠ 0 are differentiable at a point, so are F and G.

theorem TauCeti.differentiableAt_of_fderiv_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : fderiv 𝕜 f x ≠ 0) : DifferentiableAt 𝕜 f x

A function is differentiable wherever its totalized derivative does not vanish.

theorem TauCeti.differentiableAt_and_of_differentiableAt_comb {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {F G : E → 𝕜} {a b c d : 𝕜} (hdet : a * d - b * c ≠ 0) (hA : DifferentiableAt 𝕜 (fun (y : E) => a * F y + b * G y) x) (hB : DifferentiableAt 𝕜 (fun (y : E) => c * F y + d * G y) x) : DifferentiableAt 𝕜 F x ∧ DifferentiableAt 𝕜 G x

If two combinations a F + b G and c F + d G with a d - b c ≠ 0 are differentiable at a point, then so are F and G: they are recovered by inverting the coefficient matrix.