Parameterized trajectories on countable dense time

def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.trajectoryCoordinate {Theta : Type uTheta} {alpha : Type uAlpha} : ℕ → Type (max uTheta uAlpha)

The initial parameter and state at zero, followed by lifted state observations.

Equations

• MarkovProcess.ParameterizedSubMarkovKernelSemigroup.trajectoryCoordinate 0 = ULift.{max ?u.2 ?u.1, max ?u.1 ?u.2} (Theta × alpha)
• MarkovProcess.ParameterizedSubMarkovKernelSemigroup.trajectoryCoordinate n.succ = ULift.{max ?u.4 ?u.3, ?u.3} alpha

@[instance_reducible]

instance MarkovProcess.ParameterizedSubMarkovKernelSemigroup.instMeasurableSpaceTrajectoryCoordinate {Theta : Type uTheta} {alpha : Type uAlpha} [MeasurableSpace Theta] [MeasurableSpace alpha] (n : ℕ) : MeasurableSpace (trajectoryCoordinate n)

Equations

• MarkovProcess.ParameterizedSubMarkovKernelSemigroup.instMeasurableSpaceTrajectoryCoordinate 0 = inferInstance
• MarkovProcess.ParameterizedSubMarkovKernelSemigroup.instMeasurableSpaceTrajectoryCoordinate n_1.succ = inferInstance

def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.historyInitial {Theta : Type uTheta} {alpha : Type uAlpha} (n : ℕ) (path : (i : ↥(Finset.Iic n)) → trajectoryCoordinate ↑i) : ULift.{max uTheta uAlpha, max uAlpha uTheta} (Theta × alpha)

Extract the immutable parameter and initial state from an augmented history.

Equations

• MarkovProcess.ParameterizedSubMarkovKernelSemigroup.historyInitial n path = path ⟨0, ⋯⟩

def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.historyObservation {Theta : Type uTheta} {alpha : Type uAlpha} (n : ℕ) (path : (i : ↥(Finset.Iic n)) → trajectoryCoordinate ↑i) (i : Fin n) : ULift.{max uTheta uAlpha, uAlpha} alpha

Extract one observed state from an augmented finite history.

Equations

• MarkovProcess.ParameterizedSubMarkovKernelSemigroup.historyObservation n path i = path ⟨↑i + 1, ⋯⟩

@[irreducible]

def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.historyEquiv {Theta : Type uTheta} {alpha : Type uAlpha} [MeasurableSpace Theta] [MeasurableSpace alpha] (n : ℕ) : ((i : ↥(Finset.Iic n)) → trajectoryCoordinate ↑i) ≃ᵐ (Theta × alpha) × (Fin n → alpha)

An augmented history is exactly the immutable data and its observed prefix.

Equations

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

noncomputable def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedTrajStep {Theta : Type uTheta} {D : Type u_1} {alpha : Type uAlpha} [MeasurableSpace Theta] [MeasurableSpace alpha] [StandardBorelSpace alpha] [Nonempty alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (hP : ∀ (theta : Theta), (P.toSubMarkovKernelSemigroup theta).IsConservative) (e : ℕ ≃ D) (iota : D ↪ NNReal) (n : ℕ) : ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → trajectoryCoordinate ↑i) (trajectoryCoordinate (n + 1))

The next conditional observation kernel, transported to augmented histories.

Equations

• P.parameterizedTrajStep hP e iota n = ((P.parameterizedObservationCondKernel hP e iota n).map ULift.up).comap ⇑(MarkovProcess.ParameterizedSubMarkovKernelSemigroup.historyEquiv n) ⋯

instance MarkovProcess.ParameterizedSubMarkovKernelSemigroup.isMarkovKernel_parameterizedTrajStep {Theta : Type uTheta} {D : Type u_1} {alpha : Type uAlpha} [MeasurableSpace Theta] [MeasurableSpace alpha] [StandardBorelSpace alpha] [Nonempty alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (hP : ∀ (theta : Theta), (P.toSubMarkovKernelSemigroup theta).IsConservative) (e : ℕ ≃ D) (iota : D ↪ NNReal) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (P.parameterizedTrajStep hP e iota n)

def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.initialHistory {Theta : Type uTheta} {alpha : Type uAlpha} (q : Theta × alpha) (i : ↥(Finset.Iic 0)) : trajectoryCoordinate ↑i

The augmented history containing only the initial parameter and state.

Equations

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

def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.eraseAugmentation {Theta : Type uTheta} {D : Type u_1} {alpha : Type uAlpha} (e : ℕ ≃ D) (path : (n : ℕ) → trajectoryCoordinate n) : D → alpha

Remove the immutable coordinate and reindex observations by the dense-time labels.

Equations

• MarkovProcess.ParameterizedSubMarkovKernelSemigroup.eraseAugmentation e path d = (path (e.symm d + 1)).down

noncomputable def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedDenseTimeTrajectory {Theta : Type uTheta} {D : Type u_1} {alpha : Type uAlpha} [MeasurableSpace Theta] [MeasurableSpace alpha] [StandardBorelSpace alpha] [Nonempty alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (hP : ∀ (theta : Theta), (P.toSubMarkovKernelSemigroup theta).IsConservative) (e : ℕ ≃ D) (iota : D ↪ NNReal) : ProbabilityTheory.Kernel (Theta × alpha) (D → alpha)

The jointly measurable dense-time trajectory kernel.

Equations

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

theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.isMarkovKernel_parameterizedDenseTimeTrajectory {Theta : Type uTheta} {D : Type u_1} {alpha : Type uAlpha} [MeasurableSpace Theta] [MeasurableSpace alpha] [StandardBorelSpace alpha] [Nonempty alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (hP : ∀ (theta : Theta), (P.toSubMarkovKernelSemigroup theta).IsConservative) (e : ℕ ≃ D) (iota : D ↪ NNReal) : ProbabilityTheory.IsMarkovKernel (P.parameterizedDenseTimeTrajectory hP e iota)

The parameterized dense-time trajectory kernel is Markov.

theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedDenseTimeTrajectory_map_prefix {Theta : Type uTheta} {D : Type u_1} {alpha : Type uAlpha} [MeasurableSpace Theta] [MeasurableSpace alpha] [StandardBorelSpace alpha] [Nonempty alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (hP : ∀ (theta : Theta), (P.toSubMarkovKernelSemigroup theta).IsConservative) (e : ℕ ≃ D) (iota : D ↪ NNReal) (n : ℕ) : (P.parameterizedDenseTimeTrajectory hP e iota).map (SubMarkovKernelSemigroup.IsConservative.denseTimeTrajectoryPrefix e n) = P.parameterizedDenseTimePrefixKernel e iota n

Restricting the trajectory to the first n enumeration labels gives exactly the parameterized prefix kernel.