The local quadratic Bellman inequality

This module follows the normalization and three active-cap cases in the appendix of manuscript-v5/optimal_dynamic_matching.tex.

def FD1D.V5.LocalBellman.Normalized.lambda (ρ : ℝ) : ℝ

Squared imbalance parameter used in the normalized Bellman calculation.

Equations

• FD1D.V5.LocalBellman.Normalized.lambda ρ = ρ ^ 2

def FD1D.V5.LocalBellman.Normalized.A (s ρ : ℝ) : ℝ

Scale times one minus the squared imbalance.

Equations

• FD1D.V5.LocalBellman.Normalized.A s ρ = s * (1 - FD1D.V5.LocalBellman.Normalized.lambda ρ)

def FD1D.V5.LocalBellman.Normalized.g (s r : ℝ) : ℝ

Shifted scale appearing in the normalized potential ratios.

Equations

• FD1D.V5.LocalBellman.Normalized.g s r = s + r

def FD1D.V5.LocalBellman.Normalized.d (s ρ : ℝ) : ℝ

Positive denominator factor in the normalized feedback identities.

Equations

• FD1D.V5.LocalBellman.Normalized.d s ρ = s * (FD1D.V5.LocalBellman.Normalized.A s ρ + 2) + 1

noncomputable def FD1D.V5.LocalBellman.Normalized.hPlus (s ρ z : ℝ) : ℝ

Normalized rate of the plus child for the selected correction.

Equations

• FD1D.V5.LocalBellman.Normalized.hPlus s ρ z = (s + z) / (s * (1 + ρ))

noncomputable def FD1D.V5.LocalBellman.Normalized.hMinus (s ρ z : ℝ) : ℝ

Normalized rate of the minus child for the selected correction.

Equations

• FD1D.V5.LocalBellman.Normalized.hMinus s ρ z = (s - z) / (s * (1 - ρ))

noncomputable def FD1D.V5.LocalBellman.Normalized.tPlus (r z : ℝ) : ℝ

Half the difference between the residual parameter and the correction.

Equations

• FD1D.V5.LocalBellman.Normalized.tPlus r z = (r - z) / 2

noncomputable def FD1D.V5.LocalBellman.Normalized.tMinus (r z : ℝ) : ℝ

Half the sum of the residual parameter and the correction.

Equations

• FD1D.V5.LocalBellman.Normalized.tMinus r z = (r + z) / 2

noncomputable def FD1D.V5.LocalBellman.Normalized.ZParent (s r : ℝ) : ℝ

Normalized parent potential ratio.

Equations

• FD1D.V5.LocalBellman.Normalized.ZParent s r = FD1D.V5.LocalBellman.Normalized.g s r / (s + 1 / 2)

noncomputable def FD1D.V5.LocalBellman.Normalized.ZPlus (s r ρ : ℝ) : ℝ

Normalized potential ratio for the plus child.

Equations

• FD1D.V5.LocalBellman.Normalized.ZPlus s r ρ = FD1D.V5.LocalBellman.Normalized.g s r / (s * (1 + ρ) + 1)

noncomputable def FD1D.V5.LocalBellman.Normalized.ZMinus (s r ρ : ℝ) : ℝ

Normalized potential ratio for the minus child.

Equations

• FD1D.V5.LocalBellman.Normalized.ZMinus s r ρ = FD1D.V5.LocalBellman.Normalized.g s r / (s * (1 - ρ) + 1)

noncomputable def FD1D.V5.LocalBellman.Normalized.residual (s r ρ z : ℝ) : ℝ

Average child Bellman contribution minus the parent contribution.

Equations

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

noncomputable def FD1D.V5.LocalBellman.Normalized.rateIncrement (s ρ z : ℝ) : ℝ

Change of the mean squared normalized child rate relative to one.

Equations

• FD1D.V5.LocalBellman.Normalized.rateIncrement s ρ z = (FD1D.V5.LocalBellman.Normalized.hPlus s ρ z ^ 2 + FD1D.V5.LocalBellman.Normalized.hMinus s ρ z ^ 2) / 2 - 1

noncomputable def FD1D.V5.LocalBellman.Normalized.feedback (s ρ : ℝ) : ℝ

Feedback correction in the normalized local policy.

Equations

• FD1D.V5.LocalBellman.Normalized.feedback s ρ = 8 * s * ρ / FD1D.V5.LocalBellman.Normalized.A s ρ

def FD1D.V5.LocalBellman.Normalized.uniform (s ρ : ℝ) : ℝ

Correction corresponding to uniform deletion rates.

Equations

• FD1D.V5.LocalBellman.Normalized.uniform s ρ = s * ρ

noncomputable def FD1D.V5.LocalBellman.Normalized.floorCap (s r ρ : ℝ) : ℝ

Largest correction permitted by the normalized floor constraint.

Equations

• FD1D.V5.LocalBellman.Normalized.floorCap s r ρ = (s - s * (1 - ρ) * r) / (s * (1 - ρ) + 1)

noncomputable def FD1D.V5.LocalBellman.Normalized.J (s ρ k : ℝ) : ℝ

Rescaled gap between the scale and the chosen floor parameter.

Equations

• FD1D.V5.LocalBellman.Normalized.J s ρ k = (s - k) / FD1D.V5.LocalBellman.Normalized.A s ρ

noncomputable def FD1D.V5.LocalBellman.Normalized.bracket (s r ρ k : ℝ) : ℝ

Auxiliary expression controlling the normalized Bellman residual.

Equations

• FD1D.V5.LocalBellman.Normalized.bracket s r ρ k = s * k - FD1D.V5.LocalBellman.Normalized.J s ρ k * (s + 1 / 2) - (1 / 2 - r) * s ^ 2 / (s + 1 / 2)

theorem FD1D.V5.LocalBellman.Normalized.lambda_nonneg (ρ : ℝ) : 0 ≤ lambda ρ

theorem FD1D.V5.LocalBellman.Normalized.lambda_lt_one {ρ : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : lambda ρ < 1

theorem FD1D.V5.LocalBellman.Normalized.A_pos {s ρ : ℝ} (hs : 0 < s) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : 0 < A s ρ

theorem FD1D.V5.LocalBellman.Normalized.g_pos {s r : ℝ} (hr : -s < r) : 0 < g s r

theorem FD1D.V5.LocalBellman.Normalized.d_pos {s ρ : ℝ} (hs : 0 < s) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : 0 < d s ρ

theorem FD1D.V5.LocalBellman.Normalized.residual_eq_common {s r ρ k : ℝ} (hs : 0 < s) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : residual s r ρ (ρ * k) = r ^ 2 / 8 - lambda ρ * k ^ 2 / 24 + g s r * (1 / 2 - r) * (s + 1) / (2 * d s ρ * (s + 1 / 2)) + lambda ρ * g s r / d s ρ * bracket s r ρ k

theorem FD1D.V5.LocalBellman.Normalized.rateIncrement_eq_common {s ρ k : ℝ} (hs : 0 < s) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : rateIncrement s ρ (ρ * k) = 2 * lambda ρ * J s ρ k + (1 + lambda ρ) * lambda ρ * J s ρ k ^ 2

theorem FD1D.V5.LocalBellman.Normalized.uniform_hPlus {s ρ : ℝ} (hs : 0 < s) (hρ1 : ρ ≠ -1) : hPlus s ρ (uniform s ρ) = 1

theorem FD1D.V5.LocalBellman.Normalized.uniform_hMinus {s ρ : ℝ} (hs : 0 < s) (hρ1 : ρ ≠ 1) : hMinus s ρ (uniform s ρ) = 1

theorem FD1D.V5.LocalBellman.Normalized.uniform_rateIncrement {s ρ : ℝ} (hs : 0 < s) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : rateIncrement s ρ (uniform s ρ) = 0

theorem FD1D.V5.LocalBellman.Normalized.uniform_residual_eq {s r ρ : ℝ} (hs : 0 < s) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : residual s r ρ (uniform s ρ) = r ^ 2 / 8 - uniform s ρ ^ 2 / 24 + g s r ^ 2 * uniform s ρ ^ 2 / (d s ρ * (s + 1 / 2)) + g s r * (1 / 2 - r) * (s + 1) / (2 * d s ρ * (s + 1 / 2))

theorem FD1D.V5.LocalBellman.Normalized.uniform_case {s r ρ : ℝ} (hs : 0 < s) (hr0 : -s < r) (hr1 : r ≤ 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hactive : A s ρ ≤ 8) : residual s r ρ (uniform s ρ) ≥ (rateIncrement s ρ (uniform s ρ) + uniform s ρ ^ 2) / 1000

theorem FD1D.V5.LocalBellman.Normalized.feedback_case {s r ρ : ℝ} (hs : 0 < s) (hr0 : -s < r) (hr1 : r ≤ 1 / 2) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hactive : feedback s ρ ≤ uniform s ρ) : residual s r ρ (feedback s ρ) ≥ (rateIncrement s ρ (feedback s ρ) + feedback s ρ ^ 2) / 1000

noncomputable def FD1D.V5.LocalBellman.Normalized.floorEll (u v K : ℝ) : ℝ

Auxiliary floor coordinate obtained from the normalized child scales.

Equations

• FD1D.V5.LocalBellman.Normalized.floorEll u v K = 1 - u * (K - 1) / (2 * v)

noncomputable def FD1D.V5.LocalBellman.Normalized.floorW (u v K : ℝ) : ℝ

Weight of the correction term in the floor residual estimate.

Equations

• FD1D.V5.LocalBellman.Normalized.floorW u v K = (K + 1) * (u + 1) / (2 * (v + 1))

noncomputable def FD1D.V5.LocalBellman.Normalized.floorEta (u v : ℝ) : ℝ

Relative difference of the shifted normalized child scales.

Equations

• FD1D.V5.LocalBellman.Normalized.floorEta u v = (v + 1 - u) / (v + 1 + u)

noncomputable def FD1D.V5.LocalBellman.Normalized.floorR (K e u v : ℝ) : ℝ

Residual bound expressed in the floor coordinates.

Equations

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

noncomputable def FD1D.V5.LocalBellman.Normalized.floorJ (K e : ℝ) : ℝ

Rational lower-bound expression used in the floor-case estimate.

Equations

• FD1D.V5.LocalBellman.Normalized.floorJ K e = 5 * K ^ 2 - 3 + 2 * e ^ 2 - (2 * K + 6) * e + 24 * (K + 1) * e * (K + e) / (K * (16 + K + e))

theorem FD1D.V5.LocalBellman.Normalized.floorJ_bound {K e : ℝ} (hK : 1 ≤ K) (he0 : 0 ≤ e) : (K ^ 2 + e ^ 2) / 4 ≤ floorJ K e

def FD1D.V5.LocalBellman.Normalized.floorU (s ρ : ℝ) : ℝ

Minus-child scale in the floor coordinate system.

Equations

• FD1D.V5.LocalBellman.Normalized.floorU s ρ = s * (1 - ρ)

def FD1D.V5.LocalBellman.Normalized.floorV (s ρ : ℝ) : ℝ

Plus-child scale in the floor coordinate system.

Equations

• FD1D.V5.LocalBellman.Normalized.floorV s ρ = s * (1 + ρ)

def FD1D.V5.LocalBellman.Normalized.floorE (r : ℝ) : ℝ

Twice the gap of the residual parameter from 1 / 2.

Equations

• FD1D.V5.LocalBellman.Normalized.floorE r = 1 - 2 * r

noncomputable def FD1D.V5.LocalBellman.Normalized.floorK (s r ρ : ℝ) : ℝ

Floor parameter expressed through the two normalized child scales.

Equations

• FD1D.V5.LocalBellman.Normalized.floorK s r ρ = (FD1D.V5.LocalBellman.Normalized.floorV s ρ - FD1D.V5.LocalBellman.Normalized.floorE r) / (FD1D.V5.LocalBellman.Normalized.floorU s ρ + 1)

theorem FD1D.V5.LocalBellman.Normalized.floor_case {s r ρ : ℝ} (hs : 0 < s) (hr1 : r ≤ 1 / 2) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hactiveU : floorCap s r ρ ≤ uniform s ρ) (hactiveF : floorCap s r ρ ≤ feedback s ρ) : residual s r ρ (floorCap s r ρ) ≥ (rateIncrement s ρ (floorCap s r ρ) + floorCap s r ρ ^ 2) / 1000

theorem FD1D.V5.LocalBellman.Normalized.equal_case {s r : ℝ} (hs : 0 < s) (hr0 : -s < r) (hr1 : r ≤ 1 / 2) : residual s r 0 0 ≥ (rateIncrement s 0 0 + 0 ^ 2) / 1000

theorem FD1D.V5.LocalBellman.Normalized.threeCap_case {s r ρ : ℝ} (hs : 0 < s) (hr0 : -s < r) (hr1 : r ≤ 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : have z := min (feedback s ρ) (min (uniform s ρ) (floorCap s r ρ)); residual s r ρ z ≥ (rateIncrement s ρ z + z ^ 2) / 1000

Empty-child boundary

noncomputable def FD1D.V5.LocalBellman.Normalized.emptyResidual (s r emptyRate : ℝ) : ℝ

The normalized residual when the larger child is occupied and the smaller child is empty. The occupied child has normalized rate one; emptyRate is the auxiliary rate assigned to the empty child.

Equations

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

noncomputable def FD1D.V5.LocalBellman.Normalized.emptyRateIncrement (emptyRate : ℝ) : ℝ

Normalized child-rate energy at a one-empty-child boundary.

Equations

• FD1D.V5.LocalBellman.Normalized.emptyRateIncrement emptyRate = (1 + emptyRate ^ 2) / 2 - 1

Concrete local policy

noncomputable def FD1D.V5.LocalBellman.localResidual (a p h : ℝ) (x y : ℕ) : ℝ

The left side of the manuscript's local Bellman inequality.

Equations

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

noncomputable def FD1D.V5.LocalBellman.localEnergy (a p h : ℝ) (x y : ℕ) : ℝ

The rate increment plus squared deletion bias in the local inequality.

Equations

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

theorem FD1D.V5.LocalBellman.local_bellman_inequality {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hp : 0 < p) (hh : 0 < h) (ht : LocalPolicy.discrepancy a p h x y ≤ h / 2) : localResidual a p h x y ≥ localEnergy a p h x y / 1000

The concrete local Bellman inequality from Lemma lem:local of the v5 manuscript, including positive, one-empty, and empty-parent nodes.