Unified energy estimates for the v5 policy

This module proves the stationary and finite-horizon forms of the manuscript's master energy inequality.

noncomputable def FD1D.V5.Dynamics.combinedEnergy {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) : ℝ

Sum of transport energy and the weighted finest-level rate energy.

Equations

• FD1D.V5.Dynamics.combinedEnergy a x = a ^ 2 / 2 * FD1D.V5.Dynamics.stateRateEnergy a x L + FD1D.V5.Dynamics.stateTransportEnergy a x

theorem FD1D.V5.Dynamics.stateRateEnergy_nonneg {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (d : ℕ) : 0 ≤ stateRateEnergy a x d

theorem FD1D.V5.Dynamics.stateTransportEnergy_nonneg {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) : 0 ≤ stateTransportEnergy a x

theorem FD1D.V5.Dynamics.combinedEnergy_nonneg {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) : 0 ≤ combinedEnergy a x

theorem FD1D.V5.Dynamics.state_combinedEnergy_le_drift {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 2000 * ↑L ≤ a) (x : InventoryState (DyadicNode L) m) : combinedEnergy a x - 501 * a ^ 2 / ↑m ^ 2 ≤ 1000 * a * (stateDrift a x - stateRemainder a x)

The one-state inequality preceding the master energy telescope.

theorem FD1D.V5.Dynamics.expect_combinedEnergy_le {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 2000 * ↑L ≤ a) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) : μ.expect (combinedEnergy a) ≤ 501 * a ^ 2 / ↑m ^ 2 + 1000 * a * (μ.expect (stateDrift a) - μ.expect (stateRemainder a))

theorem FD1D.V5.Dynamics.stationary_expected_drift_eq_remainder {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hμ : (kernel a ha hm).IsStationary μ) : μ.expect (stateDrift a) = μ.expect (stateRemainder a)

theorem FD1D.V5.Dynamics.stationary_energy_estimates {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 2000 * ↑L ≤ a) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hμ : (kernel a ha hm).IsStationary μ) : (μ.expect fun (x : InventoryState (DyadicNode L) m) => stateRateEnergy a x L) ≤ 1002 / ↑m ^ 2 ∧ μ.expect (stateTransportEnergy a) ≤ 501 * a ^ 2 / ↑m ^ 2

The two stationary energy bounds in Proposition 4.4.

theorem FD1D.V5.Dynamics.existsUnique_stationaryLaw {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) : ∃! μ : FiniteLaw (InventoryState (DyadicNode L) m), (kernel a ha hm).IsStationary μ

theorem FD1D.V5.Dynamics.master_energy_estimate {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 2000 * ↑L ≤ a) (μ₀ : FiniteLaw (InventoryState (DyadicNode L) m)) (T : ℕ) (hT : 0 < T) : (∑ t ∈ Finset.range T, ((kernel a ha hm).iterate t μ₀).expect (combinedEnergy a)) / ↑T ≤ 501 * a ^ 2 / ↑m ^ 2 + 1000 * a / ↑T * (((kernel a ha hm).iterate T μ₀).expect (statePotential a) - μ₀.expect (statePotential a))

The manuscript's finite-horizon master energy estimate.

theorem FD1D.V5.Dynamics.finite_transport_energy_estimate {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 2000 * ↑L ≤ a) (hbudget : Real.log (1 + 2 * ↑m / a) ≤ a / 2000) (μ₀ : FiniteLaw (InventoryState (DyadicNode L) m)) (T : ℕ) (hT : 0 < T) : (∑ t ∈ Finset.range T, ((kernel a ha hm).iterate t μ₀).expect (stateTransportEnergy a)) / ↑T ≤ 501 * a ^ 2 / ↑m ^ 2 + a ^ 2 / (2 * ↑T)

The finite-horizon bound on average transport energy.