Bellman

The deterministic Bellman certificate

This file formalizes the local Bellman inequality and the exact four-chart certificate in optimal_dynamic_matching.tex. The coefficient checks use the kernel-checked integer polynomials in FD1D.PolynomialCertificate; the surrounding lemmas connect them to the real-valued Bellman residual.

noncomputable def FD1D.d (y : ℝ) : ℝ

The cubic scalar weight in the Bellman function.

Equations

• FD1D.d y = (1 + 7 * y ^ 3) / 12

noncomputable def FD1D.B (h t y : ℝ) : ℝ

The Bellman function from equation (6).

Equations

• FD1D.B h t y = FD1D.d y * (t - y * h) * (2 * h - t - 3 / 2 * y * h)

noncomputable def FD1D.normalizedW (s v : ℝ) : ℝ

W = w² in the normalized local variables.

Equations

• FD1D.normalizedW s v = s * (1 + v) * v / (s + 2)

noncomputable def FD1D.normalizedResidual (s r v : ℝ) : ℝ

The normalized residual in equation (8).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev FD1D.R (s r v : ℝ) : ℝ

Short mathematical name for the normalized residual.

Equations

• FD1D.R s r v = FD1D.normalizedResidual s r v

def FD1D.bellmanPolynomial (s r v : ℝ) : ℝ

The cleared polynomial P from the exact certificate.

Equations

• FD1D.bellmanPolynomial s r v = FD1D.BellmanCertificate.bellmanRealAt s r v

@[reducible, inline]

abbrev FD1D.P (s r v : ℝ) : ℝ

Short mathematical name for the cleared polynomial certificate.

Equations

• FD1D.P s r v = FD1D.bellmanPolynomial s r v

def FD1D.bellmanDenominator (s v : ℝ) : ℝ

The positive denominator used to clear the normalized residual.

Equations

• FD1D.bellmanDenominator s v = 1200 * (s + 1) ^ 5 * (s + 2) * (s + 2 + 2 * v) ^ 5

theorem FD1D.normalizedResidual_mul_denominator {s r v : ℝ} (hs1 : s + 1 ≠ 0) (hs2 : s + 2 ≠ 0) (hM : s + 2 + 2 * v ≠ 0) : normalizedResidual s r v * bellmanDenominator s v = bellmanPolynomial s r v

The exact bridge omitted by a bare coefficient check: equation (8), after clearing its rational denominators, is exactly equation (13).

theorem FD1D.normalizedResidual_eq_div {s r v : ℝ} (hs1 : s + 1 ≠ 0) (hs2 : s + 2 ≠ 0) (hM : s + 2 + 2 * v ≠ 0) : normalizedResidual s r v = bellmanPolynomial s r v / bellmanDenominator s v

Exact four-chart certificate

Each transformed polynomial has nonnegative integer coefficients. The certificate module computes and kernel-checks those coefficients, proves its evaluator sound, and exposes the resulting real nonnegativity theorems.

theorem FD1D.bellmanPolynomial_nonnegative_closed {s r v : ℝ} (_hs : 0 ≤ s) (hrLower : -s ≤ r) (hrUpper : r ≤ 1 / 2) (hv : 0 ≤ v) (hvUpper : v ≤ s / 2) : 0 ≤ bellmanPolynomial s r v

The four charts cover the full closed normalized domain.

theorem FD1D.bellmanPolynomial_nonnegative {s r v : ℝ} (hs : 0 ≤ s) (hrLower : -s < r) (hrUpper : r ≤ 1 / 2) (hv : 0 ≤ v) (hvUpper : v ≤ s / 2) : 0 ≤ bellmanPolynomial s r v

Polynomial nonnegativity on the (strict-lower-bound) physical domain.

theorem FD1D.normalizedResidual_nonnegative {s r v : ℝ} (hs : 0 ≤ s) (hrLower : -s < r) (hrUpper : r ≤ 1 / 2) (hv : 0 ≤ v) (hvUpper : v ≤ s / 2) : 0 ≤ normalizedResidual s r v

The normalized local Bellman residual is nonnegative on its full domain.

The local Bellman inequality

noncomputable def FD1D.localBellmanGap (h s r v w : ℝ) : ℝ

Equation (7), moved to the left-hand side and written in the canonical normalized child coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem FD1D.localBellmanGap_eq {h s r v w : ℝ} (hw : w ^ 2 = normalizedW s v) : localBellmanGap h s r v w = h ^ 2 * normalizedResidual s r v

Exact algebra connecting the normalized residual to equation (7).

theorem FD1D.localBellmanGap_nonnegative {h s r v w : ℝ} (hs : 0 ≤ s) (hrLower : -s < r) (hrUpper : r ≤ 1 / 2) (hv : 0 ≤ v) (hvUpper : v ≤ s / 2) (hw : w ^ 2 = normalizedW s v) : 0 ≤ localBellmanGap h s r v w

Canonical normalized form of the full deterministic local lemma (7).

theorem FD1D.local_bellman_inequality {h t y hL hR tL tR yL yR ZL ZR s r v w : ℝ} (hs : 0 ≤ s) (hrLower : -s < r) (hrUpper : r ≤ 1 / 2) (hv : 0 ≤ v) (hvUpper : v ≤ s / 2) (hw : w ^ 2 = normalizedW s v) (ht : t = h * r) (hy : y = (s + r) / (s + 1)) (hhL : hL = h * (1 + v + w)) (hhR : hR = h * (1 + v - w)) (htL : tL = h * (r / 2 + w)) (htR : tR = h * (r / 2 - w)) (hyL : yL = (s + r) / (s + 2 + 2 * v)) (hyR : yR = (s + r) / (s + 2 + 2 * v)) (hZL : ZL = yL * hL) (hZR : ZR = yR * hR) : (tL * ZL + tR * ZR) / 2 + (B hL tL yL + B hR tR yR) / 2 - B h t y ≥ 1 / 100 * ((hL ^ 2 + hR ^ 2) / 2 - h ^ 2)

A reusable form of (7). Callers need only provide the normalized identities for their parent and two children.

Terminal and root bounds

theorem FD1D.d_nonnegative {y : ℝ} (hy : 0 ≤ y) : 0 ≤ d y

theorem FD1D.bellman_nonpositive {h r y : ℝ} (hh : 0 ≤ h) (hr : r ≤ 1 / 2) (_hy0 : 0 ≤ y) (hy1 : y ≤ 1) (hry : r ≤ y) : B h (h * r) y ≤ 0

The sign argument used at terminal nodes: if t = hr, r ≤ y ≤ 1, and r ≤ 1/2, then the Bellman value is nonpositive.

theorem FD1D.normalized_bellman_nonpositive {h s r : ℝ} (hh : 0 ≤ h) (hs : 0 ≤ s) (hrLower : -s < r) (hrUpper : r ≤ 1 / 2) : B h (h * r) ((s + r) / (s + 1)) ≤ 0

The parent Bellman value is nonpositive throughout the normalized domain.

theorem FD1D.root_bellman_identity (h y : ℝ) : h ^ 2 / 3 + B h 0 y = h ^ 2 * (1 - y) * (5 + (1 - y) * (3 + 7 * y + 14 * y ^ 2 + 21 * y ^ 3)) / 24

Exact polynomial identity behind the root estimate.

theorem FD1D.bellman_root_bound {h y : ℝ} (hy0 : 0 ≤ y) (hy1 : y ≤ 1) : -h ^ 2 / 3 ≤ B h 0 y

At the root, B(h,0,y) ≥ -h²/3.

theorem FD1D.bellman_root_bound_inv {m y : ℝ} (hm : 0 < m) (hy0 : 0 ≤ y) (hy1 : y ≤ 1) : -1 / (3 * m ^ 2) ≤ B (1 / m) 0 y

Root bound in the h = 1/m normalization used in the tree proof.