Ordinary suffix risk for time-varying predictable tilts

The sleeping predictable-tilt theorem controls a normalized, tilt-weighted conditional-risk average. This module compares that target with the ordinary uniform average on the same suffix. The comparison cost is the total variation distance between the uniform suffix weights and the realized normalized tilt weights.

For losses in [0,1], the conditional-risk and empirical-risk comparisons each cost at most this discrepancy. Consequently, the existing weighted PAC-Bayes certificate implies an ordinary encountered suffix-risk certificate with an explicit 2 * discrepancy surcharge. Constant positive post-wake tilts have zero discrepancy and recover the exact constant-tilt specialization.

The strategy catalog is still fixed before observing the trajectory, and each strategy remains predictable. The target is encountered conditional risk on the monitored suffix, not future, stationary, population, or deployment risk.

A reusable finite total-variation comparison

noncomputable def FormalSLT.StochasticDynamics.finiteUniformNormalizedWeightDiscrepancy {Alpha : Type u_3} (s : Finset Alpha) (weight : Alpha → ℝ) (exposure : ℝ) : ℝ

Half the finite L1 distance between a uniform distribution on s and weights weight / exposure. The definition is total; comparison theorems assume that s is nonempty and that exposure is the sum of the weights.

Equations

• FormalSLT.StochasticDynamics.finiteUniformNormalizedWeightDiscrepancy s weight exposure = 1 / 2 * ∑ i ∈ s, |(↑s.card)⁻¹ - weight i / exposure|

theorem FormalSLT.StochasticDynamics.abs_weightedSum_sub_weightedSum_le_half_l1 {Alpha : Type u_3} (s : Finset Alpha) (p q value : Alpha → ℝ) (hp : ∑ i ∈ s, p i = 1) (hq : ∑ i ∈ s, q i = 1) (hvalue : ∀ i ∈ s, value i ∈ Set.Icc 0 1) : |∑ i ∈ s, p i * value i - ∑ i ∈ s, q i * value i| ≤ 1 / 2 * ∑ i ∈ s, |p i - q i|

A [0,1]-valued function changes by at most half the L1 distance between two finite unit-mass weight vectors. Nonnegativity of the vectors is not needed for this deterministic inequality.

theorem FormalSLT.StochasticDynamics.abs_uniformAverage_sub_normalizedWeightedAverage_le_discrepancy {Alpha : Type u_3} (s : Finset Alpha) (hs : s.Nonempty) (weight value : Alpha → ℝ) {exposure : ℝ} (hexposure : exposure ≠ 0) (hsum : ∑ i ∈ s, weight i = exposure) (hvalue : ∀ i ∈ s, value i ∈ Set.Icc 0 1) : |(∑ i ∈ s, value i) / ↑s.card - (∑ i ∈ s, weight i * value i) / exposure| ≤ finiteUniformNormalizedWeightDiscrepancy s weight exposure

A normalized weighted average of [0,1] values differs from their uniform average by at most finiteUniformNormalizedWeightDiscrepancy.

Suffix weights and discrepancy

noncomputable def FormalSLT.StochasticDynamics.continuousTrajectorySleepingPredictableTiltUniformDiscrepancy {Z : Type u_2} (strategy : ℕ → TrajectoryPredictableTilt Z) (j n : ℕ) (x : ℕ → Z) : ℝ

Realized total-variation discrepancy between uniform weights on [j,n) and the normalized weights of sleeping atom j.

Equations

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

theorem FormalSLT.StochasticDynamics.continuousTrajectorySleepingPredictableTiltExposure_eq_sum_Ico {Z : Type u_2} (strategy : ℕ → TrajectoryPredictableTilt Z) {j n : ℕ} (hjn : j ≤ n) (x : ℕ → Z) : PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x = ∑ k ∈ Finset.Ico j n, observedTrajectoryPredictableTilt (strategy j) k x

theorem FormalSLT.StochasticDynamics.abs_trajectoryConditionalSuffixAverage_sub_sleepingNormalizedConditionalMeanAt_le {Theta : Type u_1} {Z : Type u_2} (mean : Theta → ℕ → (ℕ → Z) → ℝ) (strategy : ℕ → TrajectoryPredictableTilt Z) (theta : Theta) {j n : ℕ} (hjn : j < n) (x : ℕ → Z) (hexposure : 0 < PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x) (hmean : ∀ k ∈ Finset.Ico j n, mean theta k x ∈ Set.Icc 0 1) : |(∑ k ∈ Finset.Ico j n, mean theta k x) / ↑(n - j) - PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingWeightedConditionalMeanAt mean (observedTrajectoryPredictableStrategyCatalog strategy) theta j n x / PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x| ≤ continuousTrajectorySleepingPredictableTiltUniformDiscrepancy strategy j n x

Pointwise conditional-risk comparison between the ordinary suffix average and the normalized time-varying predictable-tilt average.

theorem FormalSLT.StochasticDynamics.abs_trajectoryEmpiricalSuffixAverage_sub_sleepingNormalizedObservationAt_le {Theta : Type u_1} {Z : Type u_2} (X : Theta → ℕ → (ℕ → Z) → ℝ) (strategy : ℕ → TrajectoryPredictableTilt Z) (theta : Theta) {j n : ℕ} (hjn : j < n) (x : ℕ → Z) (hexposure : 0 < PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x) (hX : ∀ k ∈ Finset.Ico j n, X theta k x ∈ Set.Icc 0 1) : |(∑ k ∈ Finset.Ico j n, X theta k x) / ↑(n - j) - PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingWeightedObservationAt X (observedTrajectoryPredictableStrategyCatalog strategy) theta j n x / PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x| ≤ continuousTrajectorySleepingPredictableTiltUniformDiscrepancy strategy j n x

Pointwise empirical-risk comparison for the same realized predictable weights.

Posterior deviations and the PAC-Bayes bridge

theorem FormalSLT.StochasticDynamics.abs_continuousTrajectoryPosteriorAverageConditionalSuffixRisk_sub_normalized_le {Theta : Type u_1} {Z : Type u_2} [MeasurableSpace Theta] [MeasurableSpace Z] (K : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) (score : Theta → TrajectoryScore Z) (posterior : MeasureTheory.Measure Theta) [MeasureTheory.IsProbabilityMeasure posterior] (strategy : ℕ → TrajectoryPredictableTilt Z) {j n : ℕ} (hjn : j < n) (x : ℕ → Z) (hexposure : 0 < PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x) (hscore : ∀ (theta : Theta) (k : ℕ), conditionalTrajectoryRisk K (score theta) k x ∈ Set.Icc 0 1) (hordinary : MeasureTheory.Integrable (fun (theta : Theta) => (∑ k ∈ Finset.Ico j n, conditionalTrajectoryRisk K (score theta) k x) / ↑(n - j)) posterior) (hweighted : MeasureTheory.Integrable (fun (theta : Theta) => PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingWeightedConditionalMeanAt (fun (theta : Theta) => conditionalTrajectoryRisk K (score theta)) (observedTrajectoryPredictableStrategyCatalog strategy) theta j n x / PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x) posterior) : |continuousTrajectoryPosteriorAverageConditionalSuffixRisk K score posterior j n x - continuousTrajectorySleepingPosteriorNormalizedConditionalRisk K score strategy posterior j n x| ≤ continuousTrajectorySleepingPredictableTiltUniformDiscrepancy strategy j n x

Posterior-level conditional-risk deviation. The explicit integrability premises make this lemma reusable independently of the trajectory master.

theorem FormalSLT.StochasticDynamics.abs_continuousTrajectoryPosteriorEmpiricalSuffixRisk_sub_normalized_le {Theta : Type u_1} {Z : Type u_2} [MeasurableSpace Theta] (score : Theta → TrajectoryScore Z) (posterior : MeasureTheory.Measure Theta) [MeasureTheory.IsProbabilityMeasure posterior] (strategy : ℕ → TrajectoryPredictableTilt Z) {j n : ℕ} (hjn : j < n) (x : ℕ → Z) (hexposure : 0 < PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x) (hscore : ∀ (theta : Theta) (k : ℕ), observedTrajectoryScore (score theta) k x ∈ Set.Icc 0 1) (hordinary : MeasureTheory.Integrable (fun (theta : Theta) => (∑ k ∈ Finset.Ico j n, observedTrajectoryScore (score theta) k x) / ↑(n - j)) posterior) (hweighted : MeasureTheory.Integrable (fun (theta : Theta) => PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingWeightedObservationAt (fun (theta : Theta) => observedTrajectoryScore (score theta)) (observedTrajectoryPredictableStrategyCatalog strategy) theta j n x / PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x) posterior) : |continuousTrajectoryPosteriorEmpiricalPrequentialSuffixRisk score posterior j n x - continuousTrajectorySleepingPosteriorNormalizedEmpiricalRisk score strategy posterior j n x| ≤ continuousTrajectorySleepingPredictableTiltUniformDiscrepancy strategy j n x

Posterior-level empirical-risk deviation under the same realized weights.

noncomputable def FormalSLT.StochasticDynamics.continuousTrajectorySleepingPredictableTiltExcess {Theta : Type u_1} {Z : Type u_2} [MeasurableSpace Theta] (prior posterior : MeasureTheory.Measure Theta) (score : Theta → TrajectoryScore Z) (strategy : ℕ → TrajectoryPredictableTilt Z) (delta : ℝ) (j n : ℕ) (x : ℕ → Z) : ℝ

The complexity and observable predictor-variance term of the normalized sleeping predictable-tilt boundary, excluding empirical risk.

Equations

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

noncomputable def FormalSLT.StochasticDynamics.continuousTrajectorySleepingPredictableTiltOrdinarySuffixBoundary {Theta : Type u_1} {Z : Type u_2} [MeasurableSpace Theta] (prior posterior : MeasureTheory.Measure Theta) (score : Theta → TrajectoryScore Z) (strategy : ℕ → TrajectoryPredictableTilt Z) (delta : ℝ) (j n : ℕ) (x : ℕ → Z) : ℝ

Observable ordinary suffix-risk endpoint for a general nonnegative time-varying predictable tilt.

Equations

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

theorem FormalSLT.StochasticDynamics.continuousTrajectorySleepingPredictableTilt_ordinaryRisk_of_weighted {Theta : Type u_1} {Z : Type u_2} [MeasurableSpace Theta] [MeasurableSpace Z] (K : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) (score : Theta → TrajectoryScore Z) (posterior prior : MeasureTheory.Measure Theta) (strategy : ℕ → TrajectoryPredictableTilt Z) (delta : ℝ) (j n : ℕ) (x : ℕ → Z) (hweighted : continuousTrajectorySleepingPosteriorNormalizedConditionalRisk K score strategy posterior j n x < continuousTrajectorySleepingPredictableTiltBoundary prior posterior score strategy delta j n x) (hconditional : |continuousTrajectoryPosteriorAverageConditionalSuffixRisk K score posterior j n x - continuousTrajectorySleepingPosteriorNormalizedConditionalRisk K score strategy posterior j n x| ≤ continuousTrajectorySleepingPredictableTiltUniformDiscrepancy strategy j n x) (hempirical : |continuousTrajectoryPosteriorEmpiricalPrequentialSuffixRisk score posterior j n x - continuousTrajectorySleepingPosteriorNormalizedEmpiricalRisk score strategy posterior j n x| ≤ continuousTrajectorySleepingPredictableTiltUniformDiscrepancy strategy j n x) : continuousTrajectoryPosteriorAverageConditionalSuffixRisk K score posterior j n x < continuousTrajectorySleepingPredictableTiltOrdinarySuffixBoundary prior posterior score strategy delta j n x

Deterministic composition of a weighted PAC-Bayes inequality with the two total-variation comparisons.

Common-event ordinary-risk theorem

theorem FormalSLT.StochasticDynamics.exists_continuousTrajectorySleepingPredictableTiltPACBayes_ordinarySuffixRisk_event_of_parameterMeasurable {Theta : Type u_1} {Z : Type u_2} [MeasurableSpace Theta] [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (K : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (K n)] (x0 : Z) (score : Theta → TrajectoryScore Z) (hscore : ∀ (theta : Theta) (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score theta n u y ∈ Set.Icc 0 1) (hscore_parameter : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), MeasureTheory.StronglyMeasurable fun (theta : Theta) => score theta n u y) (strategy : ℕ → TrajectoryPredictableTilt Z) {L : ℝ} (hL1 : L < 1) (hstrategy_range : ∀ (j n : ℕ) (u : ↥(Finset.Iic n) → Z), strategy j n u ∈ Set.Icc 0 L) (prior : MeasureTheory.Measure Theta) [MeasureTheory.IsProbabilityMeasure prior] {delta : ℝ} (hdelta : 0 < delta) : ∃ (goodEvent : Set (ℕ → Z)), (trajectoryMeasure K x0).real goodEventᶜ ≤ delta ∧ ∀ x ∈ goodEvent, ∀ (posterior : MeasureTheory.Measure Theta), MeasureTheory.IsProbabilityMeasure posterior → posterior.AbsolutelyContinuous prior → MeasureTheory.Integrable (MeasureTheory.llr posterior prior) posterior → ∀ (j n : ℕ), j < n → 0 < PACBayes.ContinuousSleepingPredictableTiltPACBayes.continuousSleepingPredictableTiltExposure (observedTrajectoryPredictableStrategyCatalog strategy) j n x → continuousTrajectoryPosteriorAverageConditionalSuffixRisk K score posterior j n x < continuousTrajectorySleepingPredictableTiltOrdinarySuffixBoundary prior posterior score strategy delta j n x

One outer-mass event controls ordinary encountered conditional risk on every nonempty path-selected suffix, for every eligible path-selected posterior and every predeclared nonnegative predictable strategy atom.

The price for using nonuniform realized time weights is exactly twice the finite total-variation discrepancy. This theorem does not select a strategy outside the fixed catalog and is not a strategy-mixture or coin-betting result.

@[simp]

theorem FormalSLT.StochasticDynamics.continuousTrajectorySleepingPredictableTiltUniformDiscrepancy_countableConstant {Z : Type u_2} (eta : ℕ → ℝ) {j n : ℕ} (hjn : j < n) (heta : 0 < eta j) (x : ℕ → Z) : continuousTrajectorySleepingPredictableTiltUniformDiscrepancy (countableConstantTrajectoryTiltCatalog eta) j n x = 0

Constant positive post-wake tilts have exactly zero uniform-weight discrepancy.