BanditRLProof.Algorithms.ETCInfinitePiExpectedRegretAssembly

The finite argmax commit arm selected from the fixed-commit exploration sample. This is only a naming wrapper around the existing argmax commit oracle and `ETC.empMeanAtExploration`; it does not add a new probability or filtration assumption.

noncomputable def fixedProductArgmaxCommit {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (omega : RewardTrace Rat) : Fin K

The ETC action trace that explores with `baseCommitArm` and then commits to the finite argmax empirical-mean arm selected from that exploration sample.

noncomputable def fixedProductArgmaxAction {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (omega : RewardTrace Rat) : ActionTrace (Fin K)

Named RHS budget for the fixed product-coordinate max-gap lower-integral ETC regret wrapper. This is still an `ENNReal.ofReal` surrogate budget. It does not claim Bochner or Rat-valued expected regret.

noncomputable def fixedProductMaxGapLintegralRegretBound {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) : ENNReal

Named ENNReal wrong-commit tail budget used by the fixed product-coordinate ETC argmax route.

noncomputable def fixedProductWrongCommitTailBudget {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (lo hi : Fin K -> Nat -> Real) : ENNReal

Named RHS budget for the fixed product-coordinate bad-gap lower-integral ETC regret wrapper. This is still an `ENNReal.ofReal` surrogate budget. It packages the explicit bad-gap suffix contract behind the same fixed-product tail budget used by the Bochner/Real bad-gap wrapper.

noncomputable def fixedProductBadGapLintegralRegretBound {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (badGapBound : Rat) (lo hi : Fin K -> Nat -> Real) : ENNReal

Named RHS budget for the conservative fixed product-coordinate sum-gap lower-integral ETC regret wrapper. This is the sum-gap specialization of `fixedProductBadGapLintegralRegretBound`; it removes the explicit `badGapBound` parameter while remaining on the `ENNReal.ofReal` lower-integral surface.

noncomputable def fixedProductSumGapLintegralRegretBound {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) : ENNReal

Real-valued view of the fixed product-coordinate wrong-commit tail budget.

noncomputable def fixedProductWrongCommitTailBudgetReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (lo hi : Fin K -> Nat -> Real) : Real

Named Real RHS for the fixed product-coordinate bad-gap Bochner ETC regret assembly.

noncomputable def fixedProductBadGapIntegralRegretBoundReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (badGapBound : Rat) (lo hi : Fin K -> Nat -> Real) : Real

Named Real RHS for the conservative fixed product-coordinate sum-gap Bochner ETC regret wrapper. This is the sum-gap specialization of `fixedProductBadGapIntegralRegretBoundReal`; it removes the explicit `badGapBound` parameter by using the total finite sum of model gaps as a conservative non-best suffix gap bound.

noncomputable def fixedProductSumGapIntegralRegretBoundReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) : Real

Named Real RHS for the fixed product-coordinate max-gap Bochner ETC regret wrapper. This is the max-gap specialization of `fixedProductBadGapIntegralRegretBoundReal`; it removes the explicit `badGapBound` parameter while keeping the same finite-product wrong-commit tail budget.

noncomputable def fixedProductMaxGapIntegralRegretBoundReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) : Real

The canonical fixed-product ETC commit arm uses the round-robin exploration prefix only. Internally it fixes the already-selected best arm as a harmless post-exploration seed; every public source contract below is stated directly against `ETC.exploreArm`.

noncomputable def explorationArgmaxCommit {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (omega : RewardTrace Rat) : Fin K

The canonical fixed-product ETC trace: round-robin exploration followed by the argmax commit computed from that exploration prefix.

noncomputable def explorationArgmaxAction {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (omega : RewardTrace Rat) : ActionTrace (Fin K)

Real-valued max-gap regret budget for the canonical round-robin exploration fixed-product ETC endpoint.

noncomputable def explorationMaxGapIntegralRegretBoundReal {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (r : Nat) (lo hi : Fin K -> Nat -> Real) : Real

Concrete lower-integral ETC regret assembly for the finite argmax commit oracle under an infinite product reward-coordinate law. The empirical means are computed from the fixed exploration trace determined by `baseCommitArm`; the post-exploration action trace commits to the argmax oracle choice computed from those empirical means. The suffix term is charged by an explicit non-best gap bound and the compiled infinite-product wrong-commit probability bound.

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

Polished fixed-product bad-gap lower-integral ETC regret wrapper. The statement names both the fixed-product argmax action trace and the bad-gap lower-integral RHS budget while remaining on the same fixed product-coordinate, fixed-exploration `ENNReal.ofReal` surface as the concrete assembly theorem.

theorem lintegral_ofReal_pseudoRegret_fixedProductArgmaxAction_le_fixedProductBadGapLintegralRegretBound_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (badGapBound : Rat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (hbadGap : forall a : Fin K, (a = model.bestArm -> False) -> model.gap a <= badGapBound) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : MeasureTheory.lintegral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => ENNReal.ofReal (((pseudoRegret model (ETC.fixedProductArgmaxAction spec model baseCommitArm omega) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.fixedProductBadGapLintegralRegretBound spec model baseCommitArm r badGapBound lo hi

Polished fixed-product sum-gap lower-integral ETC regret wrapper. The statement names both the fixed-product argmax action trace and the conservative sum-gap lower-integral RHS budget, while remaining on the fixed product-coordinate, fixed-exploration `ENNReal.ofReal` surface.

theorem lintegral_ofReal_pseudoRegret_fixedProductArgmaxAction_le_fixedProductSumGapLintegralRegretBound_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : MeasureTheory.lintegral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => ENNReal.ofReal (((pseudoRegret model (ETC.fixedProductArgmaxAction spec model baseCommitArm omega) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.fixedProductSumGapLintegralRegretBound spec model baseCommitArm r lo hi

Real-valued fixed-product wrong-commit probability bound. This exposes the `ENNReal.toReal` conversion used by the Bochner expected-regret assembly as a standalone reusable surface. It remains tied to the concrete infinite product-coordinate reward source and fixed exploration trace.

theorem real_measure_fixedProductArgmaxCommit_ne_bestArm_le_fixedProductWrongCommitTailBudgetReal_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : 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 rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : (MeasureTheory.Measure.infinitePi coordLaw).real {omega : RewardTrace Rat | ETC.fixedProductArgmaxCommit spec model baseCommitArm omega = model.bestArm -> False} <= ETC.fixedProductWrongCommitTailBudgetReal spec model baseCommitArm lo hi

Concrete Bochner/Real ETC regret assembly for the finite argmax commit oracle under an infinite product reward-coordinate law. This is the Real-valued counterpart of `lintegral_ofReal_pseudoRegret_argmaxCommitOracle_actionWithCommit_le_exploration_add_suffix_badGap_prob_of_infinitePi_bounded_actionMean`. It uses the same infinite-product wrong-commit probability source, converts that probability budget with `ENNReal.toReal`, and discharges the abstract integrability side condition from the measurable finite-valued commit selector.

theorem integral_real_pseudoRegret_argmaxCommitOracle_actionWithCommit_le_exploration_add_suffix_badGap_prob_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (badGapBound : Rat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (hbadGap : forall a : Fin K, (a = model.bestArm -> False) -> model.gap a <= badGapBound) (hbadGap_nonneg : (0 : Rat) <= badGapBound) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : MeasureTheory.integral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => (((pseudoRegret model (ETC.fixedProductArgmaxAction spec model baseCommitArm omega) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.fixedProductBadGapIntegralRegretBoundReal spec model baseCommitArm r badGapBound lo hi

Polished fixed-product bad-gap Bochner/Real ETC regret wrapper. The underlying concrete theorem already uses the named fixed-product argmax action in its conclusion; this wrapper gives that endpoint the same API shape as the sum-gap and max-gap Bochner wrappers.

theorem integral_real_pseudoRegret_fixedProductArgmaxAction_le_fixedProductBadGapIntegralRegretBoundReal_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (badGapBound : Rat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (hbadGap : forall a : Fin K, (a = model.bestArm -> False) -> model.gap a <= badGapBound) (hbadGap_nonneg : (0 : Rat) <= badGapBound) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : MeasureTheory.integral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => (((pseudoRegret model (ETC.fixedProductArgmaxAction spec model baseCommitArm omega) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.fixedProductBadGapIntegralRegretBoundReal spec model baseCommitArm r badGapBound lo hi

Conservative concrete Bochner/Real ETC regret assembly using the total sum of model gaps as the suffix bad-gap bound. This is the Real-valued counterpart of the existing sum-gap `ENNReal.ofReal` lower-integral adapter. It removes the explicit `badGapBound` and `hbadGap` contracts from the concrete fixed-product expected-regret theorem by using gap nonnegativity over the finite arm set.

theorem integral_real_pseudoRegret_argmaxCommitOracle_actionWithCommit_le_exploration_add_suffix_sumGap_prob_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : MeasureTheory.integral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => (((pseudoRegret model (ETC.actionWithCommit spec ((ETC.argmaxCommitOracle model.hK).choose (fun a : Fin K => ETC.empMeanAtExploration spec baseCommitArm omega a))) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.fixedProductSumGapIntegralRegretBoundReal spec model baseCommitArm r lo hi

Polished fixed-product sum-gap Bochner/Real ETC regret wrapper. The statement names both the argmax-commit action trace and the conservative Real-valued sum-gap RHS budget, while remaining on the fixed product-coordinate, fixed-exploration surface.

theorem integral_real_pseudoRegret_fixedProductArgmaxAction_le_fixedProductSumGapIntegralRegretBoundReal_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : MeasureTheory.integral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => (((pseudoRegret model (ETC.fixedProductArgmaxAction spec model baseCommitArm omega) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.fixedProductSumGapIntegralRegretBoundReal spec model baseCommitArm r lo hi

Sharper concrete Bochner/Real ETC regret assembly using `FiniteBanditModel.maxGap` as the suffix bad-gap bound. This is the Real-valued counterpart of the existing max-gap `ENNReal.ofReal` lower-integral adapter. It removes the explicit `badGapBound` and `hbadGap` contracts from the concrete fixed-product expected-regret theorem by using the compiled finite-model max-gap invariants.

theorem integral_real_pseudoRegret_argmaxCommitOracle_actionWithCommit_le_exploration_add_suffix_maxGap_prob_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : MeasureTheory.integral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => (((pseudoRegret model (ETC.actionWithCommit spec ((ETC.argmaxCommitOracle model.hK).choose (fun a : Fin K => ETC.empMeanAtExploration spec baseCommitArm omega a))) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.fixedProductMaxGapIntegralRegretBoundReal spec model baseCommitArm r lo hi

Polished fixed-product max-gap Bochner/Real ETC regret wrapper. The statement names both the argmax-commit action trace and the Real-valued RHS budget, while remaining on the fixed product-coordinate, fixed-exploration surface.

theorem integral_real_pseudoRegret_fixedProductArgmaxAction_le_fixedProductMaxGapIntegralRegretBoundReal_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : MeasureTheory.integral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => (((pseudoRegret model (ETC.fixedProductArgmaxAction spec model baseCommitArm omega) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.fixedProductMaxGapIntegralRegretBoundReal spec model baseCommitArm r lo hi

Canonical fixed-product Bochner/Real ETC expected-regret theorem stated only with round-robin exploration coordinates. Unlike the lower-level fixed-product wrapper, callers do not supply an arbitrary `baseCommitArm`: every coordinate bound and mean identity is indexed by `ETC.exploreArm`. The result remains a fixed-product/fixed-exploration endpoint and does not construct an adaptive environment or policy law.

theorem integral_real_pseudoRegret_explorationArgmaxAction_le_explorationMaxGapIntegralRegretBoundReal_of_infinitePi_bounded_exploreMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (r : Nat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.exploreArm spec t) t) (hi (ETC.exploreArm spec t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.exploreArm spec t) : Rat) : Real))) : MeasureTheory.integral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => (((pseudoRegret model (ETC.explorationArgmaxAction spec model omega) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.explorationMaxGapIntegralRegretBoundReal spec model r lo hi

Conservative concrete lower-integral ETC regret assembly using the total sum of model gaps as the suffix bad-gap bound. This removes the explicit `badGapBound`/`hbadGap` contract from the concrete infinite-product wrapper. The price is a looser suffix constant: `sum_a model.gap a` bounds every non-best gap by nonnegativity.

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

Sharper concrete lower-integral ETC regret assembly using `FiniteBanditModel.maxGap` as the suffix bad-gap bound. This keeps the same infinite-product wrong-commit probability term as the sum-gap wrapper, but charges each wrong suffix pull by the maximum local gap instead of the total sum of all gaps.

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

Polished fixed-product max-gap lower-integral ETC regret wrapper. The statement names both the argmax-commit action trace and the RHS max-gap budget, while remaining exactly on the same fixed product-coordinate, fixed-exploration, `ENNReal.ofReal` surface as the concrete max-gap assembly.

theorem lintegral_ofReal_pseudoRegret_fixedProductArgmaxAction_le_fixedProductMaxGapLintegralRegretBound_of_infinitePi_bounded_actionMean {K : Nat} (coordLaw : Nat -> MeasureTheory.Measure Rat) [forall t : Nat, MeasureTheory.IsProbabilityMeasure (coordLaw t)] (spec : ETC.Spec K) (model : FiniteBanditModel K) (baseCommitArm : Fin K) (r : Nat) (lo hi : Fin K -> Nat -> Real) (hexplorationPulls_pos : 0 < spec.explorationPulls) (h_coord_bound : forall t, t < spec.explorationPulls * K -> Filter.Eventually (fun rewardValue : Rat => Set.Icc (lo (ETC.actionWithCommit spec baseCommitArm t) t) (hi (ETC.actionWithCommit spec baseCommitArm t) t) (((rewardValue : Rat) : Real))) (MeasureTheory.ae (coordLaw t))) (h_coord_mean : forall t, t < spec.explorationPulls * K -> MeasureTheory.integral (coordLaw t) (fun rewardValue : Rat => (((rewardValue : Rat) : Real))) = (((model.mean (ETC.actionWithCommit spec baseCommitArm t) : Rat) : Real))) : MeasureTheory.lintegral (MeasureTheory.Measure.infinitePi coordLaw) (fun omega : RewardTrace Rat => ENNReal.ofReal (((pseudoRegret model (ETC.fixedProductArgmaxAction spec model baseCommitArm omega) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.fixedProductMaxGapLintegralRegretBound spec model baseCommitArm r lo hi