# How to prove a Theorem numerically

Setting: I have a function $$f$$ of 4 real variables $$(x,y,w,z)$$ in $$\mathbb R^4$$. The function $$f$$ satisfies $$f(0,y,w,z)=1$$ and $$-I \preceq \mathsf{H}f(x,y,w,z) \preceq I$$, $$\forall x,y,w,z \in [0,1]$$, where $$\mathsf{H}$$ denotes the Hessian operator. Otherwise, the function $$f$$ does not have any special structure in any of the variables (i.e. no monoticity, convexity, etc). (The analytical expression of $$f$$ is quite involved and very hard to study analytically.)

Goal: I want to show that $$f(\mathbf{v})\leq 1$$ for all $$\mathbf{v}\triangleq(x,y,w,z)$$ in $$[0,1]^4$$, by showing that $$\partial f /\partial x(\mathbf{v})\leq0$$, for all $$\mathbf{v}$$ in $$[0,1]^4$$.

Since $$f(0,y,w,z)=1$$, for all $$y,w,z\in [0,1]^3$$, showing that $$\partial f /\partial x(\mathbf{v})\leq0$$, for all $$\mathbf{v}$$ in $$[0,1]^4$$, will certainly get me what I want. However, the expression of $$\partial f/\partial x$$ is very involved making it very hard to show any inequality analytically.

Desired Strategy: Numerical optimization suggests that $$\partial f /\partial x(\mathbf{v})\leq -0.1$$. Given that I also know that $$-I \preceq \mathsf{H}f \preceq I$$, my strategy was to evalutate $$\partial f /\partial x(\mathbf{v})$$ on a fine enough grid in $$[0,1]^4$$ and then invoke Taylor's Theorem to argue that $$\partial f /\partial x (\mathbf v)<0$$, for all $$\mathbf{v} \in[0,1]^4$$. Would this be an acceptable proof?

Side Note: The result that I am chasing will ultimately be part of a Theorem in a research article (my field is maths/computer science). And so I want to know if my strategy above for proving the result is still acceptable'' even though it relies on the numerical evaluating of a function (in this case $$\partial f/\partial x$$) on a (large) set of grid points.

Conterexample: $$f(x,y,z,w):=1+\frac{1}{2}x^2.$$ Then $$f(0,y,z,w)=1$$ and $$\partial^2 f /\partial x^2=1.$$
But $$f(1,0,0,0,)=\frac{3}{2}>1.$$