Prequential risk for history-dependent trajectory kernels

This file extends the finite-state trajectory-risk layer from time-homogeneous Markov transitions to arbitrary prefix-dependent kernels. At time n, the kernel may inspect the entire prefix indexed by Finset.Iic n, and the score may depend on that prefix and the next state. For any score taking values in [0, 1], the observed score minus its kernel-conditional risk is an adapted, conditionally centered innovation with conditional second moment at most 1 / 4.

The existing Markov API remains unchanged. The final bridge lemmas identify its path law, squared loss, conditional risk, and innovation as special cases of the prefix-dependent definitions.

@[reducible, inline]

abbrev FormalSLT.StochasticDynamics.TrajectoryScore (Z : Type u_2) : Type u_2

A one-step score which may inspect the complete trajectory prefix before scoring the next state.

Equations

• FormalSLT.StochasticDynamics.TrajectoryScore Z = ((n : ℕ) → (↥(Finset.Iic n) → Z) → Z → ℝ)

noncomputable def FormalSLT.StochasticDynamics.trajectoryMeasure {Z : Type u_1} [MeasurableSpace Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (x0 : Z) : MeasureTheory.Measure (ℕ → Z)

The Ionescu--Tulcea path law generated by a deterministic initial state and an arbitrary family of prefix-dependent Markov kernels.

Equations

• FormalSLT.StochasticDynamics.trajectoryMeasure κ x0 = (ProbabilityTheory.Kernel.traj κ 0) fun (x : ↥(Finset.Iic 0)) => x0

instance FormalSLT.StochasticDynamics.trajectoryMeasure.instIsProbabilityMeasure {Z : Type u_1} [MeasurableSpace Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (x0 : Z) : MeasureTheory.IsProbabilityMeasure (trajectoryMeasure κ x0)

def FormalSLT.StochasticDynamics.observedTrajectoryScore {Z : Type u_1} (score : TrajectoryScore Z) (n : ℕ) (x : ℕ → Z) : ℝ

The score observed after extending a path prefix by its next state.

Equations

• FormalSLT.StochasticDynamics.observedTrajectoryScore score n x = score n (Preorder.frestrictLe n x) (x (n + 1))

noncomputable def FormalSLT.StochasticDynamics.conditionalTrajectoryRisk {Z : Type u_1} [MeasurableSpace Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) (score : TrajectoryScore Z) (n : ℕ) (x : ℕ → Z) : ℝ

The one-step score averaged against the kernel selected by the observed prefix.

Equations

• FormalSLT.StochasticDynamics.conditionalTrajectoryRisk κ score n x = ∫ (y : Z), score n (Preorder.frestrictLe n x) y ∂(κ n) (Preorder.frestrictLe n x)

theorem FormalSLT.StochasticDynamics.stronglyMeasurable_observedTrajectoryScore_succ {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (score : TrajectoryScore Z) (n : ℕ) : MeasureTheory.StronglyMeasurable (observedTrajectoryScore score n)

The observed score at step n is measurable with respect to the path through coordinate n + 1.

theorem FormalSLT.StochasticDynamics.measurable_observedTrajectoryScore {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (score : TrajectoryScore Z) (n : ℕ) : Measurable (observedTrajectoryScore score n)

theorem FormalSLT.StochasticDynamics.observedTrajectoryScore_mem_Icc {Z : Type u_1} {score : TrajectoryScore Z} (hscore : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score n u y ∈ Set.Icc 0 1) (n : ℕ) (x : ℕ → Z) : observedTrajectoryScore score n x ∈ Set.Icc 0 1

theorem FormalSLT.StochasticDynamics.integrable_observedTrajectoryScore {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] {κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z} [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {x0 : Z} {score : TrajectoryScore Z} (hscore : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score n u y ∈ Set.Icc 0 1) (n : ℕ) : MeasureTheory.Integrable (observedTrajectoryScore score n) (trajectoryMeasure κ x0)

theorem FormalSLT.StochasticDynamics.map_trajectory_next {Z : Type u_1} [MeasurableSpace Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (n : ℕ) (u : ↥(Finset.Iic n) → Z) : MeasureTheory.Measure.map (fun (x : ℕ → Z) => x (n + 1)) ((ProbabilityTheory.Kernel.traj κ n) u) = (κ n) u

Under a trajectory continuation from prefix u, coordinate n + 1 has exactly the law selected by the prefix-dependent kernel κ n u.

theorem FormalSLT.StochasticDynamics.integral_observedTrajectoryScore_traj {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (score : TrajectoryScore Z) (n : ℕ) (u : ↥(Finset.Iic n) → Z) : ∫ (x : ℕ → Z), observedTrajectoryScore score n x ∂(ProbabilityTheory.Kernel.traj κ n) u = ∫ (y : Z), score n u y ∂(κ n) u

Integrating the observed score against a trajectory continuation is the kernel-conditional risk associated with its supplied prefix.

theorem FormalSLT.StochasticDynamics.observedTrajectoryScore_condExp {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (x0 : Z) (score : TrajectoryScore Z) (hscore : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score n u y ∈ Set.Icc 0 1) (n : ℕ) : (trajectoryMeasure κ x0)[observedTrajectoryScore score n | ↑MeasureTheory.Filtration.piLE n] =ᵐ[trajectoryMeasure κ x0] conditionalTrajectoryRisk κ score n

The trajectory construction determines the exact conditional expectation of the next score from the whole observed prefix.

theorem FormalSLT.StochasticDynamics.stronglyMeasurable_conditionalTrajectoryRisk {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) (score : TrajectoryScore Z) (n : ℕ) : MeasureTheory.StronglyMeasurable (conditionalTrajectoryRisk κ score n)

theorem FormalSLT.StochasticDynamics.conditionalTrajectoryRisk_mem_Icc {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {score : TrajectoryScore Z} (hscore : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score n u y ∈ Set.Icc 0 1) (n : ℕ) (x : ℕ → Z) : conditionalTrajectoryRisk κ score n x ∈ Set.Icc 0 1

theorem FormalSLT.StochasticDynamics.integrable_conditionalTrajectoryRisk {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] {κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z} [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {x0 : Z} {score : TrajectoryScore Z} (hscore : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score n u y ∈ Set.Icc 0 1) (n : ℕ) : MeasureTheory.Integrable (conditionalTrajectoryRisk κ score n) (trajectoryMeasure κ x0)

noncomputable def FormalSLT.StochasticDynamics.trajectoryRiskInnovation {Z : Type u_1} [MeasurableSpace Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) (score : TrajectoryScore Z) (n : ℕ) (x : ℕ → Z) : ℝ

Observed score minus its exact prefix-conditional risk.

Equations

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

theorem FormalSLT.StochasticDynamics.trajectoryRiskInnovation_incrementAdapted {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) (score : TrajectoryScore Z) : AnytimeValid.IncrementAdapted MeasureTheory.Filtration.piLE (trajectoryRiskInnovation κ score)

theorem FormalSLT.StochasticDynamics.measurable_trajectoryRiskInnovation {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) (score : TrajectoryScore Z) (n : ℕ) : Measurable (trajectoryRiskInnovation κ score n)

theorem FormalSLT.StochasticDynamics.abs_trajectoryRiskInnovation_le_one {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {score : TrajectoryScore Z} (hscore : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score n u y ∈ Set.Icc 0 1) (n : ℕ) (x : ℕ → Z) : |trajectoryRiskInnovation κ score n x| ≤ 1

theorem FormalSLT.StochasticDynamics.integrable_trajectoryRiskInnovation {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] {κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z} [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {x0 : Z} {score : TrajectoryScore Z} (hscore : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score n u y ∈ Set.Icc 0 1) (n : ℕ) : MeasureTheory.Integrable (trajectoryRiskInnovation κ score n) (trajectoryMeasure κ x0)

theorem FormalSLT.StochasticDynamics.trajectoryRiskInnovation_condExp_eq_zero {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (x0 : Z) {score : TrajectoryScore Z} (hscore : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score n u y ∈ Set.Icc 0 1) (n : ℕ) : (trajectoryMeasure κ x0)[trajectoryRiskInnovation κ score n | ↑MeasureTheory.Filtration.piLE n] =ᵐ[trajectoryMeasure κ x0] 0

The prefix-dependent trajectory innovation is conditionally centered under the path law generated by the same kernels.

theorem FormalSLT.StochasticDynamics.trajectoryRiskInnovation_condSecondMoment_le_one_fourth {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (κ : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (x0 : Z) {score : TrajectoryScore Z} (hscore : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score n u y ∈ Set.Icc 0 1) (n : ℕ) : (trajectoryMeasure κ x0)[fun (x : ℕ → Z) => trajectoryRiskInnovation κ score n x ^ 2 | ↑MeasureTheory.Filtration.piLE n] ≤ᵐ[trajectoryMeasure κ x0] fun (x : ℕ → Z) => 1 / 4

A [0,1] prefix-dependent score has conditional centered second moment at most 1 / 4, with no stationarity or finite-memory assumption on the kernels.

theorem FormalSLT.StochasticDynamics.trajectoryMeasure_prefixKernel_eq_markovPathMeasure {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (P : Z → PMF Z) (x0 : Z) : trajectoryMeasure (prefixKernel P) x0 = markovPathMeasure P x0

The Markov path measure is the specialization of trajectoryMeasure to the current-state prefixKernel.

def FormalSLT.StochasticDynamics.markovSquaredTrajectoryScore {Z : Type u_1} (f q : Z → ℝ) : TrajectoryScore Z

Squared Markov loss as a prefix-dependent trajectory score.

Equations

• FormalSLT.StochasticDynamics.markovSquaredTrajectoryScore f q n u y = FormalSLT.StochasticDynamics.transitionSquaredLoss f q (u ⟨n, ⋯⟩) y

theorem FormalSLT.StochasticDynamics.observedTrajectoryScore_markovSquaredTrajectoryScore {Z : Type u_1} (f q : Z → ℝ) (n : ℕ) (x : ℕ → Z) : observedTrajectoryScore (markovSquaredTrajectoryScore f q) n x = pathSquaredLoss f q n x

theorem FormalSLT.StochasticDynamics.conditionalTrajectoryRisk_markovSquaredTrajectoryScore {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (P : Z → PMF Z) (f q : Z → ℝ) (n : ℕ) (x : ℕ → Z) : conditionalTrajectoryRisk (prefixKernel P) (markovSquaredTrajectoryScore f q) n x = conditionalSquaredRisk P f q n x

theorem FormalSLT.StochasticDynamics.trajectoryRiskInnovation_markovSquaredTrajectoryScore {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (P : Z → PMF Z) (f q : Z → ℝ) (n : ℕ) (x : ℕ → Z) : trajectoryRiskInnovation (prefixKernel P) (markovSquaredTrajectoryScore f q) n x = markovRiskInnovation P f q n x

theorem FormalSLT.StochasticDynamics.pathSquaredLoss_condExp_via_trajectory {Z : Type u_1} [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (P : Z → PMF Z) (x0 : Z) (f q : Z → ℝ) (hf : ∀ (z : Z), f z ∈ Set.Icc 0 1) (hq : ∀ (z : Z), q z ∈ Set.Icc 0 1) (n : ℕ) : (markovPathMeasure P x0)[pathSquaredLoss f q n | ↑MeasureTheory.Filtration.piLE n] =ᵐ[markovPathMeasure P x0] conditionalSquaredRisk P f q n

The original homogeneous-Markov squared-loss conditional-expectation theorem is an instance of the prefix-dependent trajectory theorem.