Final arithmetic for the chosen parameters

This file turns the concrete stationary and finite-time hazard estimates into the advertised 6a/m and 7a/m bounds. Transport enters only through an equation-(3) inequality supplied as a hypothesis.

noncomputable def FD1D.parameterizedKernel (m : ℕ) (hm : 1 ≤ m) : FiniteKernel (InventoryState (DyadicNode (treeDepth m)) m)

The concrete hierarchical count kernel with the paper's parameter and tree depth.

Equations

• FD1D.parameterizedKernel m hm = FD1D.HierarchicalDynamics.kernel ↑(FD1D.parameterA m) ⋯ ⋯

noncomputable def FD1D.parameterizedHazardEnergy (m : ℕ) (x : InventoryState (DyadicNode (treeDepth m)) m) : ℝ

Terminal hazard energy for the paper's parameter and tree depth.

Equations

• FD1D.parameterizedHazardEnergy m x = FD1D.HierarchicalDynamics.stateHazardEnergy (↑(FD1D.parameterA m)) x (FD1D.treeDepth m)

noncomputable def FD1D.refreshedIterate (m : ℕ) (hm : 1 ≤ m) (t : ℕ) : FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)

The count law at time t after iid uniform refreshing.

Equations

• FD1D.refreshedIterate m hm t = (FD1D.parameterizedKernel m hm).iterate t (FD1D.refreshedLaw (FD1D.treeDepth m) m)

theorem FD1D.expected_hazard_root_lower_bound {m : ℕ} (hm : 1 ≤ m) (μ : FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)) : 1 / ↑m ^ 2 ≤ μ.expect (parameterizedHazardEnergy m)

The root node gives a lower bound on expected hazard energy.

theorem FD1D.averaged_hazard_root_lower_bound {m T : ℕ} (hm : 1 ≤ m) (hT : 0 < T) : 1 / ↑m ^ 2 ≤ (∑ t ∈ Finset.range T, (refreshedIterate m hm t).expect (parameterizedHazardEnergy m)) / ↑T

The root lower bound also holds for a positive finite time average.

theorem FD1D.stationary_expected_cost_le_six {m : ℕ} (hm : 1 ≤ m) (μ : FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)) (cost : InventoryState (DyadicNode (treeDepth m)) m → ℝ) (hμ : (parameterizedKernel m hm).IsStationary μ) (htransport : μ.expect cost ≤ 1 / ↑(leafCount m) + ↑(parameterA m) / √6 * √(μ.expect (parameterizedHazardEnergy m) - 1 / ↑m ^ 2)) : μ.expect cost ≤ 6 * ↑(parameterA m) / ↑m

For the chosen parameters, stationary equation (3) implies the advertised stationary 6a/m bound. All hazard and parameter hypotheses are discharged internally.

theorem FD1D.finite_average_expected_cost_le_six {m T : ℕ} (hm : 1 ≤ m) (hT : m ^ 2 ≤ T) (cost : ℕ → InventoryState (DyadicNode (treeDepth m)) m → ℝ) (htransport : (∑ t ∈ Finset.range T, (refreshedIterate m hm t).expect (cost t)) / ↑T ≤ 1 / ↑(leafCount m) + ↑(parameterA m) / √6 * √((∑ t ∈ Finset.range T, (refreshedIterate m hm t).expect (parameterizedHazardEnergy m)) / ↑T - 1 / ↑m ^ 2)) : (∑ t ∈ Finset.range T, (refreshedIterate m hm t).expect (cost t)) / ↑T ≤ 6 * ↑(parameterA m) / ↑m

For T ≥ m², an averaged equation-(3)/Jensen estimate along the concrete iterates from the refreshed law implies average expected cost at most 6a/m.

theorem FD1D.finite_horizon_expected_cost_le_seven {m N : ℕ} (hm : 1 ≤ m) (hN : 2 * m ^ 2 ≤ N) (initializationCost : ℝ) (cost : ℕ → InventoryState (DyadicNode (treeDepth m)) m → ℝ) (hinitialization : initializationCost ≤ ↑m) (htransport : (∑ t ∈ Finset.range (N - m), (refreshedIterate m hm t).expect (cost t)) / ↑(N - m) ≤ 1 / ↑(leafCount m) + ↑(parameterA m) / √6 * √((∑ t ∈ Finset.range (N - m), (refreshedIterate m hm t).expect (parameterizedHazardEnergy m)) / ↑(N - m) - 1 / ↑m ^ 2)) : (initializationCost + ∑ t ∈ Finset.range (N - m), (refreshedIterate m hm t).expect (cost t)) / ↑N ≤ 7 * ↑(parameterA m) / ↑m

For N ≥ 2m², at most m initialization cost followed by the concrete main policy bound gives total expected average cost at most 7a/m.