From now on, $f$ denotes an infinitely differentiable function from $[0,1]$ to $\mathbb{R}$. We assume that there exists a unique point $x_0 \in [0,1]$ where $f'$ vanishes. We also assume that $f''(x_0) > 0$. We are also given an infinitely differentiable function $g : [0,1] \rightarrow \mathbb{R}$. For all $x \in [x_0, 1]$, we define $$h(x) = \sqrt{|f(x) - f(x_0)|}$$ We admit that the bijection $h : [x_0, 1] \rightarrow [0, h(1)]$ admits an inverse application $h^{-1} : [0, h(1)] \rightarrow [x_0, 1]$ that is infinitely differentiable. We assume that $x_0 \in ]0,1[$. Show that, as $t \rightarrow +\infty$, $$\int_0^1 g(x) \sin(tf(x)) \mathrm{d}x = g(x_0) \sin\left(tf(x_0) + \frac{\pi}{4}\right) \sqrt{\frac{2\pi}{tf''(x_0)}} + O\left(\frac{1}{t}\right)$$
From now on, $f$ denotes an infinitely differentiable function from $[0,1]$ to $\mathbb{R}$. We assume that there exists a unique point $x_0 \in [0,1]$ where $f'$ vanishes. We also assume that $f''(x_0) > 0$. We are also given an infinitely differentiable function $g : [0,1] \rightarrow \mathbb{R}$.
For all $x \in [x_0, 1]$, we define
$$h(x) = \sqrt{|f(x) - f(x_0)|}$$
We admit that the bijection $h : [x_0, 1] \rightarrow [0, h(1)]$ admits an inverse application $h^{-1} : [0, h(1)] \rightarrow [x_0, 1]$ that is infinitely differentiable.
We assume that $x_0 \in ]0,1[$. Show that, as $t \rightarrow +\infty$,
$$\int_0^1 g(x) \sin(tf(x)) \mathrm{d}x = g(x_0) \sin\left(tf(x_0) + \frac{\pi}{4}\right) \sqrt{\frac{2\pi}{tf''(x_0)}} + O\left(\frac{1}{t}\right)$$