2. Probability, kernels, filtrations, and concentration

Plain-English statement. A policy is an action-valued function of a state together with proof that this function is measurable.

Intuition

An algorithmic formula is not enough for a probability theorem: the selected action must be a legitimate random variable.

Why it is needed

Generated trajectories, conditional distributions, filtrations, and expected regret all depend on policy measurability.

Place in the proof

This structure is the interface from deterministic state computation to probability-kernel construction.

Proof idea

The structure stores the action function and its measurability proof. Composition lemmas then obtain measurable actions from measurable states.

Lean reading notes

Measurable spaces are typeclass arguments. The structure makes the regularity contract explicit instead of relying on an informal claim that the policy is well behaved.

Teaching dependencies

No direct teaching dependency recorded.

structure MeasurablePolicy (State : Type u) (Action : Type v) [MeasurableSpace State] [MeasurableSpace Action] where

Plain-English statement. A geometric budget over all times can be shared equally across every member of one nonempty finite index type while preserving the total outer confidence budget.

Intuition

Use a finite union bound across arms or contexts at each time, then a summable geometric schedule across all times.

Why it is needed

ETC and UCB confidence arguments repeatedly need simultaneous control over a finite family and more than one horizon; this theorem packages only that reusable bookkeeping step.

Place in the proof

It joins the finite outer-union wrapper to the geometric confidence schedule in Chapter 2, before any algorithm-specific tail producer.

Proof idea

Apply countable outer-measure subadditivity over time, invoke the compiled equal-share finite-union theorem at each time, compare the ENNReal series termwise, and rewrite the exact geometric total.

Lean reading notes

The exact statement assumes only a measurable ambient space, a nonempty Fintype index, nonnegative delta, and the pointwise outer-measure bounds. It does not require event measurability, a probability measure, independence, filtration, or a concentration producer.

Teaching dependencies

BanditRLProof.ProbabilityUnionBound.measure_biUnion_finset_le_of_uniform, BanditRLProof.Concentration.tsum_ofReal_geometricConfidenceShare

theorem measure_iUnion_iUnion_fintype_le_delta_of_geometricConfidenceShare {Omega : Type u} {Idx : Type v} [MeasurableSpace Omega] [Fintype Idx] [Nonempty Idx] (mu : Measure Omega) (bad : Nat -> Idx -> Set Omega) (delta : Real) (hdelta : 0 <= delta) (hbad : forall n i, mu (bad n i) <= ENNReal.ofReal (geometricConfidenceShare delta n / (Fintype.card Idx : Real))) : mu (⋃ n, ⋃ i, bad n i) <= ENNReal.ofReal delta

Plain-English statement. One canonical generated action/reward trajectory satisfies the existing random-pull-count empirical-mean confidence radius simultaneously for every finite arm and every positive successor horizon, outside one geometrically budgeted failure event.

Intuition

The fixed-arm tail already adapts to the random number of pulls inside a fixed horizon. This theorem keeps the generated law fixed, shares each time budget across all arms, and then sums the geometric schedule over all horizons.

Why it is needed

It closes the gap between generic confidence-budget bookkeeping and a real finite-arm trajectory-level empirical-mean event needed by UCB-facing work.

Place in the proof

It sits above the canonical random-pull-count tail and finite-index geometric union, and below any UCB score-selection or regret consumer.

Proof idea

At each pair (n, arm), instantiate the compiled canonical tail at horizon n+1 and confidence share delta_n divided by the arm count; then apply the accepted finite-index geometric all-time union to the identical trajectory measure.

Lean reading notes

The theorem requires a probability initial pair law, measurable generated context/state, a centered reward-kernel law, a global selected-history variance ceiling, stationary per-arm means, and positive sigma2 and delta. It assumes neither event measurability nor delta at most one, and it proves no maximal inequality or UCB regret bound.

Teaching dependencies

BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_abs_tail_random_pullCount_ennreal_delta_trajMeasure_on_horizon, BanditRLProof.Concentration.measure_iUnion_iUnion_fintype_le_delta_of_geometricConfidenceShare

theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_geometricAllTime_abs_tail_ennreal_delta_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Fintype Action] [Nonempty Action] [DecidableEq Action] (mu0 : Measure (Prod Action Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (armMean : Action -> Rat) (sigma2 : NNReal) (hvariance : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Action, mean (context i history) arm = armMean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context

Plain-English statement. One canonical generated action/reward trajectory satisfies the random-pull-count empirical-mean confidence radius for every finite arm and every positive successor horizon under a telescoping confidence schedule.

Intuition

The shares telescope exactly to delta while their reciprocal grows only polynomially, so logarithmic radii retain logarithmic time growth instead of the linear growth caused by geometric shares.

Why it is needed

This supplies the confidence schedule now consumed by the fixed-policy ordinary-UCB route on the canonical Rat trajectory.

Place in the proof

It sits above the fixed-horizon random-count tail and directly below the compiled same-source scheduled UCB score, policy, all-horizon count, and finite-time expected-regret consumers.

Proof idea

Prove the reciprocal telescope, convert its exact Real HasSum to ENNReal, share each time budget across the finite arm type, instantiate the accepted fixed-horizon tail at n+1, and apply countable outer-measure subadditivity without changing trajMeasure.

Lean reading notes

The theorem retains the same probability, measurability, centered-kernel, stationary-mean, variance-ceiling, and positivity contracts as the geometric producer. It adds no independence, event-measurability, optional-stopping, or delta-at-most-one premise.

Teaching dependencies

BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_abs_tail_random_pullCount_ennreal_delta_trajMeasure_on_horizon, BanditRLProof.Concentration.measure_iUnion_iUnion_fintype_le_delta_of_telescopingConfidenceShare

theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_telescopingAllTime_abs_tail_ennreal_delta_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Fintype Action] [Nonempty Action] [DecidableEq Action] (mu0 : Measure (Prod Action Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (armMean : Action -> Rat) (sigma2 : NNReal) (hvariance : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Action, mean (context i history) arm = armMean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context

Plain-English statement. If the joint law of environment and history is the canonical prior-likelihood law, the canonical posterior kernel agrees almost everywhere with the conditional distribution of the environment given history.

Intuition

Bayes' posterior and measure-theoretic conditional distribution are two descriptions of the same object once their joint law is identified.

Why it is needed

Thompson sampling needs to replace a reference posterior sampler by the actual conditional environment law along a generated history.

Place in the proof

This theorem is the principal posterior-law transport in the Thompson proof DAG.

Proof idea

Rewrite the supplied pair pushforward as the canonical joint measure and use Mathlib's posterior/conditional-distribution identity, transporting the almost-everywhere statement along the history marginal.

Lean reading notes

The conclusion is kernel equality almost everywhere, not pointwise equality. Standard Borel and finiteness hypotheses make conditional distributions available.

Teaching dependencies

No direct teaching dependency recorded.

theorem canonicalPosterior_kernel_ae_eq_condDistrib_of_pair_map_eq {Omega : Type*} [MeasurableSpace Omega] [StandardBorelSpace Env] [Nonempty Env] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (hhistory : Measurable history) (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (hpair : mu.map (fun omega => (env omega, history omega)) = canonicalJointMeasure prior likelihood) : (canonicalPosterior prior likelihood).kernel =ᵐ[mu.map history] ProbabilityTheory.condDistrib env history mu

Plain-English statement. The partial sums of an adapted integrable successor-indexed martingale-difference sequence form a martingale.

Intuition

Zero conditional drift is exactly the local condition needed for cumulative noise to have no predictable trend.

Why it is needed

Concentration and optional-stopping arguments reason about cumulative centered reward, not isolated one-step rewards.

Place in the proof

This theorem converts conditional reward-law work into Mathlib's martingale API.

Proof idea

Use the witness fields for strong adaptedness, integrability, and zero conditional expectation; unfold the successor partial sum and verify the martingale conditional-expectation equation.

Lean reading notes

The packaged witness prevents measurability and integrability assumptions from disappearing inside a tactic proof.

Teaching dependencies

No direct teaching dependency recorded.

theorem martingale_partialSumsSucc_of_succMartingaleDifference {Omega : Type u} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} (h : SuccMartingaleDifference mu F Y) : Martingale (partialSumsSucc Y) F mu

Plain-English statement. On the canonical trajectory generated by a measurable history step-kernel family, the selected centered successor reward has the promised conditional sub-Gaussian MGF.

Intuition

The theorem closes the gap between a one-step kernel law and the random reward actually observed on the recursively generated path.

Why it is needed

UCB, ETC, and adversarial high-probability routes need conditional concentration on the same measure that generates the policy history.

Place in the proof

It is a reusable law-transport endpoint in the conditional-reward layer.

Proof idea

Identify the conditional kernel of the successor reward under trajMeasure, center the selected law by its declared mean, and reuse the kernel-level conditional-MGF contract.

Lean reading notes

The long name records the transport path. The exact Lean statement below is the authoritative list of measurable-space, kernel, mean, and proxy hypotheses.

Teaching dependencies

BanditRLProof.Policy.MeasurablePolicy

theorem historyStepKernelFamily_centeredReward_succ_hasCondSubgaussianMGF_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu0 : Measure Rat) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (defaultAction : Action) (i : Nat) (c : NNReal) (hvariance : forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= c) : let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Plain-English statement. A countable family of deviation events, each controlled by its own fixed-MGF quadratic tail and confidence share, has total outer probability at most the supplied overall budget.

Intuition

Spend a small part of the confidence budget at each index, prove the corresponding one-event tail, and add the possible failures. Countable subadditivity is enough; the events need not form a martingale stopping argument.

Why it is needed

Many all-time algorithm statements need one event covering every deterministic prefix. This theorem turns a reusable fixed-index MGF bound into such a scheduled union without overstating it as Ville, Doob, mixture, optional-stopping, or general Freedman theory.

Place in the proof

It is the generic probability bridge consumed by the new all-positive-prefix EXP3 predictable-variance theorem.

Proof idea

Apply the measure-of-countable-union upper bound, instantiate the optimized one-event quadratic fixed-MGF theorem at every index, compare termwise ENNReal bounds, and finish with the caller's total confidence-budget inequality.

Lean reading notes

The conclusion is an outer-measure inequality, so event measurability is not assumed. Positivity of every scale, variance budget, tilt cap, and confidence share is explicit in the signature.

Teaching dependencies

BanditRLProof.Concentration.measure_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tail

theorem measure_iUnion_scheduled_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tail {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) (deviation predictableVariance : Nat -> Omega -> Real) (varianceScale varianceBudget tiltCap deltaAt : Nat -> Real) (delta : Real) (hvarianceScale : forall n, 0 < varianceScale n) (hvarianceBudget : forall n, 0 < varianceBudget n) (htiltCap : forall n, 0 < tiltCap n) (hdeltaAt : forall n, 0 < deltaAt n) (hfixed : forall n tilt, 0 <= tilt -> tilt <= tiltCap n -> mu {omega | quadraticFixedMGFScheduledRadius varianceScale varianceBudget tiltCap deltaAt n <= deviation n omega ∧ predictableVariance n omega <= varianceBudget n} <= ENNReal.ofReal (Real.exp (-tilt * quadraticFixedMGFScheduledRadius varianceScale varianceBudget tiltCap deltaAt n + varianceScale n * (tilt ^ 2 * varianceBudget n)))) (hbudget : (∑' n, ENNReal.ofReal (deltaAt n)) <= ENNReal.ofReal delta) : mu (⋃ n, {omega | quadraticFixedMGFScheduledRadius varianceScale varianceBudget tiltCap deltaAt n <= deviation n omega ∧ predictableVariance n omega <= varianceBudget n}) <= ENNReal.ofReal delta