taylor mean remainder thm

Stream: new members

[Abu Al Hassan]

Hello, I would like some help with the following.

My goal is:

⊢ ∃ (p : ℝ → formal_multilinear_series ℝ ℝ ℝ), has_ftaylor_series_up_to_on ↑m g p (set.Icc 0 α)

I want to give it a function p, which is the Taylor series of a function g.

f : E → ℝ,
x_star : E,
α : ℝ,
d : E,
f' : E → (E →L[ℝ] ℝ),
h_stationary : f' x_star = 0
h_deriv_exists : ∀ (y : E), y ∈ u → has_fderiv_at f (f' y) y,
h_twice_continuous_diffable : cont_diff_on ℝ 2 f u,
g : ℝ → ℝ := λ (α : ℝ), f (x_star + α • d),

I want to set p to be the taylor series of g upto order 1, i have tried:
set p : ℝ → ℝ := λ α, (f (x_star)) + (matrix.dot_product (f' (x_star + (α • d))) d) with hp, which gives an error. Matrix_product isn't working for me as I am using bilinear maps (look at structure of f').

I have also tried use (taylor_within g 1 (set.Icc 0 α) 0), and use (taylor_within f 1 (segment ℝ x_star (x_star + (α • d))) x_star),. Which both fail to instantiate goal such as:
failed to instantiate goal with taylor_within f 1 (segment (frozen_name real) x_star ((frozen_name has_add.add) x_star ((frozen_name has_smul.smul) α d))) x_star

I would appreciate some help in defining f to be the taylor series of g upto order 1

[Abu Al Hassan]

Some context: I am currently trying to prove:
cont_diff_on ℝ 1 g (set.Icc 0 α) so later i can use theorem taylor_mean_remainder_lagrange on g.

[Ruben Van de Velde]

Have you read #mwe?

[Eric Wieser]

I would guess that instead of matrix.dot_product (f' (x_star + (α • d))) d) you just want f' (x_star + (α • d)) d

[Eric Wieser]

The frechet derivative f' in a sense "includes the dot product" you'd write when using $a \cdot \nabla f$

[Abu Al Hassan]

Hi Eric, thank you, that worked. Sorry for the late reply, I realised I needed to make p: ℝ → formal_multilinear_series ℝ ℝ ℝ so went off on quite a journey figuring out the way of my proof.