Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Equality in the Hermite envelope

Abstract

The logarithmic Hermite bound is attained exactly at the moment nodes, with one upper coordinate when the variance is positive.

Theorem 1.1 (Strict sign to the left of the double node).

Proof. Machine-checked in Lean as D5/S3/Analytic/Interpolation/HermiteEnvelopeEquality.negative_left_of_double_node (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let x, L and H be real numbers with x less than L and L less than H. Let g be three times continuously differentiable on the real line. Suppose g vanishes at L and H, its derivative vanishes at L, and its third derivative is strictly positive throughout the open interval from x to H. Then g(x) is strictly negative. If g(x) were nonnegative, two mean value arguments would produce a nonnegative second derivative to the left of L. Two Rolle arguments produce a zero second derivative to the right of L, contradicting strict increase of the second derivative.

Theorem 1.2 (Positive variance and the unique upper coordinate).

Proof. Machine-checked in Lean as D5/S3/Analytic/Interpolation/HermiteEnvelopeEquality.hermite_envelope_equality (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let k be a natural number at least two and let x assign positive real coordinates to Fin k. Write m for their mean, V for their total squared deviation, r for the radius, and L and H for the two nodes.

If V is positive, the sum attains the envelope if and only if every coordinate equals L or H. For coordinates at these nodes, the first moment forces exactly one coordinate to equal H and every other coordinate to equal L.

Use the quadratic agreeing with f and its derivative at L and with f at H. Its sum is determined by the first two moments. At any positive coordinate below H other than the nodes, f is strictly below this quadratic: the interval remainder handles coordinates between the nodes, and the preceding strict sign handles coordinates to the left. The nonnegative differences sum to zero exactly when every difference is zero. Finally, counting the upper coordinates gives their count times H-L equal to H-L, so their count is one.

Theorem 1.3 (Zero variance).

Proof. Machine-checked in Lean as D5/S3/Analytic/Interpolation/HermiteEnvelopeEquality.hermite_envelope_zero_variance (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any natural k and real vector indexed by Fin k, use the same definitions of m, V, r, L and H. If V is zero, each nonnegative squared deviation is zero. Thus every coordinate equals m, both nodes equal m, and the logarithmic sum equals its envelope. This identity requires no positivity assumption.

Theorem 1.4 (Attainment for every feasible pair of moments).

Proof. Machine-checked in Lean as D5/S3/Analytic/Interpolation/HermiteEnvelopeEquality.hermite_envelope_sharpness (✓ std3). ∎

Source. Repository-derived.

Commentary.

Now prescribe a natural k at least two and real parameters m and V satisfying m positive and zero at most V strictly less than k(k-1)m squared. Define r, L and H from these parameters as follows.

There is a positive real vector whose first sum is km, whose total squared deviation about m is V, and whose square sum is km squared plus V. It attains the logarithmic envelope and has one distinguished coordinate H and all other coordinates L. When V is zero the nodes coincide, so the distinguished index need not be unique.

Choose index zero for H and put L at every other index. The radius is smaller than m, which proves positivity. Summing any function over this vector gives its value at H plus k-1 times its value at L. Applying this to the identity, centered square and square gives the required moments. The equality classification, including its zero variance case, then gives attainment. Together with the upper bound this proves optimality in the class of positive real vectors with the prescribed moments.

References