Trajectory Bounds

theorem FD1D.V5.ContinuousProcess.expected_cost_le_sqrt_expected_squared_cost {L m : ℕ} (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : trajectoryExpectedCost a hm fallback t ≤ √(trajectoryExpectedSquaredCost a hm fallback t)

Cauchy--Schwarz converts the concrete one-period second moment into an upper bound for its expected distance.

theorem FD1D.V5.ContinuousProcess.trajectoryExpectedSquaredCost_nonneg {L m : ℕ} (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : 0 ≤ trajectoryExpectedSquaredCost a hm fallback t

theorem FD1D.V5.ContinuousProcess.trajectoryExpectedSquaredCost_le_refreshedEnvelope {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : trajectoryExpectedSquaredCost a hm fallback t ≤ ((Dynamics.kernel a ha hm).iterate t (refreshedLaw L m)).expect (Transport.stateSquaredCostEnvelope a)

The iid spatial initialization projects the concrete squared cost to the refreshed finite count chain.

noncomputable def FD1D.V5.ContinuousProcess.trajectoryRMSCostFromState (m : ℕ) (hm : 1 ≤ m) (s₀ : SpatialState m) (t : ℕ) : ℝ

Per-period RMS cost of the parameterized policy from a fixed arbitrary initial inventory.

Equations

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

theorem FD1D.V5.ContinuousProcess.trajectoryRMSCostFromState_le_envelope {m : ℕ} (hm : 1 ≤ m) (s₀ : SpatialState m) (t : ℕ) : trajectoryRMSCostFromState m hm s₀ t ≤ rmsSquaredCostExpectation m hm (FiniteLaw.dirac (spatialCount (treeDepth m) s₀)) t

theorem FD1D.V5.ContinuousProcess.limsup_trajectoryRMSCostFromState_le {m : ℕ} (hm : 1 ≤ m) (s₀ : SpatialState m) : Filter.limsup (trajectoryRMSCostFromState m hm s₀) Filter.atTop ≤ 17 / 2 * ↑(parameterA m) / ↑m

Manuscript part (i), with the explicit proof constant 8.5.

theorem FD1D.V5.ContinuousProcess.refreshed_average_expected_squared_cost_rms_le {m T : ℕ} (hm : 1 ≤ m) (hT : m ^ 2 ≤ T) : √((∑ t ∈ Finset.range T, trajectoryExpectedSquaredCost ↑(parameterA m) ⋯ (SupplyConfiguration.canonicalFallback ⋯) t) / ↑T) ≤ 17 / 2 * ↑(parameterA m) / ↑m

The concrete refreshed trajectory inherits the count-chain average RMS bound.

theorem FD1D.V5.ContinuousProcess.refreshed_average_expected_cost_le {m T : ℕ} (hm : 1 ≤ m) (hT : m ^ 2 ≤ T) : (∑ t ∈ Finset.range T, trajectoryExpectedCost ↑(parameterA m) ⋯ (SupplyConfiguration.canonicalFallback ⋯) t) / ↑T ≤ 17 / 2 * ↑(parameterA m) / ↑m

Average expected distance is bounded by the refreshed average RMS second moment.