Continuous Process

The continuous-coordinate matching process

This module constructs the policy on one probability space. A state records the live supply coordinates together with the current independent demand and replenishment coordinates. The reward and the inventory update therefore use the same demand sample.

@[reducible, inline]

abbrev FD1D.V5.ContinuousProcess.Noise : Type

One period's independent demand and replenishment coordinates.

Equations

• FD1D.V5.ContinuousProcess.Noise = (↑unitInterval × ↑unitInterval)

noncomputable def FD1D.V5.ContinuousProcess.noiseLaw : MeasureTheory.Measure Noise

The law of an independent uniform demand/replenishment pair.

Equations

• FD1D.V5.ContinuousProcess.noiseLaw = MeasureTheory.volume.prod MeasureTheory.volume

instance FD1D.V5.ContinuousProcess.noiseLaw.isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure noiseLaw

theorem FD1D.V5.ContinuousProcess.map_coe_volume : MeasureTheory.Measure.map (fun (u : ↑unitInterval) => ↑u) MeasureTheory.volume = DyadicMass.uniformDemand

Coercing the canonical unit-interval law gives restricted Lebesgue measure.

theorem FD1D.V5.ContinuousProcess.map_selectedIndex_volume {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) : MeasureTheory.Measure.map (fun (u : ↑unitInterval) => q.selectedIndex ↑u) MeasureTheory.volume = (q.selectedIndexLaw hq).toMeasure

A continuous uniform coordinate has the finite selected-index law.

theorem FD1D.V5.ContinuousProcess.map_uniformArrivalLeaf_volume (L : ℕ) : MeasureTheory.Measure.map (fun (u : ↑unitInterval) => DyadicMass.uniformArrivalLeaf L ↑u) MeasureTheory.volume = FiniteLaw.uniform.toMeasure

The replenishment coordinate induces the uniform dyadic-leaf law.

theorem FD1D.V5.ContinuousProcess.map_noiseLeaves {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) : MeasureTheory.Measure.map (fun (z : Noise) => (q.selectedIndex ↑z.1, DyadicMass.uniformArrivalLeaf L ↑z.2)) noiseLaw = ((q.selectedIndexLaw hq).product FiniteLaw.uniform).toMeasure

The two leaf labels extracted from one noise pair have the product law.

noncomputable def FD1D.V5.ContinuousProcess.initialSpatialLaw (m : ℕ) : MeasureTheory.Measure (SpatialState m)

Iid continuous coordinates for the refreshed live inventory.

Equations

• FD1D.V5.ContinuousProcess.initialSpatialLaw m = MeasureTheory.Measure.pi fun (x : Fin m) => MeasureTheory.volume

instance FD1D.V5.ContinuousProcess.initialSpatialLaw.isProbabilityMeasure {m : ℕ} : MeasureTheory.IsProbabilityMeasure (initialSpatialLaw m)

theorem FD1D.V5.ContinuousProcess.map_spatialLeaves_initialSpatialLaw (L m : ℕ) : MeasureTheory.Measure.map (spatialLeaves L) (initialSpatialLaw m) = FiniteLaw.uniform.toMeasure

The leaf assignment obtained from iid continuous coordinates is uniform.

theorem FD1D.V5.ContinuousProcess.map_spatialCount_initialSpatialLaw (L m : ℕ) : MeasureTheory.Measure.map (spatialCount L) (initialSpatialLaw m) = (refreshedLaw L m).toMeasure

The refreshed continuous inventory projects to the existing refreshed count law.

One-step lumping to the finite count kernel

noncomputable def FD1D.V5.ContinuousProcess.leafPairLaw {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (s : SpatialState m) : FiniteLaw (DyadicNode L × DyadicNode L)

The finite deleted/arrived leaf pair generated at a fixed spatial state.

Equations

• FD1D.V5.ContinuousProcess.leafPairLaw a ha hm s = ((FD1D.V5.Dynamics.stateDyadicMass a (FD1D.V5.spatialCount L s)).selectedIndexLaw ⋯).product FD1D.FiniteLaw.uniform

theorem FD1D.V5.ContinuousProcess.leafPairLaw_map_move {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (s : SpatialState m) : FiniteLaw.map (fun (p : DyadicNode L × DyadicNode L) => (spatialCount L s).move p.1 p.2) (leafPairLaw a ha hm s) = (Dynamics.kernel a ha hm).rowLaw (spatialCount L s)

Forgetting the leaf pair after its move gives exactly one finite-kernel row.

theorem FD1D.V5.ContinuousProcess.noise_demand_ne_zero_ae : ∀ᵐ (z : Noise) ∂noiseLaw, ↑z.1 ≠ 0

The zero demand endpoint is null under the continuous noise law.

theorem FD1D.V5.ContinuousProcess.map_noiseLeaves_eq_leafPairLaw {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (s : SpatialState m) : MeasureTheory.Measure.map (fun (z : Noise) => ((Dynamics.stateDyadicMass a (spatialCount L s)).selectedIndex ↑z.1, DyadicMass.uniformArrivalLeaf L ↑z.2)) noiseLaw = (leafPairLaw a ha hm s).toMeasure

The continuous noise pair, mapped to deleted/arrived leaves, has leafPairLaw.

theorem FD1D.V5.ContinuousProcess.map_spatialCount_spatialStep {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (s : SpatialState m) : MeasureTheory.Measure.map (spatialCount L) (MeasureTheory.Measure.map (spatialStep L a fallback s) noiseLaw) = (Dynamics.kernel a ha hm).toKernel (spatialCount L s)

The count projection of one continuous-coordinate update is exactly the measure-valued row of the finite count kernel.

The spatial Markov kernel and its count marginals

noncomputable def FD1D.V5.ContinuousProcess.spatialKernel {L m : ℕ} (a : ℝ) (fallback : Fin m) : ProbabilityTheory.Kernel (SpatialState m) (SpatialState m)

One Markov step: sample fresh continuous noise and apply spatialStep.

Equations

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

instance FD1D.V5.ContinuousProcess.spatialKernel.isMarkovKernel {L m : ℕ} (a : ℝ) (fallback : Fin m) : ProbabilityTheory.IsMarkovKernel (spatialKernel a fallback)

theorem FD1D.V5.ContinuousProcess.spatialKernel_apply {L m : ℕ} (a : ℝ) (fallback : Fin m) (s : SpatialState m) : (spatialKernel a fallback) s = MeasureTheory.Measure.map (spatialStep L a fallback s) noiseLaw

The row of spatialKernel is the pushforward of one independent noise pair.

theorem FD1D.V5.ContinuousProcess.spatialKernel_map_count {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) : (spatialKernel a fallback).map (spatialCount L) = (Dynamics.kernel a ha hm).toKernel.comap (spatialCount L) ⋯

Mapping every spatial-kernel row through counts gives the finite row.

def FD1D.V5.ContinuousProcess.spatialLaw {L m : ℕ} (a : ℝ) (fallback : Fin m) : ℕ → MeasureTheory.Measure (SpatialState m)

The continuous spatial law after t policy steps.

Equations

• FD1D.V5.ContinuousProcess.spatialLaw a fallback 0 = FD1D.V5.ContinuousProcess.initialSpatialLaw m
• FD1D.V5.ContinuousProcess.spatialLaw a fallback t.succ = (FD1D.V5.ContinuousProcess.spatialLaw a fallback t).bind ⇑(FD1D.V5.ContinuousProcess.spatialKernel a fallback)

@[simp]

theorem FD1D.V5.ContinuousProcess.spatialLaw_zero {L m : ℕ} (a : ℝ) (fallback : Fin m) : spatialLaw a fallback 0 = initialSpatialLaw m

@[simp]

theorem FD1D.V5.ContinuousProcess.spatialLaw_succ {L m : ℕ} (a : ℝ) (fallback : Fin m) (t : ℕ) : spatialLaw a fallback (t + 1) = (spatialLaw a fallback t).bind ⇑(spatialKernel a fallback)

instance FD1D.V5.ContinuousProcess.spatialLaw.isProbabilityMeasure {L m : ℕ} (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.IsProbabilityMeasure (spatialLaw a fallback t)

theorem FD1D.V5.ContinuousProcess.map_spatialCount_spatialLaw {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure.map (spatialCount L) (spatialLaw a fallback t) = ((Dynamics.kernel a ha hm).iterate t (refreshedLaw L m)).toMeasure

Every continuous spatial marginal has exactly the finite count-chain law.

A single joint continuous trajectory

@[reducible, inline]

abbrev FD1D.V5.ContinuousProcess.ProcessState (m : ℕ) : Type

At a policy time, the joint state contains the pre-match inventory and the current independent demand/replenishment pair.

Equations

• FD1D.V5.ContinuousProcess.ProcessState m = (FD1D.V5.SpatialState m × FD1D.V5.ContinuousProcess.Noise)

noncomputable def FD1D.V5.ContinuousProcess.initialProcessLaw (m : ℕ) : MeasureTheory.Measure (ProcessState m)

The refreshed inventory and first noise pair are independent.

Equations

• FD1D.V5.ContinuousProcess.initialProcessLaw m = (FD1D.V5.ContinuousProcess.initialSpatialLaw m).prod FD1D.V5.ContinuousProcess.noiseLaw

instance FD1D.V5.ContinuousProcess.initialProcessLaw.isProbabilityMeasure {m : ℕ} : MeasureTheory.IsProbabilityMeasure (initialProcessLaw m)

noncomputable def FD1D.V5.ContinuousProcess.processAdvance {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (p : ProcessState m × Noise) : ProcessState m

Apply the current noise pair to the inventory, then attach the freshly sampled noise pair for the following period.

Equations

• FD1D.V5.ContinuousProcess.processAdvance L a fallback p = (FD1D.V5.spatialStep L a fallback p.1.1 p.1.2, p.2)

theorem FD1D.V5.ContinuousProcess.processAdvance_measurable {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) : Measurable (processAdvance L a fallback)

noncomputable def FD1D.V5.ContinuousProcess.processKernel {L m : ℕ} (a : ℝ) (fallback : Fin m) : ProbabilityTheory.Kernel (ProcessState m) (ProcessState m)

The homogeneous transition kernel of the joint process.

Equations

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

instance FD1D.V5.ContinuousProcess.processKernel.isMarkovKernel {L m : ℕ} (a : ℝ) (fallback : Fin m) : ProbabilityTheory.IsMarkovKernel (processKernel a fallback)

theorem FD1D.V5.ContinuousProcess.spatialKernel_comp {L m : ℕ} (a : ℝ) (fallback : Fin m) (μ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.SFinite μ] : μ.bind ⇑(spatialKernel a fallback) = MeasureTheory.Measure.map (fun (p : SpatialState m × Noise) => spatialStep L a fallback p.1 p.2) (μ.prod noiseLaw)

Spatial-kernel composition is the pushforward of state/noise product law.

theorem FD1D.V5.ContinuousProcess.processKernel_comp_product {L m : ℕ} (a : ℝ) (fallback : Fin m) (μ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.SFinite μ] : (μ.prod noiseLaw).bind ⇑(processKernel a fallback) = (μ.bind ⇑(spatialKernel a fallback)).prod noiseLaw

Starting from an independent state/noise pair preserves that factorization.

noncomputable def FD1D.V5.ContinuousProcess.processLaw {L m : ℕ} (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure (ProcessState m)

The recursively iterated joint-state law.

Equations

• FD1D.V5.ContinuousProcess.processLaw a fallback t = FD1D.TrajectoryBridge.iterateLaw (FD1D.V5.ContinuousProcess.processKernel a fallback) (FD1D.V5.ContinuousProcess.initialProcessLaw m) t

instance FD1D.V5.ContinuousProcess.processLaw.isProbabilityMeasure {L m : ℕ} (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.IsProbabilityMeasure (processLaw a fallback t)

theorem FD1D.V5.ContinuousProcess.processLaw_eq_product {L m : ℕ} (a : ℝ) (fallback : Fin m) (t : ℕ) : processLaw a fallback t = (spatialLaw a fallback t).prod noiseLaw

At every time, current noise remains independent of the live inventory.

noncomputable def FD1D.V5.ContinuousProcess.trajectoryLaw {L m : ℕ} (a : ℝ) (fallback : Fin m) : MeasureTheory.Measure (ℕ → ProcessState m)

One path-space law carrying the entire joint continuous process.

Equations

• FD1D.V5.ContinuousProcess.trajectoryLaw a fallback = FD1D.TrajectoryBridge.trajectoryLaw (FD1D.V5.ContinuousProcess.initialProcessLaw m) (FD1D.V5.ContinuousProcess.processKernel a fallback)

instance FD1D.V5.ContinuousProcess.trajectoryLaw.isProbabilityMeasure {L m : ℕ} (a : ℝ) (fallback : Fin m) : MeasureTheory.IsProbabilityMeasure (trajectoryLaw a fallback)

theorem FD1D.V5.ContinuousProcess.trajectoryLaw_marginal {L m : ℕ} (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure.map (fun (path : ℕ → ProcessState m) => path t) (trajectoryLaw a fallback) = processLaw a fallback t

Each coordinate of the single path law is the corresponding joint-state law.

theorem FD1D.V5.ContinuousProcess.trajectoryLaw_count_marginal {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure.map (fun (path : ℕ → ProcessState m) => spatialCount L (path t).1) (trajectoryLaw a fallback) = ((Dynamics.kernel a ha hm).iterate t (refreshedLaw L m)).toMeasure

The count at every path coordinate has the existing finite-chain law.

Reward from the same demand coordinate used by the update

theorem FD1D.V5.ContinuousProcess.spatialLookup_measurable {m : ℕ} : Measurable fun (p : SpatialState m × Fin m) => p.1 p.2

Evaluation at a measurably selected finite label is measurable.

noncomputable def FD1D.V5.ContinuousProcess.processCost {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (z : ProcessState m) : ℝ

The actual matching cost paid at one joint process state.

Equations

• FD1D.V5.ContinuousProcess.processCost L a fallback z = FD1D.V5.Dynamics.actualStepCost a (FD1D.V5.toConfiguration L z.1) fallback ↑z.2.1

theorem FD1D.V5.ContinuousProcess.processCost_measurable {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) : Measurable (processCost L a fallback)

theorem FD1D.V5.ContinuousProcess.processCost_nonneg {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (z : ProcessState m) : 0 ≤ processCost L a fallback z

theorem FD1D.V5.ContinuousProcess.processCost_le_one {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (z : ProcessState m) : processCost L a fallback z ≤ 1

theorem FD1D.V5.ContinuousProcess.processCost_integrable {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (μ : MeasureTheory.Measure (ProcessState m)) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable (processCost L a fallback) μ

The process cost is integrable under every finite measure.

noncomputable def FD1D.V5.ContinuousProcess.processSquaredCost {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (z : ProcessState m) : ℝ

The squared matching cost paid at one joint process state.

Equations

• FD1D.V5.ContinuousProcess.processSquaredCost L a fallback z = FD1D.V5.Dynamics.actualStepSquaredCost a (FD1D.V5.toConfiguration L z.1) fallback ↑z.2.1

@[simp]

theorem FD1D.V5.ContinuousProcess.processSquaredCost_eq_sq {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (z : ProcessState m) : processSquaredCost L a fallback z = processCost L a fallback z ^ 2

theorem FD1D.V5.ContinuousProcess.processSquaredCost_measurable {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) : Measurable (processSquaredCost L a fallback)

theorem FD1D.V5.ContinuousProcess.processSquaredCost_nonneg {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (z : ProcessState m) : 0 ≤ processSquaredCost L a fallback z

theorem FD1D.V5.ContinuousProcess.processSquaredCost_le_one {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (z : ProcessState m) : processSquaredCost L a fallback z ≤ 1

theorem FD1D.V5.ContinuousProcess.processSquaredCost_integrable {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (μ : MeasureTheory.Measure (ProcessState m)) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable (processSquaredCost L a fallback) μ

The squared process cost is integrable under every finite measure.

theorem FD1D.V5.ContinuousProcess.processAdvance_configuration {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (z : ProcessState m) (fresh : Noise) : toConfiguration L (processAdvance L a fallback (z, fresh)).1 = Dynamics.actualStep a (toConfiguration L z.1) fallback ↑z.2.1 ↑z.2.2 ⋯

The reward and next inventory use the same current demand and replenishment coordinates, pathwise.

theorem FD1D.V5.ContinuousProcess.integral_processCost_noise {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (s : SpatialState m) : ∫ (z : Noise), processCost L a fallback (s, z) ∂noiseLaw = (toConfiguration L s).expectedActualDistance (Dynamics.stateDyadicMass a (spatialCount L s)) fallback

Integrating a fixed inventory over its current noise gives its actual configured cost.

theorem FD1D.V5.ContinuousProcess.integral_processCost_noise_eq_actualConfigurationCost {m : ℕ} (L : ℕ) (a : ℝ) (hm : 0 < m) (s : SpatialState m) : ∫ (z : Noise), processCost L a (SupplyConfiguration.canonicalFallback hm) (s, z) ∂noiseLaw = Dynamics.actualConfigurationCost a hm (toConfiguration L s)

With the canonical fallback, the conditional reward is actualConfigurationCost.

theorem FD1D.V5.ContinuousProcess.integral_processSquaredCost_noise {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (s : SpatialState m) : ∫ (z : Noise), processSquaredCost L a fallback (s, z) ∂noiseLaw = Transport.expectedActualSquaredDistance (toConfiguration L s) (Dynamics.stateDyadicMass a (spatialCount L s)) fallback

Integrating the squared cost over current noise gives the configured conditional second moment.

theorem FD1D.V5.ContinuousProcess.integral_processSquaredCost_noise_eq_actualConfigurationSquaredCost {m : ℕ} (L : ℕ) (a : ℝ) (hm : 0 < m) (s : SpatialState m) : ∫ (z : Noise), processSquaredCost L a (SupplyConfiguration.canonicalFallback hm) (s, z) ∂noiseLaw = Dynamics.actualConfigurationSquaredCost a hm (toConfiguration L s)

With the canonical fallback, the conditional squared reward is actualConfigurationSquaredCost.

theorem FD1D.V5.ContinuousProcess.actualConfigurationCost_spatial_integrable {L m : ℕ} (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : MeasureTheory.Integrable (fun (s : SpatialState m) => Dynamics.actualConfigurationCost a hm (toConfiguration L s)) (spatialLaw a fallback t)

The configured-cost observable is integrable under every spatial marginal.

theorem FD1D.V5.ContinuousProcess.integral_processCost_processLaw {L m : ℕ} (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : ∫ (z : ProcessState m), processCost L a (SupplyConfiguration.canonicalFallback hm) z ∂processLaw a fallback t = ∫ (s : SpatialState m), Dynamics.actualConfigurationCost a hm (toConfiguration L s) ∂spatialLaw a fallback t

Expected joint-state reward equals expected configured inventory cost.

noncomputable def FD1D.V5.ContinuousProcess.trajectoryExpectedCost {L m : ℕ} (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : ℝ

One-period reward, integrated on the single infinite trajectory law.

Equations

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

theorem FD1D.V5.ContinuousProcess.trajectoryExpectedCost_eq_spatial {L m : ℕ} (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : trajectoryExpectedCost a hm fallback t = ∫ (s : SpatialState m), Dynamics.actualConfigurationCost a hm (toConfiguration L s) ∂spatialLaw a fallback t

The path-coordinate reward is the corresponding spatial marginal cost.

theorem FD1D.V5.ContinuousProcess.actualConfigurationSquaredCost_spatial_integrable {L m : ℕ} (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : MeasureTheory.Integrable (fun (s : SpatialState m) => Dynamics.actualConfigurationSquaredCost a hm (toConfiguration L s)) (spatialLaw a fallback t)

The configured squared-cost observable is integrable under every spatial marginal.

theorem FD1D.V5.ContinuousProcess.integral_processSquaredCost_processLaw {L m : ℕ} (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : ∫ (z : ProcessState m), processSquaredCost L a (SupplyConfiguration.canonicalFallback hm) z ∂processLaw a fallback t = ∫ (s : SpatialState m), Dynamics.actualConfigurationSquaredCost a hm (toConfiguration L s) ∂spatialLaw a fallback t

Expected joint-state squared reward equals expected configured squared inventory cost.

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

One-period squared reward, integrated on the single infinite trajectory law.

Equations

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

theorem FD1D.V5.ContinuousProcess.trajectoryExpectedSquaredCost_eq_spatial {L m : ℕ} (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : trajectoryExpectedSquaredCost a hm fallback t = ∫ (s : SpatialState m), Dynamics.actualConfigurationSquaredCost a hm (toConfiguration L s) ∂spatialLaw a fallback t

The path-coordinate squared reward is the corresponding spatial marginal cost.