Bound on an intermediate derivative of a smooth map on a half-plane by its neighbouring derivatives

Let $F$ be a real normed space, $s_0\in\mathbb{R}$, and let $f:\mathbb{R}\times\mathbb{R}\to F$ be $C^\infty$ on the open half-plane $(s_0,\infty)\times\mathbb{R}$. Let $j\in\mathbb{N}$, let $p=(p_1,p_2)$ with $p_1>s_0$, and let $A,B\in\mathbb{R}$, $h>0$. Suppose that for every $q$ with $q_1\ge p_1$ we have $\|D^jf(q)\|\le A$ and $\|D^{j+2}f(q)\|\le B$. Then

This is a pointwise interpolation inequality for consecutive derivative orders on a half-plane, using only the region to the right of the point. It is meant for estimating derivatives of maps defined on cylindrical ends.

Formalization Note $D^kf$ is iteratedFDeriv ℝ k f, with the norm of continuous multilinear maps on ℝ × ℝ (sup norm). The half-plane is Set.Ioi s₀ ×ˢ Set.univ, and the bounds are assumed on {q | p.1 ≤ q.1}.