Joined Trajectory

Initialization joined to the continuous trajectory

The time-zero spatial coordinate of trajectoryLaw is the iid refreshed inventory. We use that exact coordinate vector as the replenishment supply for the first m scheduled matches. Thus initialization and the main policy live on one path space, with a pathwise (not merely count-law) phase boundary.

noncomputable def FD1D.V5.ContinuousProcess.coordinateRefreshSupply {m : ℕ} (L : ℕ) (s : SpatialState m) : RefreshSupply L m

A continuous coordinate state, viewed as the supply used by initialization.

Equations

• FD1D.V5.ContinuousProcess.coordinateRefreshSupply L s = { location := fun (j : Fin m) => ↑(s j), leaf := FD1D.V5.spatialLeaves L s, location_mem_unit := ⋯ }

@[simp]

theorem FD1D.V5.ContinuousProcess.coordinateRefreshSupply_location {m : ℕ} (L : ℕ) (s : SpatialState m) (j : Fin m) : (coordinateRefreshSupply L s).location j = ↑(s j)

@[simp]

theorem FD1D.V5.ContinuousProcess.coordinateRefreshSupply_leaf {m : ℕ} (L : ℕ) (s : SpatialState m) : (coordinateRefreshSupply L s).leaf = spatialLeaves L s

theorem FD1D.V5.ContinuousProcess.refresh_coordinateRefreshSupply_location {L m : ℕ} (initial : RefreshSupply L m) (s : SpatialState m) (j : Fin m) : (initial.refresh (coordinateRefreshSupply L s) m).location j = ↑(s j)

theorem FD1D.V5.ContinuousProcess.refresh_coordinateRefreshSupply_leaf {L m : ℕ} (initial : RefreshSupply L m) (s : SpatialState m) : (initial.refresh (coordinateRefreshSupply L s) m).leaf = spatialLeaves L s

theorem FD1D.V5.ContinuousProcess.refresh_coordinateRefreshSupply_countState {L m : ℕ} (initial : RefreshSupply L m) (s : SpatialState m) : (initial.refresh (coordinateRefreshSupply L s) m).countState = spatialCount L s

noncomputable def FD1D.V5.ContinuousProcess.joinedInitializationTerminal {L m : ℕ} (initial : RefreshSupply L m) (path : ℕ → ProcessState m) : RefreshSupply L m

The terminal initialized supply read from the same path used by the main policy.

Equations

• FD1D.V5.ContinuousProcess.joinedInitializationTerminal initial path = initial.refresh (FD1D.V5.ContinuousProcess.coordinateRefreshSupply L (path 0).1) m

@[simp]

theorem FD1D.V5.ContinuousProcess.joinedInitializationTerminal_location {L m : ℕ} (initial : RefreshSupply L m) (path : ℕ → ProcessState m) (j : Fin m) : (joinedInitializationTerminal initial path).location j = ↑((path 0).1 j)

Every terminal initialized coordinate is the corresponding time-zero path coordinate.

@[simp]

theorem FD1D.V5.ContinuousProcess.joinedInitializationTerminal_leaf {L m : ℕ} (initial : RefreshSupply L m) (path : ℕ → ProcessState m) : (joinedInitializationTerminal initial path).leaf = spatialLeaves L (path 0).1

The terminal initialized leaf labels are the labels of the time-zero path coordinates.

@[simp]

theorem FD1D.V5.ContinuousProcess.joinedInitializationTerminal_countState {L m : ℕ} (initial : RefreshSupply L m) (path : ℕ → ProcessState m) : (joinedInitializationTerminal initial path).countState = spatialCount L (path 0).1

The terminal initialized count is the time-zero count of the same path.

theorem FD1D.V5.ContinuousProcess.map_timeZeroSpatial_trajectoryLaw {L m : ℕ} (a : ℝ) (fallback : Fin m) : MeasureTheory.Measure.map (fun (path : ℕ → ProcessState m) => (path 0).1) (trajectoryLaw a fallback) = initialSpatialLaw m

The time-zero spatial vector on the trajectory has the iid continuous law.

theorem FD1D.V5.ContinuousProcess.map_joinedInitializationTerminal_countState {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (initial : RefreshSupply L m) : MeasureTheory.Measure.map (fun (path : ℕ → ProcessState m) => (joinedInitializationTerminal initial path).countState) (trajectoryLaw a fallback) = (refreshedLaw L m).toMeasure

On the joined path law, initialization terminates with the refreshed count law.

noncomputable def FD1D.V5.ContinuousProcess.joinedInitializationStepCost {L m : ℕ} (initial : RefreshSupply L m) (demand : Fin m → ℝ) (path : ℕ → ProcessState m) (j : Fin m) : ℝ

Cost of scheduled initialization match j on the joined path.

Equations

• FD1D.V5.ContinuousProcess.joinedInitializationStepCost initial demand path j = |demand j - (initial.refresh (FD1D.V5.ContinuousProcess.coordinateRefreshSupply L (path 0).1) ↑j).location j|

@[simp]

theorem FD1D.V5.ContinuousProcess.joinedInitializationStepCost_eq {L m : ℕ} (initial : RefreshSupply L m) (demand : Fin m → ℝ) (path : ℕ → ProcessState m) (j : Fin m) : joinedInitializationStepCost initial demand path j = |demand j - initial.location j|

The joined scheduled match removes the still-unrefreshed original label.

theorem FD1D.V5.ContinuousProcess.sum_joinedInitializationStepCost {L m : ℕ} (initial : RefreshSupply L m) (demand : Fin m → ℝ) (path : ℕ → ProcessState m) : ∑ j : Fin m, joinedInitializationStepCost initial demand path j = initializationMatchingCost initial demand

The joined path's initialization costs sum to the explicit initialization cost.

theorem FD1D.V5.ContinuousProcess.pathProcessCost_integrable {L m : ℕ} (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.Integrable (fun (path : ℕ → ProcessState m) => processCost L a fallback (path t)) (trajectoryLaw a fallback)

A main-period path cost is integrable on the continuous trajectory law.

noncomputable def FD1D.V5.ContinuousProcess.joinedTrajectoryAverageCost {L m : ℕ} (initial : RefreshSupply L m) (demand : Fin m → ℝ) (a : ℝ) (hm : 0 < m) (N : ℕ) (path : ℕ → ProcessState m) : ℝ

The average cost of initialization followed by the main policy, as one random variable on the single infinite continuous trajectory.

Equations

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

theorem FD1D.V5.ContinuousProcess.joinedTrajectoryAverageCost_integrable {L m : ℕ} (initial : RefreshSupply L m) (demand : Fin m → ℝ) (a : ℝ) (hm : 0 < m) (N : ℕ) : MeasureTheory.Integrable (joinedTrajectoryAverageCost initial demand a hm N) (trajectoryLaw a (SupplyConfiguration.canonicalFallback hm))

The joined full-horizon path cost is integrable.

theorem FD1D.V5.ContinuousProcess.integral_joinedTrajectoryAverageCost {L m : ℕ} (initial : RefreshSupply L m) (demand : Fin m → ℝ) (a : ℝ) (hm : 0 < m) (N : ℕ) : ∫ (path : ℕ → ProcessState m), joinedTrajectoryAverageCost initial demand a hm N path ∂trajectoryLaw a (SupplyConfiguration.canonicalFallback hm) = (initializationMatchingCost initial demand + ∑ t ∈ Finset.range (N - m), trajectoryExpectedCost a hm (SupplyConfiguration.canonicalFallback hm) t) / ↑N

The expectation of the one-path full-horizon cost is exactly initialization cost plus the sum of the trajectory's one-period expected costs.

theorem FD1D.V5.ContinuousProcess.finite_horizon_expected_joinedTrajectoryCost_le_nine {m N : ℕ} (hm : 1 ≤ m) (hN : 2 * m ^ 2 ≤ N) (initial : RefreshSupply (treeDepth m) m) (demand : Fin m → ℝ) (hdemand : ∀ (j : Fin m), demand j ∈ Set.Icc 0 1) : ∫ (path : ℕ → ProcessState m), joinedTrajectoryAverageCost initial demand ↑(parameterA m) ⋯ N path ∂trajectoryLaw (↑(parameterA m)) (SupplyConfiguration.canonicalFallback ⋯) ≤ 9 * ↑(parameterA m) / ↑m

Manuscript part (ii): scheduled replacement followed by the v5 policy has average expected cost at most 9a/m once N ≥ 2m².