HermiteMajorant

Abstract

Two double contacts and a nonnegative fourth derivative force nonnegativity on the positive half-line.

Theorem 1.1 (Fourth derivative comparison).

$$\forall (f:\mathrm{Real}\to \mathrm{Real}),(\forall (f_1:\mathrm{Real}\to \mathrm{Real}),(\forall (f_2:\mathrm{Real}\to \mathrm{Real}),(\forall (f_3:\mathrm{Real}\to \mathrm{Real}),(\forall (f_4:\mathrm{Real}\to \mathrm{Real}),((\forall (x:\mathrm{Real}),((0<x)\Rightarrow (\mathrm{HasDerivAt}\left(f,\left(f_1\right)\left(x\right),x\right))))\Rightarrow ((\forall (x:\mathrm{Real}),((0<x)\Rightarrow (\mathrm{HasDerivAt}\left(f_1,\left(f_2\right)\left(x\right),x\right))))\Rightarrow ((\forall (x:\mathrm{Real}),((0<x)\Rightarrow (\mathrm{HasDerivAt}\left(f_2,\left(f_3\right)\left(x\right),x\right))))\Rightarrow ((\forall (x:\mathrm{Real}),((0<x)\Rightarrow (\mathrm{HasDerivAt}\left(f_3,\left(f_4\right)\left(x\right),x\right))))\Rightarrow ((\forall (x:\mathrm{Real}),((0<x)\Rightarrow (0\le \left(f_4\right)\left(x\right))))\Rightarrow (\forall (a:\mathrm{Real}),(\forall (b:\mathrm{Real}),(((((0<a)\wedge (a<b))\wedge ((f\left(a\right)=0)\wedge (f\left(b\right)=0)))\wedge ((\left(f_1\right)\left(a\right)=0)\wedge (\left(f_1\right)\left(b\right)=0)))\Rightarrow (\forall (x:\mathrm{Real}),((0<x)\Rightarrow (0\le f\left(x\right))))))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/HiguchiSudbery/HermiteMajorant.double_contact_nonnegative (✓ std3). ∎

Source. Repository-derived.

Commentary.

The functions f, f₁, f₂, f₃ and f₄ form a derivative chain at every positive point. Both f and f₁ vanish at the ordered positive nodes a and b. The displayed conclusion covers every positive x, including the contact nodes.

References

• Truth anchor: D5/S3/Quantum/Entanglement/HiguchiSudbery/HermiteMajorant.double_contact_nonnegative