Initial Process

Spatial evolution from an arbitrary initial law

noncomputable def FD1D.V5.ContinuousProcess.spatialLawFrom {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure (SpatialState m)

The continuous spatial law after t policy steps, starting from μ₀.

Equations

• FD1D.V5.ContinuousProcess.spatialLawFrom μ₀ a fallback t = FD1D.TrajectoryBridge.iterateLaw (FD1D.V5.ContinuousProcess.spatialKernel a fallback) μ₀ t

@[simp]

theorem FD1D.V5.ContinuousProcess.spatialLawFrom_zero {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) (a : ℝ) (fallback : Fin m) : spatialLawFrom μ₀ a fallback 0 = μ₀

@[simp]

theorem FD1D.V5.ContinuousProcess.spatialLawFrom_succ {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) (a : ℝ) (fallback : Fin m) (t : ℕ) : spatialLawFrom μ₀ a fallback (t + 1) = (spatialLawFrom μ₀ a fallback t).bind ⇑(spatialKernel a fallback)

instance FD1D.V5.ContinuousProcess.spatialLawFrom.isProbabilityMeasure {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.IsProbabilityMeasure (spatialLawFrom μ₀ a fallback t)

theorem FD1D.V5.ContinuousProcess.map_spatialCount_spatialLawFrom {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) (ν₀ : FiniteLaw (InventoryState (DyadicNode L) m)) (hμ₀ : MeasureTheory.Measure.map (spatialCount L) μ₀ = ν₀.toMeasure) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure.map (spatialCount L) (spatialLawFrom μ₀ a fallback t) = ((Dynamics.kernel a ha hm).iterate t ν₀).toMeasure

If μ₀ projects to the finite count law ν₀, every later spatial marginal projects to the corresponding iterate of the finite count kernel.

Joint process and trajectory laws

noncomputable def FD1D.V5.ContinuousProcess.initialProcessLawFrom {m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) : MeasureTheory.Measure (ProcessState m)

Attach an independent first demand/replenishment pair to μ₀.

Equations

• FD1D.V5.ContinuousProcess.initialProcessLawFrom μ₀ = μ₀.prod FD1D.V5.ContinuousProcess.noiseLaw

@[simp]

theorem FD1D.V5.ContinuousProcess.initialProcessLawFrom_eq_product {m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) : initialProcessLawFrom μ₀ = μ₀.prod noiseLaw

instance FD1D.V5.ContinuousProcess.initialProcessLawFrom.isProbabilityMeasure {m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] : MeasureTheory.IsProbabilityMeasure (initialProcessLawFrom μ₀)

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

The joint process law at time t, starting from spatial law μ₀.

Equations

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

instance FD1D.V5.ContinuousProcess.processLawFrom.isProbabilityMeasure {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.IsProbabilityMeasure (processLawFrom μ₀ a fallback t)

theorem FD1D.V5.ContinuousProcess.processLawFrom_eq_product {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (a : ℝ) (fallback : Fin m) (t : ℕ) : processLawFrom μ₀ a fallback t = (spatialLawFrom μ₀ a fallback t).prod noiseLaw

Current noise stays independent of the live inventory for every μ₀.

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

One path-space law for the joint process initialized by μ₀.

Equations

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

instance FD1D.V5.ContinuousProcess.trajectoryLawFrom.isProbabilityMeasure {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (a : ℝ) (fallback : Fin m) : MeasureTheory.IsProbabilityMeasure (trajectoryLawFrom μ₀ a fallback)

theorem FD1D.V5.ContinuousProcess.trajectoryLawFrom_marginal {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure.map (fun (path : ℕ → ProcessState m) => path t) (trajectoryLawFrom μ₀ a fallback) = processLawFrom μ₀ a fallback t

Each trajectory coordinate has the recursively iterated joint-state law.

theorem FD1D.V5.ContinuousProcess.trajectoryLawFrom_count_marginal {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (ν₀ : FiniteLaw (InventoryState (DyadicNode L) m)) (hμ₀ : MeasureTheory.Measure.map (spatialCount L) μ₀ = ν₀.toMeasure) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure.map (fun (path : ℕ → ProcessState m) => spatialCount L (path t).1) (trajectoryLawFrom μ₀ a fallback) = ((Dynamics.kernel a ha hm).iterate t ν₀).toMeasure

Every trajectory count coordinate has the corresponding finite iterate.

One-period cost from an arbitrary initial law

theorem FD1D.V5.ContinuousProcess.actualConfigurationSquaredCost_spatialLawFrom_integrable {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : MeasureTheory.Integrable (fun (s : SpatialState m) => Dynamics.actualConfigurationSquaredCost a hm (toConfiguration L s)) (spatialLawFrom μ₀ a fallback t)

The configured-cost observable is integrable under each generalized spatial law.

theorem FD1D.V5.ContinuousProcess.integral_processSquaredCost_processLawFrom {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : ∫ (z : ProcessState m), processSquaredCost L a (SupplyConfiguration.canonicalFallback hm) z ∂processLawFrom μ₀ a fallback t = ∫ (s : SpatialState m), Dynamics.actualConfigurationSquaredCost a hm (toConfiguration L s) ∂spatialLawFrom μ₀ a fallback t

Joint-state expected cost equals the generalized spatial configured-cost integral.

noncomputable def FD1D.V5.ContinuousProcess.trajectoryExpectedSquaredCostFrom {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : ℝ

One-period cost on the generalized path-space law.

Equations

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

theorem FD1D.V5.ContinuousProcess.trajectoryExpectedSquaredCostFrom_eq_spatial {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (a : ℝ) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : trajectoryExpectedSquaredCostFrom μ₀ a hm fallback t = ∫ (s : SpatialState m), Dynamics.actualConfigurationSquaredCost a hm (toConfiguration L s) ∂spatialLawFrom μ₀ a fallback t

Generalized trajectory cost equals the spatial configured-cost integral.

theorem FD1D.V5.ContinuousProcess.trajectoryExpectedSquaredCostFrom_le_envelope {L m : ℕ} (μ₀ : MeasureTheory.Measure (SpatialState m)) [MeasureTheory.IsProbabilityMeasure μ₀] (ν₀ : FiniteLaw (InventoryState (DyadicNode L) m)) (hμ₀ : MeasureTheory.Measure.map (spatialCount L) μ₀ = ν₀.toMeasure) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : trajectoryExpectedSquaredCostFrom μ₀ a hm fallback t ≤ ((Dynamics.kernel a ha hm).iterate t ν₀).expect (Transport.stateSquaredCostEnvelope a)

The generalized one-period cost is bounded by the matching finite iterate.

Fixed-initial-state specializations

theorem FD1D.V5.ContinuousProcess.toMeasure_dirac {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [DecidableEq α] (x : α) : (FiniteLaw.dirac x).toMeasure = MeasureTheory.Measure.dirac x

A finite point law is represented by the corresponding measure-theoretic Dirac law.

theorem FD1D.V5.ContinuousProcess.map_spatialCount_dirac {m : ℕ} (L : ℕ) (s₀ : SpatialState m) : MeasureTheory.Measure.map (spatialCount L) (MeasureTheory.Measure.dirac s₀) = (FiniteLaw.dirac (spatialCount L s₀)).toMeasure

The count pushforward of a fixed spatial state is its finite point law.

noncomputable def FD1D.V5.ContinuousProcess.spatialLawFromState {L m : ℕ} (s₀ : SpatialState m) (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure (SpatialState m)

Spatial evolution from the fixed initial state s₀.

Equations

• FD1D.V5.ContinuousProcess.spatialLawFromState s₀ a fallback t = FD1D.V5.ContinuousProcess.spatialLawFrom (MeasureTheory.Measure.dirac s₀) a fallback t

noncomputable def FD1D.V5.ContinuousProcess.initialProcessLawFromState {m : ℕ} (s₀ : SpatialState m) : MeasureTheory.Measure (ProcessState m)

The initial joint law for a fixed spatial state.

Equations

• FD1D.V5.ContinuousProcess.initialProcessLawFromState s₀ = FD1D.V5.ContinuousProcess.initialProcessLawFrom (MeasureTheory.Measure.dirac s₀)

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

Joint process evolution from a fixed spatial state.

Equations

• FD1D.V5.ContinuousProcess.processLawFromState s₀ a fallback t = FD1D.V5.ContinuousProcess.processLawFrom (MeasureTheory.Measure.dirac s₀) a fallback t

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

Path-space law from a fixed spatial state.

Equations

• FD1D.V5.ContinuousProcess.trajectoryLawFromState s₀ a fallback = FD1D.V5.ContinuousProcess.trajectoryLawFrom (MeasureTheory.Measure.dirac s₀) a fallback

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

One-period trajectory cost from a fixed spatial state.

Equations

• FD1D.V5.ContinuousProcess.trajectoryExpectedSquaredCostFromState s₀ a hm fallback t = FD1D.V5.ContinuousProcess.trajectoryExpectedSquaredCostFrom (MeasureTheory.Measure.dirac s₀) a hm fallback t

theorem FD1D.V5.ContinuousProcess.map_spatialCount_spatialLawFromState {L m : ℕ} (s₀ : SpatialState m) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure.map (spatialCount L) (spatialLawFromState s₀ a fallback t) = ((Dynamics.kernel a ha hm).iterate t (FiniteLaw.dirac (spatialCount L s₀))).toMeasure

Fixed-state spatial counts follow the finite kernel from the matching point law.

theorem FD1D.V5.ContinuousProcess.processLawFromState_eq_product {L m : ℕ} (s₀ : SpatialState m) (a : ℝ) (fallback : Fin m) (t : ℕ) : processLawFromState s₀ a fallback t = (spatialLawFromState s₀ a fallback t).prod noiseLaw

Fixed-state process laws retain the spatial/noise product factorization.

theorem FD1D.V5.ContinuousProcess.trajectoryLawFromState_marginal {L m : ℕ} (s₀ : SpatialState m) (a : ℝ) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure.map (fun (path : ℕ → ProcessState m) => path t) (trajectoryLawFromState s₀ a fallback) = processLawFromState s₀ a fallback t

Fixed-state trajectory coordinates have the corresponding process laws.

theorem FD1D.V5.ContinuousProcess.trajectoryLawFromState_count_marginal {L m : ℕ} (s₀ : SpatialState m) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : MeasureTheory.Measure.map (fun (path : ℕ → ProcessState m) => spatialCount L (path t).1) (trajectoryLawFromState s₀ a fallback) = ((Dynamics.kernel a ha hm).iterate t (FiniteLaw.dirac (spatialCount L s₀))).toMeasure

Fixed-state trajectory counts follow the finite kernel from the matching point law.

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

Fixed-state trajectory cost equals its spatial configured-cost integral.

theorem FD1D.V5.ContinuousProcess.trajectoryExpectedSquaredCostFromState_le_envelope {L m : ℕ} (s₀ : SpatialState m) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (t : ℕ) : trajectoryExpectedSquaredCostFromState s₀ a hm fallback t ≤ ((Dynamics.kernel a ha hm).iterate t (FiniteLaw.dirac (spatialCount L s₀))).expect (Transport.stateSquaredCostEnvelope a)

Fixed-state trajectory cost is bounded by its finite-kernel iterate.