BanditRLProof.Algorithms.ETCExpectedRegretAssembly

Lower-integral assembly for an `Omega`-indexed ETC commit selector. The theorem consumes a pointwise non-best gap bound and an abstract upper bound `pWrong` on the wrong-commit event probability. It is intentionally still an `ENNReal.ofReal` lower-integral statement, matching the existing expectation surface in the project.

theorem lintegral_ofReal_pseudoRegret_actionWithCommit_choice_le_exploration_add_suffix_badGap_prob {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commit : Omega -> Fin K) (r : Nat) (badGapBound : Rat) (pWrong : ENNReal) (hbadGap : forall a : Fin K, (a = model.bestArm -> False) -> model.gap a <= badGapBound) (hmeas_wrong : MeasurableSet {omega : Omega | commit omega = model.bestArm -> False}) (hprob_wrong : mu {omega : Omega | commit omega = model.bestArm -> False} <= pWrong) : MeasureTheory.lintegral mu (fun omega : Omega => ENNReal.ofReal (((pseudoRegret model (ETC.actionWithCommit spec (commit omega)) (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))) * pWrong

Finite-arm `actionWithCommit` pseudo-regret has an integrable Real cast when the selected commit arm is measurable and the ambient measure is finite. The proof uses only the finite range of `commit : Omega -> Fin K`: the integrand is a measurable finite-valued function, hence bounded by the finite sum of the absolute values of its arm-indexed constants.

theorem integrable_real_pseudoRegret_actionWithCommit_choice_of_measurable_commit {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commit : Omega -> Fin K) (r : Nat) (hmeas_commit : Measurable commit) : Integrable (fun omega : Omega => (((pseudoRegret model (ETC.actionWithCommit spec (commit omega)) (spec.explorationPulls * K + r) : Rat) : Real))) mu

Bochner/Real expected-regret assembly with a separate probability charge for each possible commit arm. The suffix term is decomposed into the finite family of measurable events `{omega | commit omega = a}`. Unlike the coarser wrong-commit wrapper below, this theorem preserves every arm gap and therefore exposes the per-arm RHS needed by the LML ETC route. It does not supply the armwise probability bounds themselves.

theorem integral_real_pseudoRegret_actionWithCommit_choice_le_exploration_add_suffix_sum_gap_mul_commit_prob {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commit : Omega -> Fin K) (r : Nat) (hmeas_commit : Measurable commit) : MeasureTheory.integral mu (fun omega : Omega => (((pseudoRegret model (ETC.actionWithCommit spec (commit omega)) (spec.explorationPulls * K + r) : Rat) : Real))) <= (((((Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a)) * (((spec.explorationPulls : Nat) : Rat)) : Rat) : Real)) + (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => ((((((r : Nat) : Rat) * model.gap a : Rat) : Real))) * mu.real {omega : Omega | commit omega = a})

Bochner/Real expected-regret assembly for an `Omega`-indexed ETC commit selector. This is the Real-valued analogue of `lintegral_ofReal_pseudoRegret_actionWithCommit_choice_le_exploration_add_suffix_badGap_prob`. It still consumes an abstract wrong-commit probability bound, but the conclusion is an ordinary Bochner integral of the Real-cast pseudo-regret.

theorem integral_real_pseudoRegret_actionWithCommit_choice_le_exploration_add_suffix_badGap_prob {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commit : Omega -> Fin K) (r : Nat) (badGapBound : Rat) (pWrong : Real) (hbadGap : forall a : Fin K, (a = model.bestArm -> False) -> model.gap a <= badGapBound) (hbadGap_nonneg : (0 : Rat) <= badGapBound) (hmeas_wrong : MeasurableSet {omega : Omega | commit omega = model.bestArm -> False}) (hprob_wrong : mu.real {omega : Omega | commit omega = model.bestArm -> False} <= pWrong) (hinteg : Integrable (fun omega : Omega => (((pseudoRegret model (ETC.actionWithCommit spec (commit omega)) (spec.explorationPulls * K + r) : Rat) : Real))) mu) : MeasureTheory.integral mu (fun omega : Omega => (((pseudoRegret model (ETC.actionWithCommit spec (commit omega)) (spec.explorationPulls * K + r) : Rat) : Real))) <= (((((Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a)) * (((spec.explorationPulls : Nat) : Rat)) : Rat) : Real)) + ((((((r : Nat) : Rat) * badGapBound : Rat) : Real)) * pWrong)