Hadamard's lemma for smooth functions on a normed space

Subtracting its value at x, a smooth real function on a real normed space is a combination of the coordinate functions of a finite basis, each relative to its value at x, with smooth coefficients whose values at x are the directional derivatives along the basis. More generally, subtracting its Taylor polynomial of order n at x, it is a combination of the products of n + 1 such relative coordinate functions, with smooth coefficients.

Main results

• ContMDiffMap.exists_hadamard_coords: Hadamard's lemma in the coordinates of a finite basis.
• ContMDiffMap.exists_taylor_coords: Taylor's formula of order n with the remainder written in the same coordinates.

theorem ContMDiffMap.exists_hadamard_coords {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} [Fintype ι] (f : ContMDiffMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) E ℝ ↑⊤) (x : E) (b : Module.Basis ι ℝ E) : ∃ (a : ι → ContMDiffMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) E ℝ ↑⊤), (∀ (i : ι), (a i) x = (fderiv ℝ (⇑f) x) (b i)) ∧ ∀ (y : E), f y - f x = ∑ i : ι, (a i) y * ((b.coord i) y - (b.coord i) x)

Hadamard's lemma in coordinates. Subtracting its value at x writes a smooth real function as a combination of the coordinate functions of any finitely-indexed basis, each taken relative to its own value at x, with smooth coefficients. At the base point those coefficients are the directional derivatives along the basis.

theorem ContMDiffMap.exists_taylor_coords {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} [Fintype ι] (f : ContMDiffMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) E ℝ ↑⊤) (x : E) (b : Module.Basis ι ℝ E) (n : ℕ) : ∃ (a : (Fin (n + 1) → ι) → ContMDiffMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) E ℝ ↑⊤), ∀ (y : E), f y = (∑ k ∈ Finset.range (n + 1), (↑k.factorial)⁻¹ * (iteratedFDeriv ℝ k (⇑f) x) fun (x_1 : Fin k) => y - x) + ∑ r : Fin (n + 1) → ι, (a r) y * ∏ j : Fin (n + 1), ((b.coord (r j)) y - (b.coord (r j)) x)

Taylor's formula in coordinates. A smooth real function on a finite-dimensional space is its Taylor polynomial of order n at x plus a combination of the products of n + 1 coordinate functions of any finitely-indexed basis, each taken relative to its value at x, with smooth coefficients. When the derivatives of order at most n vanish at x, this writes the function as a sum of products of n + 1 functions vanishing at x with smooth functions.