BanditRLProof.Algorithms.ETCBoundedRewardInfinitePiSource

Under an infinite product reward-coordinate law, the centered reward at time `i + 1` is independent of the reward-only past sigma-algebra generated by coordinates `j <= i`. This is the concrete product-law specialization of `indep_centeredReward_succ_pastReward_iSup_of_iIndepFun_reward`. It does not add the deterministic action generators from `History.historyFiltrationSucc`; use `indep_centeredReward_succ_historyFiltrationSucc_infinitePi` for that.

theorem indep_centeredReward_succ_pastReward_iSup_infinitePi {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (model : FiniteBanditModel K) (b : Fin K) (i : Nat) : ProbabilityTheory.Indep (MeasurableSpace.comap (fun omega : RewardTrace Rat => (((omega (i + 1) - model.mean b : Rat) : Real))) inferInstance) (iSup fun j : Nat => iSup fun _h : j <= i => MeasurableSpace.comap (fun omega : RewardTrace Rat => omega j) inferInstance) (MeasureTheory.Measure.infinitePi coordLaw)

Under an infinite product reward-coordinate law, the centered reward at time `i + 1` is independent of the full fixed-commit shifted history filtration. This specializes the deterministic action-history inclusion and reward-coordinate `iIndepFun` bridge to `Measure.infinitePi`.

theorem indep_centeredReward_succ_historyFiltrationSucc_infinitePi {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (b : Fin K) (i : Nat) : ProbabilityTheory.Indep (MeasurableSpace.comap (fun omega : RewardTrace Rat => (((omega (i + 1) - model.mean b : Rat) : Real))) inferInstance) (History.historyFiltrationSucc (fun _omega : RewardTrace Rat => ETC.actionWithCommit spec commitArm) (fun omega : RewardTrace Rat => omega) (fun _t : Nat => measurable_const) (fun t : Nat => measurable_pi_apply t) i) (MeasureTheory.Measure.infinitePi coordLaw)

The infinite product law over reward coordinates satisfies the action-matched bounded reward source contract when each coordinate law has the corresponding a.s. bound and mean for the arm pulled by the fixed-commit ETC trace.

theorem boundedRewardTraceSource_infinitePi_actionWithCommit {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (lo hi : Fin K -> Nat -> Real) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun r : Rat => Set.Icc (lo (ETC.actionWithCommit spec commitArm t) t) (hi (ETC.actionWithCommit spec commitArm t) t) (((r : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun r : Rat => (((r : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec commitArm t) : Rat) : Real))) : ETC.BoundedRewardTraceSource (MeasureTheory.Measure.infinitePi coordLaw) spec model commitArm (fun omega : RewardTrace Rat => omega) lo hi where

Under an infinite product reward-coordinate law, construct the reward-level conditional sub-Gaussian witness package for the fixed `actionWithCommit` route with the canonical centered-diff exponential tail.

noncomputable def centeredRewardCondSubGaussianWitnesses_of_infinitePi_bounded_actionMean_canonicalTail {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (lo hi : Fin K -> Nat -> Real) (horizon_pos : 0 < spec.explorationPulls * K) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun r : Rat => Set.Icc (lo (ETC.actionWithCommit spec commitArm t) t) (hi (ETC.actionWithCommit spec commitArm t) t) (((r : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun r : Rat => (((r : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec commitArm t) : Rat) : Real))) : ETC.CenteredRewardCondSubGaussianWitnesses (MeasureTheory.Measure.infinitePi coordLaw) spec model commitArm (fun omega : RewardTrace Rat => omega) (ETC.centeredDiffSubGaussianTail spec model (ETC.centeredPairwiseRewardDiffVarianceProxy spec model commitArm (ETC.centeredRewardBoundVarianceProxy lo hi)))

Under an infinite product reward-coordinate law, produce the fixed-commit pairwise empirical-mean tail contract through the conditional sub-Gaussian route with the canonical centered-diff exponential tail.

theorem pairwiseEmpMeanTailContract_of_infinitePi_bounded_actionMean_condSubGaussian_canonicalTail {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (lo hi : Fin K -> Nat -> Real) (horizon_pos : 0 < spec.explorationPulls * K) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun r : Rat => Set.Icc (lo (ETC.actionWithCommit spec commitArm t) t) (hi (ETC.actionWithCommit spec commitArm t) t) (((r : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun r : Rat => (((r : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec commitArm t) : Rat) : Real))) : ETC.PairwiseEmpMeanTailContract (MeasureTheory.Measure.infinitePi coordLaw) spec model commitArm (fun omega : RewardTrace Rat => omega) (ETC.centeredDiffSubGaussianTail spec model (ETC.centeredPairwiseRewardDiffVarianceProxy spec model commitArm (ETC.centeredRewardBoundVarianceProxy lo hi)))

Concrete fixed-commit ETC wrong-commit probability bound under an infinite product reward-coordinate law with action-matched boundedness and means.

theorem prob_argmaxCommitOracle_ne_bestArm_le_filtered_sum_centeredDiffSubGaussianTail_of_infinitePi_bounded_actionMean {K : Nat} (hK : 0 < K) (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun r : Rat => Set.Icc (lo (ETC.actionWithCommit spec commitArm t) t) (hi (ETC.actionWithCommit spec commitArm t) t) (((r : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun r : Rat => (((r : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec commitArm t) : Rat) : Real))) : MeasureTheory.Measure.infinitePi coordLaw {omega : RewardTrace Rat | (ETC.argmaxCommitOracle hK).choose (fun a : Fin K => ETC.empMeanAtExploration spec commitArm omega a) = model.bestArm -> False} <= ((Finset.univ : Finset (Fin K)).filter (fun a : Fin K => a = model.bestArm -> False)).sum (ETC.centeredDiffSubGaussianTail spec model (ETC.centeredPairwiseRewardDiffVarianceProxy spec model commitArm (ETC.centeredRewardBoundVarianceProxy lo hi)))

Concrete fixed-commit ETC wrong-commit probability bound under an infinite product reward-coordinate law, routed through the conditional sub-Gaussian canonical-tail source package.

theorem prob_argmaxCommitOracle_ne_bestArm_le_filtered_sum_centeredDiffSubGaussianTail_of_infinitePi_bounded_actionMean_condSubGaussian {K : Nat} (hK : 0 < K) (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun r : Rat => Set.Icc (lo (ETC.actionWithCommit spec commitArm t) t) (hi (ETC.actionWithCommit spec commitArm t) t) (((r : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun r : Rat => (((r : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec commitArm t) : Rat) : Real))) : MeasureTheory.Measure.infinitePi coordLaw {omega : RewardTrace Rat | (ETC.argmaxCommitOracle hK).choose (fun a : Fin K => ETC.empMeanAtExploration spec commitArm omega a) = model.bestArm -> False} <= ((Finset.univ : Finset (Fin K)).filter (fun a : Fin K => a = model.bestArm -> False)).sum (ETC.centeredDiffSubGaussianTail spec model (ETC.centeredPairwiseRewardDiffVarianceProxy spec model commitArm (ETC.centeredRewardBoundVarianceProxy lo hi)))