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$.
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 admit the identities: $$\lim_{a \rightarrow +\infty} \int_0^a \sin(x^2) \mathrm{d}x = \lim_{a \rightarrow +\infty} \int_0^a \cos(x^2) \mathrm{d}x = \frac{\sqrt{2\pi}}{4}$$
Show that, as $t \rightarrow +\infty$, $$\int_{x_0}^1 \sin(tf(x)) \mathrm{d}x = \sin\left(tf(x_0) + \frac{\pi}{4}\right) \sqrt{\frac{\pi}{2tf''(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 \left[ 0,1 \left[ \right. \right.$ where $f ^ { \prime }$ vanishes. We also assume that $f ^ { \prime \prime } \left( x _ { 0 } \right) > 0$. We are also given an infinitely differentiable function $g : [ 0,1 ] \rightarrow \mathbb { R }$.
For all $x \in \left[ x _ { 0 } , 1 \right]$, we define $$h ( x ) = \sqrt { \left| f ( x ) - f \left( x _ { 0 } \right) \right| }$$ We admit that the bijection $$h : \left\{ \begin{array} { c c c } { \left[ x _ { 0 } , 1 \right] } & \rightarrow & { [ 0 , h ( 1 ) ] } \\ x & \mapsto & h ( x ) \end{array} \right.$$ admits an inverse map $h ^ { - 1 } : [ 0 , h ( 1 ) ] \rightarrow \left[ x _ { 0 } , 1 \right]$ that is infinitely differentiable.
Show that, as $t \rightarrow + \infty$, $$\int _ { x _ { 0 } } ^ { 1 } \sin ( t f ( x ) ) \mathrm { d } x = \sin \left( t f \left( x _ { 0 } \right) + \frac { \pi } { 4 } \right) \sqrt { \frac { \pi } { 2 t f ^ { \prime \prime } \left( x _ { 0 } \right) } } + O \left( \frac { 1 } { t } \right)$$