Continuous-model PAC-Bayes for finite strategies and countable wakes #
This module builds a genuine two-axis process master. For every model
parameter theta, it mixes a finite predeclared strategy catalog and the
countable polynomial sleeping-wake prior:
M(theta,n) = tail(n) + sum_{w<n} p(w) sum_a q(a) exp(S(theta,a,w,n)).
The construction reuses finiteStrategySleepingProcessMixture, so each
finite-time value is a finite sum plus a closed-form tail despite the
countable wake axis. A second mixture integrates M(theta,n) against an
arbitrary measurable model prior.
Under the explicit Fubini obligations below, Ville gives one crossing event
for that continuous prior mixture.
Outside the event, nested change of measure gives, simultaneously for every eligible continuous model posterior, finite strategy posterior, active wake, and time,
`E_rho E_sigma S < KL(rho || pi) + KL(sigma || q)
- log p(w) + log(1 / delta)`.
The posterior is factorized: a continuous posterior over models and a finite posterior over strategies. The strategy catalog and wake prior are fixed before observation, while both reporting posteriors and the wake may be selected after observing the path. This is a master-mixture result, not coin betting or parameter-free inference, and it makes no claim about correlated model--strategy posteriors or ordinary risk without a separate score-to-risk bridge.
noncomputable def
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.parameterizedTwoAxisSleepingMaster
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
(strategyPrior : A → ℝ)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
:
The exact finite-strategy, countable-wake master for one model parameter.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.continuousTwoAxisSleepingMaster
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[MeasurableSpace Theta]
(modelPrior : MeasureTheory.Measure Theta)
(strategyPrior : A → ℝ)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
:
The continuous model-prior mixture of the exact two-axis masters.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.finiteStrategyPriorMoment
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
(strategyPrior : A → ℝ)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
(theta : Theta)
(w n : ℕ)
(omega : Omega)
:
The prior exponential moment of the finite strategy catalog at one wake.
Equations
- FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.finiteStrategyPriorMoment strategyPrior score theta w n omega = ∑ a : A, strategyPrior a * Real.exp (score theta a w n omega)
Instances For
def
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.finiteStrategyPosteriorScore
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
(strategyPosterior : A → ℝ)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
(theta : Theta)
(w n : ℕ)
(omega : Omega)
:
The soft strategy-posterior average of the selected-wake score.
Equations
- FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.finiteStrategyPosteriorScore strategyPosterior score theta w n omega = ∑ a : A, strategyPosterior a * score theta a w n omega
Instances For
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.parameterizedTwoAxisSleepingMaster_eq
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsPMF strategyPrior)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
(theta : Theta)
(n : ℕ)
(omega : Omega)
:
parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega = AnytimeValid.polynomialSleepingTail n + ∑ w ∈ Finset.range n,
AnytimeValid.AllocationLogLog.polynomialEpochWeight w * finiteStrategyPriorMoment strategyPrior score theta w n omega
Expanded finite-time formula for the parameterized master. The closed form tail is shared across strategies because the strategy prior sums to one.
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.parameterizedTwoAxisSleepingMaster_eProcess
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[DecidableEq A]
{mOmega : MeasurableSpace Omega}
{theta : Theta}
{mu : MeasureTheory.Measure Omega}
[MeasureTheory.IsFiniteMeasure mu]
{F : MeasureTheory.Filtration ℕ mOmega}
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsFullSupportPMF strategyPrior)
{score : Theta → A → ℕ → ℕ → Omega → ℝ}
(hscore :
∀ (a : A) (w : ℕ), AnytimeValid.EProcess mu F fun (n : ℕ) (omega : Omega) => Real.exp (score theta a w n omega))
(hsleep : ∀ (a : A) (w n : ℕ) (omega : Omega), n ≤ w → score theta a w n omega = 0)
:
AnytimeValid.EProcess mu F (parameterizedTwoAxisSleepingMaster strategyPrior score theta)
The generic finite-strategy/countable-wake closure gives one e-process for each fixed model parameter. The atom scores must be zero while sleeping so their exponentials remain exactly one.
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.parameterizedTwoAxisSleepingMaster_nonneg
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsPMF strategyPrior)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
:
The two-axis master is pointwise nonnegative without any stochastic assumption on the score.
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.parameterizedTwoAxisSleepingMaster_pos
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[Nonempty A]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsFullSupportPMF strategyPrior)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
(theta : Theta)
(n : ℕ)
(omega : Omega)
:
A full-support strategy prior makes every parameterized master strictly positive; the unused sleeping-wake tail already has positive mass.
@[simp]
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.parameterizedTwoAxisSleepingMaster_zero
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsPMF strategyPrior)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
(theta : Theta)
(omega : Omega)
:
Every parameterized master starts at one.
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.finiteStrategyPriorMoment_mul_wakeWeight_le_master
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsPMF strategyPrior)
{score : Theta → A → ℕ → ℕ → Omega → ℝ}
{w n : ℕ}
(hwn : w < n)
(theta : Theta)
(omega : Omega)
:
AnytimeValid.AllocationLogLog.polynomialEpochWeight w * finiteStrategyPriorMoment strategyPrior score theta w n omega ≤ parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega
The selected wake's soft finite-strategy prior moment is dominated by the single two-axis master after multiplication by its polynomial wake weight.
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.finiteStrategyPriorMoment_pos
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[Nonempty A]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsFullSupportPMF strategyPrior)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
(theta : Theta)
(w n : ℕ)
(omega : Omega)
:
The selected-wake finite strategy moment is strictly positive.
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.finiteStrategyPosteriorScore_le_logMaster
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[Nonempty A]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsFullSupportPMF strategyPrior)
{strategyPosterior : A → ℝ}
(hstrategyPosterior : PACBayesKL.IsPMF strategyPosterior)
{score : Theta → A → ℕ → ℕ → Omega → ℝ}
{w n : ℕ}
(hwn : w < n)
(theta : Theta)
(omega : Omega)
:
finiteStrategyPosteriorScore strategyPosterior score theta w n omega ≤ PACBayesKL.klDiv strategyPosterior strategyPrior + Real.log (parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega) - Real.log (AnytimeValid.AllocationLogLog.polynomialEpochWeight w)
A selected active wake and soft finite strategy posterior pay finite strategy KL plus the exact wake log-prior cost against the one master.
def
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.continuousTwoAxisSleepingExceptionalEvent
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[MeasurableSpace Theta]
(modelPrior : MeasureTheory.Measure Theta)
(strategyPrior : A → ℝ)
(score : Theta → A → ℕ → ℕ → Omega → ℝ)
(delta : ℝ)
:
Set Omega
The crossing event of the single continuous-prior two-axis master.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.continuousTwoAxisSleepingExceptionalEvent_mass_le_delta
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[MeasurableSpace Theta]
{mOmega : MeasurableSpace Omega}
{mu : MeasureTheory.Measure Omega}
[MeasureTheory.IsProbabilityMeasure mu]
{F : MeasureTheory.Filtration ℕ mOmega}
(modelPrior : MeasureTheory.Measure Theta)
[MeasureTheory.IsProbabilityMeasure modelPrior]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsFullSupportPMF strategyPrior)
{score : Theta → A → ℕ → ℕ → Omega → ℝ}
{delta : ℝ}
(hdelta : 0 < delta)
(h_adapted_mix : MeasureTheory.StronglyAdapted F (continuousTwoAxisSleepingMaster modelPrior strategyPrior score))
(h_integrable_mix :
∀ (n : ℕ), MeasureTheory.Integrable (continuousTwoAxisSleepingMaster modelPrior strategyPrior score n) mu)
(hM_int_next :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (p : Theta × Omega) => parameterizedTwoAxisSleepingMaster strategyPrior score p.1 (n + 1) p.2)
(modelPrior.prod mu))
(hM_int_next_restrict :
∀ (n : ℕ) {s : Set Omega},
MeasurableSet s →
mu s < ⊤ →
MeasureTheory.Integrable
(fun (p : Omega × Theta) => parameterizedTwoAxisSleepingMaster strategyPrior score p.2 (n + 1) p.1)
((mu.restrict s).prod modelPrior))
(hM_int_current :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (p : Omega × Theta) => parameterizedTwoAxisSleepingMaster strategyPrior score p.2 n p.1)
(mu.prod modelPrior))
(hM_int_current_restrict :
∀ (n : ℕ) {s : Set Omega},
MeasurableSet s →
mu s < ⊤ →
MeasureTheory.Integrable
(fun (p : Omega × Theta) => parameterizedTwoAxisSleepingMaster strategyPrior score p.2 n p.1)
((mu.restrict s).prod modelPrior))
(hfixed :
∀ᵐ (theta : Theta) ∂modelPrior, AnytimeValid.EProcess mu F (parameterizedTwoAxisSleepingMaster strategyPrior score theta))
:
Under the explicit continuous-mixture Fubini obligations, the continuous
model-prior integral of the finite-strategy/countable-wake masters has one
Ville crossing event of mass at most delta.
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.continuousTwoAxisSleeping_allPosteriorsLogMaster_of_not_mem
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[Nonempty A]
[MeasurableSpace Theta]
(modelPrior : MeasureTheory.Measure Theta)
[MeasureTheory.IsProbabilityMeasure modelPrior]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsFullSupportPMF strategyPrior)
{score : Theta → A → ℕ → ℕ → Omega → ℝ}
{delta : ℝ}
(hdelta : 0 < delta)
(hprior_integrable :
∀ (n : ℕ) (omega : Omega),
MeasureTheory.Integrable
(fun (theta : Theta) => parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega) modelPrior)
{omega : Omega}
(homega : omega ∉ continuousTwoAxisSleepingExceptionalEvent modelPrior strategyPrior score delta)
(modelPosterior : MeasureTheory.Measure Theta)
:
MeasureTheory.IsProbabilityMeasure modelPosterior →
modelPosterior.AbsolutelyContinuous modelPrior →
MeasureTheory.Integrable (MeasureTheory.llr modelPosterior modelPrior) modelPosterior →
∀ (n : ℕ),
0 < n →
MeasureTheory.Integrable
(fun (theta : Theta) => Real.log (parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega))
modelPosterior →
∫ (theta : Theta), Real.log (parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega) ∂modelPosterior < (InformationTheory.klDiv modelPosterior modelPrior).toReal + Real.log (1 / delta)
Outside the one master crossing event, continuous Donsker--Varadhan controls the posterior mean log master for every eligible model posterior.
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.continuousTwoAxisSleeping_selectedWakeSoftPosteriorScore_of_not_mem
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[Nonempty A]
[MeasurableSpace Theta]
(modelPrior : MeasureTheory.Measure Theta)
[MeasureTheory.IsProbabilityMeasure modelPrior]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsFullSupportPMF strategyPrior)
{score : Theta → A → ℕ → ℕ → Omega → ℝ}
{delta : ℝ}
(hdelta : 0 < delta)
(hprior_integrable :
∀ (n : ℕ) (omega : Omega),
MeasureTheory.Integrable
(fun (theta : Theta) => parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega) modelPrior)
{omega : Omega}
(homega : omega ∉ continuousTwoAxisSleepingExceptionalEvent modelPrior strategyPrior score delta)
(modelPosterior : MeasureTheory.Measure Theta)
(hmodelPosterior : MeasureTheory.IsProbabilityMeasure modelPosterior)
(hposterior_prior : modelPosterior.AbsolutelyContinuous modelPrior)
(hllr : MeasureTheory.Integrable (MeasureTheory.llr modelPosterior modelPrior) modelPosterior)
{strategyPosterior : A → ℝ}
(hstrategyPosterior : PACBayesKL.IsPMF strategyPosterior)
{w n : ℕ}
(hwn : w < n)
(hlog_integrable :
MeasureTheory.Integrable
(fun (theta : Theta) => Real.log (parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega))
modelPosterior)
(hscore_integrable :
MeasureTheory.Integrable (fun (theta : Theta) => finiteStrategyPosteriorScore strategyPosterior score theta w n omega)
modelPosterior)
:
∫ (theta : Theta), finiteStrategyPosteriorScore strategyPosterior score theta w n omega ∂modelPosterior < (InformationTheory.klDiv modelPosterior modelPrior).toReal + PACBayesKL.klDiv strategyPosterior strategyPrior - Real.log (AnytimeValid.AllocationLogLog.polynomialEpochWeight w) + Real.log (1 / delta)
Nested finite and continuous change of measure. An active wake and a soft strategy posterior may be selected after observing the path. Model and strategy selection are charged separately, and the wake pays the exact polynomial-prior log cost.
theorem
FormalSLT.PACBayes.ContinuousFiniteStrategySleepingPACBayes.exists_continuousTwoAxisSleepingPACBayes_factorized_event
{A : Type u_1}
{Theta : Type u_2}
{Omega : Type u_3}
[Fintype A]
[Nonempty A]
[MeasurableSpace Theta]
{mOmega : MeasurableSpace Omega}
{mu : MeasureTheory.Measure Omega}
[MeasureTheory.IsProbabilityMeasure mu]
{F : MeasureTheory.Filtration ℕ mOmega}
(modelPrior : MeasureTheory.Measure Theta)
[MeasureTheory.IsProbabilityMeasure modelPrior]
{strategyPrior : A → ℝ}
(hstrategyPrior : PACBayesKL.IsFullSupportPMF strategyPrior)
{score : Theta → A → ℕ → ℕ → Omega → ℝ}
{delta : ℝ}
(hdelta : 0 < delta)
(h_adapted_mix : MeasureTheory.StronglyAdapted F (continuousTwoAxisSleepingMaster modelPrior strategyPrior score))
(h_integrable_mix :
∀ (n : ℕ), MeasureTheory.Integrable (continuousTwoAxisSleepingMaster modelPrior strategyPrior score n) mu)
(hM_int_next :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (p : Theta × Omega) => parameterizedTwoAxisSleepingMaster strategyPrior score p.1 (n + 1) p.2)
(modelPrior.prod mu))
(hM_int_next_restrict :
∀ (n : ℕ) {s : Set Omega},
MeasurableSet s →
mu s < ⊤ →
MeasureTheory.Integrable
(fun (p : Omega × Theta) => parameterizedTwoAxisSleepingMaster strategyPrior score p.2 (n + 1) p.1)
((mu.restrict s).prod modelPrior))
(hM_int_current :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (p : Omega × Theta) => parameterizedTwoAxisSleepingMaster strategyPrior score p.2 n p.1)
(mu.prod modelPrior))
(hM_int_current_restrict :
∀ (n : ℕ) {s : Set Omega},
MeasurableSet s →
mu s < ⊤ →
MeasureTheory.Integrable
(fun (p : Omega × Theta) => parameterizedTwoAxisSleepingMaster strategyPrior score p.2 n p.1)
((mu.restrict s).prod modelPrior))
(hfixed :
∀ᵐ (theta : Theta) ∂modelPrior, AnytimeValid.EProcess mu F (parameterizedTwoAxisSleepingMaster strategyPrior score theta))
(hprior_integrable :
∀ (n : ℕ) (omega : Omega),
MeasureTheory.Integrable
(fun (theta : Theta) => parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega) modelPrior)
:
∃ (goodEvent : Set Omega),
mu.real goodEventᶜ ≤ delta ∧ ∀ omega ∈ goodEvent,
∀ (modelPosterior : MeasureTheory.Measure Theta),
MeasureTheory.IsProbabilityMeasure modelPosterior →
modelPosterior.AbsolutelyContinuous modelPrior →
MeasureTheory.Integrable (MeasureTheory.llr modelPosterior modelPrior) modelPosterior →
∀ (strategyPosterior : A → ℝ),
PACBayesKL.IsPMF strategyPosterior →
∀ (w n : ℕ),
w < n →
MeasureTheory.Integrable
(fun (theta : Theta) =>
Real.log (parameterizedTwoAxisSleepingMaster strategyPrior score theta n omega))
modelPosterior →
MeasureTheory.Integrable
(fun (theta : Theta) =>
finiteStrategyPosteriorScore strategyPosterior score theta w n omega)
modelPosterior →
∫ (theta : Theta), finiteStrategyPosteriorScore strategyPosterior score theta w n omega ∂modelPosterior < (InformationTheory.klDiv modelPosterior modelPrior).toReal + PACBayesKL.klDiv strategyPosterior strategyPrior - Real.log (AnytimeValid.AllocationLogLog.polynomialEpochWeight w) + Real.log (1 / delta)
One event simultaneously supports path-selected continuous model posteriors, soft finite strategy posteriors, active wakes, and report times. All model-measure and integrability eligibility conditions remain explicit.