about fderiv and integral

Stream: maths

[Chenyi Li]

Assume f is C^1 in \mathbb{R}^d, how to prove f(y)- f(x) = \int_0^1 \nabla f(x+t(y-x))^T (y-x) dt, or easily consider d=1?

[Chenyi Li]

I am confused about the type of the fderiv in lean and I am curious about how to transform the type of the fderiv to a type that can easily do integral or rather, it can be done with the fderiv type $\mathbb{R} \to L[\mathbb{k}] \mathbb{R}$ ?

[Yury G. Kudryashov]

Could you please use double dollars around LaTeX formulas and #backticks around code?

[Yury G. Kudryashov]

What is the domain and codomain of f?

[Chenyi Li]

Assume f is $C^1$ in $\mathbb{R}^d$, how to prove $f(y)- f(x) = \int_0^1 \nabla f(x+t(y-x))^T (y-x) dt$, or easily consider d=1?

[Chenyi Li]

The domain is $\mathbb{R}^d$, codomain is $\mathbb{R}$. f is a continuous differentiable function. i.e. $f: \mathbb{R}^d \to \mathbb{R}$

[Yury G. Kudryashov]

You should consider $g(t)=f(x+t(y-x))$.

[Yury G. Kudryashov]

Then apply something like docs#interval_integral.integral_deriv_eq_sub (exact lemma may depend on how you write your assumptions in Lean).

[Yury G. Kudryashov]

You will need deriv (λ t : ℝ, f (x + t • (y - x))) t₀ = fderiv ℝ f (x + t₀ • (y - x)) (y - x). Either we have it somewhere near docs#deriv, or you can prove it using generic lemmas from that file.