BanditRLProof.ConditionalRewardPartialTrajectoryMaskedLaw

On the canonical action/reward trajectory, every sampled successor action is almost surely the action selected by the policy from the frozen pair prefix. This is an ambient trajectory statement, not merely an a.e. statement inside the regular conditional kernel.

theorem actionRewardHistoryStepKernelFamily_action_succ_ae_eq_policy_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} {Reward : Type*} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [MeasurableSingletonClass Action] [Countable Action] (mu0 : Measure (Prod Action Reward)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let mu := ProbabilityTheory.Kernel.trajMeasure (X

Canonical action/reward `trajMeasure` two-sided tail for one policy-selected arm under a random cumulative predictable-variance budget. The mask uses the action selected from the observed reward history, so it is measurable at filtration level `i`. Identifying this mask with the sampled next-action coordinate is intentionally left to a separate transport theorem.

theorem actionRewardHistoryStepKernelFamily_policyArmMaskedCenteredRewardSuccProcess_sum_abs_tail_predictableVariance_ennreal_delta_trajMeasure_on_horizon {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable Action] [Nonempty 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)) (arm : Action) (sigma2 : NNReal) (n : Nat) (hvariance : forall i : Nat, i < n - 1 -> forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context

Canonical sampled-arm masked centered-reward tail with the random predictable proxy written as `sigma2` times the actual successor pull count. The proof transports the history-policy mask through the canonical ambient a.e. successor-action law. It remains a fixed-horizon joint event, before exact-count peeling or empirical-mean normalization.

theorem actionRewardHistoryStepKernelFamily_sampledArmMaskedCenteredRewardSuccProcess_sum_abs_tail_successorPullCount_ennreal_delta_trajMeasure_on_horizon {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable 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)) (arm : Action) (sigma2 : NNReal) (n : Nat) (hvariance : forall i : Nat, i < n - 1 -> forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context

Canonical fixed-arm empirical-mean confidence on one exact positive successor pull-count fiber. The canonical sampled-arm tail is instantiated with budget `sigma2 * k`, and the centered sum is divided by the positive count `k`.

theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_abs_tail_exact_pullCount_ennreal_delta_trajMeasure_on_horizon {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable 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)) (arm : Action) (armMean : Rat) (sigma2 : NNReal) (n k : Nat) (hvariance : forall i : Nat, i < n - 1 -> 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), mean (context i history) arm = armMean) (hk : 0 < k) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context

Canonical positive random-pull-count empirical-mean confidence obtained by peeling the exact-count theorem over the at most `n` successor count fibers. This is fixed-horizon confidence, not an anytime confidence sequence.

theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_abs_tail_random_pullCount_ennreal_delta_trajMeasure_on_horizon {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable 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)) (arm : Action) (armMean : Rat) (sigma2 : NNReal) (n : Nat) (hvariance : forall i : Nat, i < n - 1 -> 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), mean (context i history) arm = armMean) (hn : 0 < n) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context

Canonical positive random-pull-count empirical-mean confidence obtained by peeling the exact-count theorem over the at most `n` successor count fibers. This is fixed-horizon confidence, not an anytime confidence sequence. -/ theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_abs_tail_random_pullCount_ennreal_delta_trajMeasure_on_horizon {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable 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)) (arm : Action) (armMean : Rat) (sigma2 : NNReal) (n : Nat) (hvariance : forall i : Nat, i < n - 1 -> 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), mean (context i history) arm = armMean) (hn : 0 < n) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context := fun i history => context i (History.pairHistoryRewardProjection history) let pairState : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> State := fun i history => state i (History.pairHistoryRewardProjection history) let hpairContext : forall i : Nat, Measurable (pairContext i) := fun i => (hcontext i).comp (History.measurable_pairHistoryRewardProjection (Action := Action) (Reward := Rat) i) let hpairState : forall i : Nat, Measurable (pairState i) := fun i => (hstate i).comp (History.measurable_pairHistoryRewardProjection (Action := Action) (Reward := Rat) i) let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState let mu := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Prod Action Rat) mu0 stepKernel let action : (Nat -> Prod Action Rat) -> ActionTrace Action := fun trajectory t => (trajectory t).1 let reward : (Nat -> Prod Action Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let count : (Nat -> Prod Action Rat) -> Nat := fun trajectory => successorArmPullCount (action trajectory) arm n mu {trajectory | 0 < count trajectory ∧ successorArmEmpiricalMeanPeelingRadius sigma2 (count trajectory) n delta <= |successorArmEmpiricalMean (action trajectory) (reward trajectory) arm n - (armMean : Real)|} <= ENNReal.ofReal delta := by let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context := fun i history => context i (History.pairHistoryRewardProjection history) let pairState : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> State := fun i history => state i (History.pairHistoryRewardProjection history) let hpairContext : forall i : Nat, Measurable (pairContext i) := fun i => (hcontext i).comp (History.measurable_pairHistoryRewardProjection (Action := Action) (Reward := Rat) i) let hpairState : forall i : Nat, Measurable (pairState i) := fun i => (hstate i).comp (History.measurable_pairHistoryRewardProjection (Action := Action) (Reward := Rat) i) let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState let mu := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Prod Action Rat) mu0 stepKernel let action : (Nat -> Prod Action Rat) -> ActionTrace Action := fun trajectory t => (trajectory t).1 let reward : (Nat -> Prod Action Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let count : (Nat -> Prod Action Rat) -> Nat := fun trajectory => successorArmPullCount (action trajectory) arm n let bad : Nat -> Set (Nat -> Prod Action Rat) := fun k => {trajectory | successorArmEmpiricalMeanPeelingRadius sigma2 k n delta <= |successorArmEmpiricalMean (action trajectory) (reward trajectory) arm n - (armMean : Real)|} have hnReal : 0 < (n : Real) := Nat.cast_pos.mpr hn have hdeltaShare : 0 < delta / (n : Real) := div_pos hdelta hnReal have hcount_le : forall trajectory, count trajectory <= n := by intro trajectory exact successorArmPullCount_le_horizon (action trajectory) arm n have hfiber : forall k, 0 < k -> k <= n -> mu {trajectory | count trajectory = k ∧ trajectory ∈ bad k} <= ENNReal.ofReal (delta / (n : Real)) := by intro k hk _hk_le simpa [pairContext, pairState, hpairContext, hpairState, stepKernel, mu, action, reward, count, bad, successorArmEmpiricalMeanPeelingRadius] using (actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_abs_tail_exact_pullCount_ennreal_delta_trajMeasure_on_horizon (mu0 := mu0) (rewardKernel := rewardKernel) (policy := policy) (context := context) (state := state) (hcontext := hcontext) (hstate := hstate) (mean := mean) (varianceProxy := varianceProxy) (law := law) (hmean := hmean) (arm := arm) (armMean := armMean) (sigma2 := sigma2) (n := n) (k := k) (hvariance := hvariance) (harmMean := harmMean) hk hsigma2 (delta / (n : Real)) hdeltaShare) simpa [pairContext, pairState, hpairContext, hpairState, stepKernel, mu, action, reward, count, bad] using (Concentration.measure_positive_randomCount_event_le_of_exactCount_uniform mu count n bad hcount_le hn delta hdelta hfiber) /- Finite-arm, finite-time empirical-mean confidence on the canonical action/reward trajectory. The variance premise is needed only through the largest predecessor index used before time `T`; this is a fixed finite union, not an anytime confidence sequence.

theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_finiteArmTime_abs_tail_ennreal_delta_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable 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)) (arms : Finset Action) (harms : arms.Nonempty) (armMean : Action -> Rat) (sigma2 : NNReal) (T : Nat) (hvariance : forall i : Nat, i < T - 1 -> 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, arm ∈ arms -> mean (context i history) arm = armMean arm) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context