Palomar endpoint for optimal fully dynamic matching

This module instantiates the compact paper-facing stochastic model with the hierarchical V5 selector and transfers the proved continuous-process bounds.

noncomputable def FD1D.V5.Palomar.hierarchicalPolicy (m : ℕ) (hm : 1 ≤ m) : OnlinePolicy m

The measurable hierarchical selector used by the V5 formalization.

Equations

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

theorem FD1D.V5.Palomar.optimalDynamicMatchingUpperBound : OptimalDynamicMatchingUpperBound

There is a measurable online policy whose RMS one-period cost from every fixed initial inventory is eventually at most C log(m+1)/m, and whose expected average cost after scheduled replacement is at most the same bound for every N >= 2m^2.