BanditRLProof.Algorithms.ETCFiniteArmRewardLaw

An action marginal and the conditional law of its feedback determine the joint action/feedback law. This is the measure-level composition used by the zeroth step of an `IsAlgEnvSeq`-shaped process contract.

theorem pair_map_eq_compProd_of_map_eq_of_condDistrib {Omega Action Feedback : Type*} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSpace Feedback] [StandardBorelSpace Feedback] [Nonempty Feedback] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> Action) (feedback : Omega -> Feedback) (hfeedback : Measurable feedback) (p0 : Measure Action) (feedbackKernel : ProbabilityTheory.Kernel Action Feedback) [ProbabilityTheory.IsFiniteKernel feedbackKernel] (haction : Measure.map action mu = p0) (hcond : ProbabilityTheory.condDistrib feedback action mu =ᵐ[mu.map action] feedbackKernel) : Measure.map (fun omega : Omega => (action omega, feedback omega)) mu = p0 ⊗ₘ feedbackKernel

The successor action policy and the feedback law conditional on `(history, action)` combine into the conditional law of the observable `(action, feedback)` pair given history. The proof is the joint-law characterization of `condDistrib` followed by associativity of `compProd`.

theorem condDistrib_pair_ae_eq_compProd_of_split {Omega History Action Feedback : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Feedback] [StandardBorelSpace Feedback] [Nonempty Feedback] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (feedback : Omega -> Feedback) (hfeedback : Measurable feedback) (policy : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel policy] (feedbackKernel : ProbabilityTheory.Kernel (History × Action) Feedback) [ProbabilityTheory.IsMarkovKernel feedbackKernel] (hactionCond : ProbabilityTheory.condDistrib action history mu =ᵐ[mu.map history] policy) (hfeedbackCond : ProbabilityTheory.condDistrib feedback (fun omega : Omega => (history omega, action omega)) mu =ᵐ[ mu.map (fun omega : Omega => (history omega, action omega))] feedbackKernel) : ProbabilityTheory.condDistrib (fun omega : Omega => (action omega, feedback omega)) history mu =ᵐ[ mu.map history] policy ⊗ₖ feedbackKernel

A constant conditional distribution given a fine conditioning variable stays constant after projecting to any measurable coarser conditioning variable. The proof uses the defining joint-law identity for `condDistrib`: the fine joint law is a product because the kernel is constant, and mapping that product by `(project, id)` gives the corresponding coarse joint law.

theorem condDistrib_ae_eq_const_of_comp {Omega Fine Coarse Target : Type*} [MeasurableSpace Omega] [MeasurableSpace Fine] [MeasurableSpace Coarse] [MeasurableSpace Target] [StandardBorelSpace Target] [Nonempty Target] (mu : Measure Omega) [IsFiniteMeasure mu] (fine : Omega -> Fine) (hfine : Measurable fine) (coarse : Omega -> Coarse) (target : Omega -> Target) (htarget : Measurable target) (project : Fine -> Coarse) (hproject : Measurable project) (hcomp : coarse = project ∘ fine) (Q : Measure Target) [IsProbabilityMeasure Q] (hcond : ProbabilityTheory.condDistrib target fine mu =ᵐ[mu.map fine] ProbabilityTheory.Kernel.const Fine Q) : ProbabilityTheory.condDistrib target coarse mu =ᵐ[mu.map coarse] ProbabilityTheory.Kernel.const Coarse Q

A constant conditional distribution determines the target marginal.

theorem map_eq_of_condDistrib_ae_eq_const {Omega Condition Target : Type*} [MeasurableSpace Omega] [MeasurableSpace Condition] [MeasurableSpace Target] [StandardBorelSpace Target] [Nonempty Target] (mu : Measure Omega) [IsProbabilityMeasure mu] (condition : Omega -> Condition) (hcondition : Measurable condition) (target : Omega -> Target) (htarget : Measurable target) (Q : Measure Target) [IsProbabilityMeasure Q] (hcond : ProbabilityTheory.condDistrib target condition mu =ᵐ[mu.map condition] ProbabilityTheory.Kernel.const Condition Q) : Measure.map target mu = Q

An action-selected conditional kernel becomes constant when the selected value is almost surely constant under the source process. The selector equality is pushed to the conditioning-variable law with `ae_map_iff`; the supplied pointwise kernel-selection identity then rewrites the conditional kernel almost everywhere.

theorem condDistrib_ae_eq_const_of_ae_eq_selected {Omega Fine Action Target : Type*} [MeasurableSpace Omega] [MeasurableSpace Fine] [MeasurableSpace Action] [MeasurableEq Action] [MeasurableSpace Target] [StandardBorelSpace Target] [Nonempty Target] (mu : Measure Omega) [IsFiniteMeasure mu] (fine : Omega -> Fine) (hfine : Measurable fine) (target : Omega -> Target) (selected : Fine -> Action) (hselected : Measurable selected) (kernel : ProbabilityTheory.Kernel Fine Target) (actionLaw : Action -> Measure Target) (selectedValue : Action) (hselectedValue : (fun omega : Omega => selected (fine omega)) =ᵐ[mu] fun _omega => selectedValue) (hkernel : forall value : Fine, kernel value = actionLaw (selected value)) (hcond : ProbabilityTheory.condDistrib target fine mu =ᵐ[mu.map fine] kernel) : ProbabilityTheory.condDistrib target fine mu =ᵐ[mu.map fine] ProbabilityTheory.Kernel.const Fine (actionLaw selectedValue)

Exact model means and direct per-arm sub-Gaussian witnesses turn finite-arm probability laws into a context-independent centered reward-kernel law. Unlike `finiteArmBoundedCenteredRewardKernelLaw`, this constructor does not derive the MGF from common bounded support. The supplied proxy is shared by all arms, matching the concentration contract of the LML ETC theorem while retaining ABRL's current `Rat` reward trace.

noncomputable def finiteArmCenteredRewardKernelLaw_of_hasSubgaussianMGF {K : Nat} {Context : Type} [MeasurableSpace Context] (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) : RewardKernel.CenteredRewardKernelLaw (RewardKernel.contextIndependentOfActionLaws (Context

Common boundedness and exact model means turn finite-arm probability laws into a context-independent centered reward-kernel law. The variance proxy is the common Hoeffding proxy for `[lo, hi]`. Raw reward integrability follows from `Integrable.of_mem_Icc`; the centered MGF is the Mathlib-backed bounded-variable wrapper in `ConcentrationSubGaussian`.

noncomputable def finiteArmBoundedCenteredRewardKernelLaw {K : Nat} {Context : Type} [MeasurableSpace Context] (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) : RewardKernel.CenteredRewardKernelLaw (RewardKernel.contextIndependentOfActionLaws (Context

Canonical generated-history ETC conditional MGF from bounded finite-arm laws. Because every arm uses the same interval `[lo, hi]`, the kernel variance proxy is constant. The selected-history variance ceiling required by the generic trajectory theorem is therefore discharged by reflexivity.

theorem explorationArgmaxHistory_centeredReward_succ_hasCondSubgaussianMGF_of_boundedArmLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (i : Nat) : let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical generated-history ETC successor conditional MGF from direct finite-arm sub-Gaussian laws with a common variance proxy. The theorem removes common bounded support from the canonical kernel route. Its remaining contracts are exact model means, a shared per-arm MGF proxy, and measurable history context; the reward trace is still `Rat`-valued.

theorem explorationArgmaxHistory_centeredReward_succ_hasCondSubgaussianMGF_of_armLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (i : Nat) : let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical ETC Azuma-Hoeffding bound for the full centered reward sum, including the actual reward at time zero. The initial trajectory law is fixed to the law of `ETC.exploreArm spec 0`. `RewardKernel.trajMeasure_map_eval_zero` transfers its bounded centered MGF to the zeroth trajectory coordinate, while the generated-history kernel law gives the successor conditional MGF witnesses. Unlike the earlier zero-initialized sum-tail surface, this sum contains rewards at every index in `Finset.range n`.

theorem explorationArgmaxHistory_centeredRewardProcess_sum_tail_ennreal_of_boundedArmLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (n : Nat) {eps : Real} (heps : 0 <= eps) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Bounded finite-arm laws provide the reward-level conditional sub-Gaussian witness package used by the existing fixed-commit pairwise ETC tail route. The ambient measure is the canonical generated-history trajectory. During the exploration horizon its generated action prefix agrees with `actionWithCommit spec model.bestArm`; the corresponding shifted history filtrations therefore agree. This transports the canonical selected-reward conditional MGF to the fixed-commit witness interface without assuming coordinate independence.

noncomputable def explorationArgmaxHistory_centeredRewardCondSubGaussianWitnesses_of_boundedArmLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Direct common-sub-Gaussian arm laws provide the reward-level conditional witness package used by the fixed-commit pairwise ETC tail route. The initial witness is transported from the initial arm law. Successor witnesses come from the generated-history kernel law and are moved to the fixed `actionWithCommit` filtration using exploration-prefix action equality. No bounded-support assumption or arm union is used.

noncomputable def explorationArgmaxHistory_centeredRewardCondSubGaussianWitnesses_of_armLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical pairwise empirical-mean tail contract for the generated-history ETC trajectory under bounded finite-arm reward laws. This consumes the reward-level witness above through the existing centered pairwise conditional sub-Gaussian adapter. The contract matches the exact empirical means used by `explorationArgmaxCommit`.

theorem explorationArgmaxHistory_pairwiseEmpMeanTailContract_of_boundedArmLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical pairwise empirical-mean tail contract for generated-history ETC under direct common-sub-Gaussian finite-arm laws. This is the concentration endpoint of the direct-MGF leaf. It retains the exact empirical means and fixed-commit one-sided pairwise process used by the bounded route, but replaces common support by the caller's shared `sigma2`.

theorem explorationArgmaxHistory_pairwiseEmpMeanTailContract_of_armLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical generated-history ETC probability bound for committing to one fixed non-best arm under direct common-sub-Gaussian finite-arm laws. The theorem consumes the direct-MGF pairwise empirical-mean contract. It keeps the single concrete commit fiber and therefore introduces no arm union.

theorem explorationArgmaxHistory_prob_commit_eq_arm_le_pairwiseTail_of_armLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (a : Fin K) (hne : a = model.bestArm -> False) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical generated-history ETC probability bound for committing to one fixed non-best arm under bounded finite-arm reward laws. The event is the actual concrete empirical-mean argmax fiber. Its probability is bounded by the matching one-sided centered pairwise tail, with no union over the other arms. This is the armwise probability source required by the gap-weighted Bochner assembly.

theorem explorationArgmaxHistory_prob_commit_eq_arm_le_pairwiseTail_of_boundedArmLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (a : Fin K) (hne : a = model.bestArm -> False) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical generated-history ETC wrong-commit probability bound from bounded finite-arm laws. The event is the actual empirical-mean argmax commit used by the generated ETC policy. Its probability is bounded by the finite union of the canonical centered pairwise sub-Gaussian tails. This is a one-horizon, one-sided, union-bounded result; it does not yet assemble expected regret or transport to an externally supplied environment law.

theorem explorationArgmaxHistory_prob_wrongCommit_le_pairwiseTailSum_of_boundedArmLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical finite-union wrong-commit tail budget for common-bounded arm laws. Every reward-level variance proxy is the common interval proxy. The pairwise mask retains that proxy only when the exploration trace samples the candidate arm or the selected best arm.

noncomputable def canonicalBoundedArmWrongCommitTailBudget {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (lo hi : Real) : ENNReal

Real view of the canonical bounded-arm wrong-commit tail budget.

noncomputable def canonicalBoundedArmWrongCommitTailBudgetReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (lo hi : Real) : Real

Named Real regret budget for canonical bounded-arm generated ETC. The first term pays the round-robin exploration cost. The second charges the remaining `r` rounds by `model.maxGap` times the canonical wrong-commit budget.

noncomputable def canonicalBoundedArmMaxGapIntegralRegretBoundReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (r : Nat) (lo hi : Real) : Real

Real view of one canonical bounded-arm centered pairwise tail.

noncomputable def canonicalBoundedArmPairwiseTailReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (lo hi : Real) (a : Fin K) : Real

Named Real regret budget for the canonical bounded-arm per-arm ETC route. The exploration term is unchanged. The suffix keeps every arm gap paired with that arm's own canonical pairwise tail instead of collapsing the finite family to `model.maxGap` times a union probability.

noncomputable def canonicalBoundedArmPerArmIntegralRegretBoundReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (r : Nat) (lo hi : Real) : Real

Real view of one canonical common-sub-Gaussian arm pairwise tail.

noncomputable def canonicalSubGaussianArmPairwiseTailReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (sigma2 : NNReal) (a : Fin K) : Real

Named Real regret budget for the canonical common-sub-Gaussian per-arm ETC route over `Rat` rewards. The suffix preserves one gap-weighted direct-MGF pairwise tail per arm and takes no finite-arm union.

noncomputable def canonicalSubGaussianArmPerArmIntegralRegretBoundReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (r : Nat) (sigma2 : NNReal) : Real

Real-valued canonical probability bound for one non-best commit fiber under direct common-sub-Gaussian finite-arm laws. The ENNReal pairwise tail is finite because it is an `ofReal` exponential, so the conversion preserves the concrete event and introduces no arm union.

theorem real_measure_explorationArgmaxCommit_eq_arm_le_canonicalSubGaussianArmPairwiseTailReal {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (a : Fin K) (hne : a = model.bestArm -> False) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Real-valued canonical probability bound for committing to one non-best arm. The corresponding ENNReal tail is finite because it is `ENNReal.ofReal` of a real exponential, so `ENNReal.toReal_mono` transports the compiled armwise probability theorem without changing the event or taking a union.

theorem real_measure_explorationArgmaxCommit_eq_arm_le_canonicalBoundedArmPairwiseTailReal {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (a : Fin K) (hne : a = model.bestArm -> False) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Real-valued canonical wrong-commit probability bound. The ENNReal finite tail sum is never infinite because each summand is an `ENNReal.ofReal` exponential. This wrapper converts the compiled canonical pairwise probability theorem with `ENNReal.toReal_mono`.

theorem real_measure_explorationArgmaxCommit_ne_bestArm_le_canonicalBoundedArmWrongCommitTailBudgetReal {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Bochner expected pseudo-regret bound for the generated finite-history ETC action under its canonical bounded-arm trajectory law. The measurable empirical-mean argmax supplies both wrong-event measurability and pseudo-regret integrability. The preceding Real probability wrapper feeds the generic pointwise-to-expectation ETC assembly with `model.maxGap` as the suffix charge. This is the canonical action-dependent kernel theorem; transport to an externally supplied environment law remains separate.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalBoundedArmMaxGapIntegralRegretBoundReal {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical bounded-arm generated-history ETC expected-regret theorem with a per-arm gap-weighted suffix budget. Each non-best commit fiber uses its own canonical centered pairwise tail. The best-arm term vanishes by `gap_bestArm`, so no artificial tail hypothesis is needed there. This endpoint removes the max-gap finite-union collapse from the canonical bounded-Rat theorem while retaining the same exploration term.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalBoundedArmPerArmIntegralRegretBoundReal {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Canonical generated-history ETC expected-regret theorem with direct common- sub-Gaussian finite-arm laws and a per-arm gap-weighted suffix budget. Each non-best commit fiber is charged by its own direct-MGF pairwise tail. The best-arm term vanishes by `gap_bestArm`; no bounded-support assumption, max-gap collapse, or arm union is used. Rewards and model means remain `Rat`-valued.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

Finite-prefix realization of the generated ETC pseudo-regret integrand. The completed trace is only an implementation device. Once the supplied history contains the complete exploration prefix, the value agrees with the original generated-history action by the factorization theorem below.

noncomputable def explorationArgmaxPrefixRegretReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (t r : Nat) (history : History.FiniteRewardHistory Rat t) : Real

The finite-prefix ETC pseudo-regret realization is measurable.

theorem measurable_explorationArgmaxPrefixRegretReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (t r : Nat) : Measurable (ETC.explorationArgmaxPrefixRegretReal spec model t r)

The finite-prefix realization agrees with canonical ETC whenever the retained history covers every exploration reward coordinate.

theorem explorationArgmaxPrefixRegretReal_finiteRewardHistoryOfTrace {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (reward : RewardTrace Rat) (t r : Nat) (horizon_le : spec.explorationPulls * K <= t + 1) : ETC.explorationArgmaxPrefixRegretReal spec model t r (History.finiteRewardHistoryOfTrace reward t) = (((pseudoRegret model (ETC.explorationArgmaxAction spec model reward) (spec.explorationPulls * K + r) : Rat) : Real))

Generated-history form of the finite exploration-prefix regret factorization.

theorem explorationArgmaxPrefixRegretReal_finiteRewardHistoryOfTrace_generated {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (reward : RewardTrace Rat) (t r : Nat) (hexplorationPulls_pos : 0 < spec.explorationPulls) (horizon_le : spec.explorationPulls * K <= t + 1) : ETC.explorationArgmaxPrefixRegretReal spec model t r (History.finiteRewardHistoryOfTrace reward t) = (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model reward) (spec.explorationPulls * K + r) : Rat) : Real))

The generated-history ETC pseudo-regret integral depends only on the finite exploration-prefix pushforward. This law-transport equality is independent of the reward-law or concentration route used later to bound either integral. It packages the measurable prefix factorization once for both max-gap and per-arm canonical endpoints.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_eq_of_explorationPrefix_map_eq {K : Nat} (mu nu : Measure (RewardTrace Rat)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hprefix : let explorationLast := spec.explorationPulls * K - 1 Measure.map (fun trajectory : RewardTrace Rat => History.finiteRewardHistoryOfTrace trajectory explorationLast) mu = Measure.map (fun trajectory : RewardTrace Rat => History.finiteRewardHistoryOfTrace trajectory explorationLast) nu) : integral mu (fun trajectory : RewardTrace Rat => (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model trajectory) (spec.explorationPulls * K + r) : Rat) : Real))) = integral nu (fun trajectory : RewardTrace Rat => (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model trajectory) (spec.explorationPulls * K + r) : Rat) : Real)))

External-law ETC expected-regret theorem from exploration-prefix law equality. The external reward law need not equal the canonical Ionescu-Tulcea law on the full infinite trajectory. It is enough that their pushforwards to the `m * K` exploration rewards agree: the generated ETC action and its finite horizon pseudo-regret factor through exactly that prefix. This is the law transport surface needed by external stationary-bandit environment models.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalBoundedArmMaxGapIntegralRegretBoundReal_of_explorationPrefix_map_eq {K : Nat} {Context : Type} [MeasurableSpace Context] (mu : Measure (RewardTrace Rat)) [IsProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hprefix : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

External-law canonical per-arm ETC expected-regret theorem from exploration- prefix law equality. The external reward law only needs the same `m * K` exploration-prefix pushforward as the canonical generated-history trajectory. The resulting bound preserves each arm's own gap-weighted pairwise tail and takes no union over commit arms.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalBoundedArmPerArmIntegralRegretBoundReal_of_explorationPrefix_map_eq {K : Nat} {Context : Type} [MeasurableSpace Context] (mu : Measure (RewardTrace Rat)) [IsProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hprefix : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

External-law common-sub-Gaussian per-arm ETC expected regret from exploration- prefix law equality. Only the `m * K` exploration reward-prefix pushforward must match the canonical generated-history trajectory. The direct-MGF gap-weighted armwise budget is transported without a full trajectory law, suffix law, or arm union.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal_of_explorationPrefix_map_eq {K : Nat} {Context : Type} [MeasurableSpace Context] (mu : Measure (RewardTrace Rat)) [IsProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hprefix : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

External-process ETC expected regret from initial and successor conditional reward laws. The contract is local to the exploration prefix: coordinate measurability, the zeroth reward marginal, and the conditional distribution of reward `i + 1` given rewards through `i` for `i < m * K - 1`. The generic finite-prefix law result identifies the required pushforward with the Ionescu-Tulcea process; the preceding prefix-transport theorem then supplies the regret bound.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalBoundedArmMaxGapIntegralRegretBoundReal_of_initial_map_eq_condDistrib {Omega : Type*} {K : Nat} {Context : Type} [MeasurableSpace Omega] [MeasurableSpace Context] (mu : Measure Omega) [IsProbabilityMeasure mu] (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = armLaw (ETC.exploreArm spec 0)) (hcond : let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

External-process canonical per-arm ETC expected regret from initial and successor conditional reward laws. The conditional laws are needed only through the exploration prefix. They identify the reward-trace prefix pushforward with the canonical trajectory; the per-arm prefix transport then preserves each gap-weighted pairwise tail without a wrong-event union.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalBoundedArmPerArmIntegralRegretBoundReal_of_initial_map_eq_condDistrib {Omega : Type*} {K : Nat} {Context : Type} [MeasurableSpace Omega] [MeasurableSpace Context] (mu : Measure Omega) [IsProbabilityMeasure mu] (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = armLaw (ETC.exploreArm spec 0)) (hcond : let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

External-process common-sub-Gaussian per-arm ETC expected regret from an initial reward marginal and successor conditional reward laws. The conditional laws are required only through exploration. They identify the external reward-prefix law with the canonical trajectory and then invoke the direct-MGF prefix transport theorem.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal_of_initial_map_eq_condDistrib {Omega : Type*} {K : Nat} {Context : Type} [MeasurableSpace Omega] [MeasurableSpace Context] (mu : Measure Omega) [IsProbabilityMeasure mu] (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = armLaw (ETC.exploreArm spec 0)) (hcond : let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context

During exploration, the generated-history ETC step kernel is exactly the law of the arm scheduled at time `i + 1`. The context disappears because `contextIndependentOfActionLaws` selects only the policy action, and the history state disappears because the exploration branch of the policy is deterministic.

theorem explorationArgmaxHistory_stepKernel_apply_eq_exploreArmLaw_of_lt {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (i : Nat) (hi : i + 1 < spec.explorationPulls * K) (history : (j : Finset.Iic i) -> Rat) : RewardKernel.historyStepKernelFamily (RewardKernel.contextIndependentOfActionLaws (Context

Practical external-process ETC expected regret from the conditional laws of the scheduled exploration arms. Unlike the preceding theorem, callers do not mention the local `historyStepKernelFamily`. They provide the initial arm law and, before the end of exploration, the conditional law of reward `i + 1` as the stationary law of `exploreArm spec (i + 1)`. The exploration step-kernel equality above turns that environment-facing contract into the canonical conditional-law contract.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalBoundedArmMaxGapIntegralRegretBoundReal_of_initial_map_eq_explorationArm_condDistrib {Omega : Type*} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = armLaw (ETC.exploreArm spec 0)) (hcond : forall i : Nat, i < spec.explorationPulls * K - 1 -> ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i) mu =ᵐ[ mu.map (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i)] fun _history => armLaw (ETC.exploreArm spec (i + 1))) : integral mu (fun omega : Omega => (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model (reward omega)) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.canonicalBoundedArmMaxGapIntegralRegretBoundReal spec model r lo hi

Practical external-process per-arm ETC expected regret from the conditional laws of the scheduled exploration arms. The step-kernel equality above converts the environment-facing scheduled-arm laws into the canonical conditional-law contract. The per-arm consumer then keeps the gap-weighted pairwise tails separate, without a wrong-event union.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalBoundedArmPerArmIntegralRegretBoundReal_of_initial_map_eq_explorationArm_condDistrib {Omega : Type*} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = armLaw (ETC.exploreArm spec 0)) (hcond : forall i : Nat, i < spec.explorationPulls * K - 1 -> ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i) mu =ᵐ[ mu.map (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i)] fun _history => armLaw (ETC.exploreArm spec (i + 1))) : integral mu (fun omega : Omega => (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model (reward omega)) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.canonicalBoundedArmPerArmIntegralRegretBoundReal spec model r lo hi

Practical external-process common-sub-Gaussian per-arm ETC expected regret from the conditional laws of the scheduled exploration arms. The public contract exposes no local context, policy state, reward kernel, or trajectory measure. It preserves the canonical direct-MGF gap-weighted armwise budget and requires no bounded support or arm union.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal_of_initial_map_eq_explorationArm_condDistrib {Omega : Type*} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = armLaw (ETC.exploreArm spec 0)) (hcond : forall i : Nat, i < spec.explorationPulls * K - 1 -> ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i) mu =ᵐ[ mu.map (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i)] fun _history => armLaw (ETC.exploreArm spec (i + 1))) : integral mu (fun omega : Omega => (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model (reward omega)) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.canonicalSubGaussianArmPerArmIntegralRegretBoundReal spec model r sigma2

External ETC expected regret from LML-shaped action/reward-history conditional laws during exploration. The initial reward law is supplied conditionally on the first action. Each successor reward has the scheduled exploration-arm law conditionally on the complete action/reward prefix together with the next action. Since those laws are constant, `RewardKernel.condDistrib_ae_eq_const_of_comp` projects them to the reward-only prefixes consumed by the preceding environment-facing theorem.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalBoundedArmMaxGapIntegralRegretBoundReal_of_actionRewardHistory_explorationArm_condDistrib {Omega : Type*} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hzero : ProbabilityTheory.condDistrib (fun omega : Omega => reward omega 0) (fun omega : Omega => action omega 0) mu =ᵐ[ mu.map (fun omega : Omega => action omega 0)] ProbabilityTheory.Kernel.const (Fin K) (armLaw (ETC.exploreArm spec 0))) (hcond : forall i : Nat, i < spec.explorationPulls * K - 1 -> let fullCondition := fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)) ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) fullCondition mu =ᵐ[mu.map fullCondition] ProbabilityTheory.Kernel.const (History.FinitePairHistory (Fin K) Rat i × Fin K) (armLaw (ETC.exploreArm spec (i + 1)))) : integral mu (fun omega : Omega => (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model (reward omega)) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.canonicalBoundedArmMaxGapIntegralRegretBoundReal spec model r lo hi

External per-arm ETC expected regret from LML-shaped action/reward-history conditional laws during exploration. Constant scheduled-arm laws conditioned on the complete action/reward prefix and next action coarsen to reward-only prefixes. The scheduled-arm per-arm consumer then preserves the gap-weighted armwise tails without a wrong-event union.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalBoundedArmPerArmIntegralRegretBoundReal_of_actionRewardHistory_explorationArm_condDistrib {Omega : Type*} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hzero : ProbabilityTheory.condDistrib (fun omega : Omega => reward omega 0) (fun omega : Omega => action omega 0) mu =ᵐ[ mu.map (fun omega : Omega => action omega 0)] ProbabilityTheory.Kernel.const (Fin K) (armLaw (ETC.exploreArm spec 0))) (hcond : forall i : Nat, i < spec.explorationPulls * K - 1 -> let fullCondition := fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)) ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) fullCondition mu =ᵐ[mu.map fullCondition] ProbabilityTheory.Kernel.const (History.FinitePairHistory (Fin K) Rat i × Fin K) (armLaw (ETC.exploreArm spec (i + 1)))) : integral mu (fun omega : Omega => (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model (reward omega)) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.canonicalBoundedArmPerArmIntegralRegretBoundReal spec model r lo hi

External direct-MGF per-arm ETC expected regret from LML-shaped action/reward-history conditional laws during exploration. The initial constant conditional reward law yields the time-zero marginal. Each successor constant scheduled-arm law is coarsened from the complete action/reward prefix and next action to the reward-only prefix, then the external scheduled-arm direct-MGF theorem preserves the gap-weighted armwise budget without bounded support or an arm union.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal_of_actionRewardHistory_explorationArm_condDistrib {Omega : Type*} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hzero : ProbabilityTheory.condDistrib (fun omega : Omega => reward omega 0) (fun omega : Omega => action omega 0) mu =ᵐ[ mu.map (fun omega : Omega => action omega 0)] ProbabilityTheory.Kernel.const (Fin K) (armLaw (ETC.exploreArm spec 0))) (hcond : forall i : Nat, i < spec.explorationPulls * K - 1 -> let fullCondition := fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)) ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) fullCondition mu =ᵐ[mu.map fullCondition] ProbabilityTheory.Kernel.const (History.FinitePairHistory (Fin K) Rat i × Fin K) (armLaw (ETC.exploreArm spec (i + 1)))) : integral mu (fun omega : Omega => (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model (reward omega)) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.canonicalSubGaussianArmPerArmIntegralRegretBoundReal spec model r sigma2

External bounded ETC regret from action-dependent stationary feedback kernels and almost-sure exploration action identities. This is the dependency-light local analogue of the law transport exposed by the exact-seed LML `IsAlgEnvSeq` fields: the initial feedback kernel is indexed by action zero, each later kernel is indexed by the next action in the complete history condition, and the exploration action identities make those selectors almost surely equal to the scheduled round-robin arms.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalBoundedArmMaxGapIntegralRegretBoundReal_of_actionDependent_actionRewardHistory_condDistrib {Omega : Type*} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hactionZero : (fun omega : Omega => action omega 0) =ᵐ[mu] fun _omega => ETC.exploreArm spec 0) (hactionExplore : forall i : Nat, i < spec.explorationPulls * K - 1 -> (fun omega : Omega => action omega (i + 1)) =ᵐ[mu] fun _omega => ETC.exploreArm spec (i + 1)) (hzero : ProbabilityTheory.condDistrib (fun omega : Omega => reward omega 0) (fun omega : Omega => action omega 0) mu =ᵐ[ mu.map (fun omega : Omega => action omega 0)] ProbabilityTheory.Kernel.ofFunOfCountable armLaw) (hcond : forall i : Nat, i < spec.explorationPulls * K - 1 -> let fullCondition := fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)) ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) fullCondition mu =ᵐ[mu.map fullCondition] (RewardKernel.contextIndependentOfActionLaws (Context

External per-arm ETC regret from action-dependent stationary feedback kernels and almost-sure exploration action identities. The selector transport turns each action-indexed feedback kernel into the constant law of the scheduled exploration arm. The full-history per-arm consumer then preserves the gap-weighted armwise tails without a wrong-event union.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalBoundedArmPerArmIntegralRegretBoundReal_of_actionDependent_actionRewardHistory_condDistrib {Omega : Type*} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hmeas : forall arm, AEMeasurable (fun reward : Rat => (((reward : Rat) : Real))) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi (((reward : Rat) : Real))) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hactionZero : (fun omega : Omega => action omega 0) =ᵐ[mu] fun _omega => ETC.exploreArm spec 0) (hactionExplore : forall i : Nat, i < spec.explorationPulls * K - 1 -> (fun omega : Omega => action omega (i + 1)) =ᵐ[mu] fun _omega => ETC.exploreArm spec (i + 1)) (hzero : ProbabilityTheory.condDistrib (fun omega : Omega => reward omega 0) (fun omega : Omega => action omega 0) mu =ᵐ[ mu.map (fun omega : Omega => action omega 0)] ProbabilityTheory.Kernel.ofFunOfCountable armLaw) (hcond : forall i : Nat, i < spec.explorationPulls * K - 1 -> let fullCondition := fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)) ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) fullCondition mu =ᵐ[mu.map fullCondition] (RewardKernel.contextIndependentOfActionLaws (Context

External direct-MGF per-arm ETC regret from action-dependent stationary feedback kernels and almost-sure exploration action identities. The selector transport converts the raw action-indexed initial and successor feedback kernels into the constant laws of the scheduled exploration arms. The full action/reward-history direct-MGF consumer then returns the same gap-weighted armwise budget without bounded support or an arm union.

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_reward_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal_of_actionDependent_actionRewardHistory_condDistrib {Omega : Type*} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) (hactionZero : (fun omega : Omega => action omega 0) =ᵐ[mu] fun _omega => ETC.exploreArm spec 0) (hactionExplore : forall i : Nat, i < spec.explorationPulls * K - 1 -> (fun omega : Omega => action omega (i + 1)) =ᵐ[mu] fun _omega => ETC.exploreArm spec (i + 1)) (hzero : ProbabilityTheory.condDistrib (fun omega : Omega => reward omega 0) (fun omega : Omega => action omega 0) mu =ᵐ[ mu.map (fun omega : Omega => action omega 0)] ProbabilityTheory.Kernel.ofFunOfCountable armLaw) (hcond : forall i : Nat, i < spec.explorationPulls * K - 1 -> let fullCondition := fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)) ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) fullCondition mu =ᵐ[mu.map fullCondition] (RewardKernel.contextIndependentOfActionLaws (Context