BanditRLProof.Algorithms.ETCCondSubGaussianWitnesses

Centered pairwise reward differences are measurable at time `t` with respect to the shifted generated history filtration. The shifted filtration contains action/reward observations with index `< t+1`, so the reward coordinate at time `t` is available. This proves only the adaptedness/measurability part of the conditional route; it does not prove any conditional MGF or conditional expectation identity.

theorem measurable_centeredPairwiseRewardDiff_historyFiltrationSucc {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (a : Fin K) (t : Nat) : @Measurable Omega Real (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) inferInstance (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega)

The fixed-commit ETC centered reward-difference process is strongly adapted to the shifted generated history filtration. This discharges the `StronglyAdapted` witness field for the conditional centered-diff package under the local discrete history model. Conditional MGF witnesses remain separate assumptions.

theorem stronglyAdapted_centeredPairwiseRewardDiff_historyFiltrationSucc {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (a : Fin K) : MeasureTheory.StronglyAdapted (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward) (fun t omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega)

Independence-based conditional mean-zero source for one centered reward coordinate. If the sigma-algebra generated by the centered reward coordinate is independent of the conditioning sigma-algebra, and the centered reward has global integral zero, then its conditional expectation against that sigma-algebra is zero. This is a thin ETC-shaped wrapper around Mathlib's `condExp_indep_eq`; it does not derive the required independence or integral identity from a reward kernel.

theorem centeredReward_condExp_eq_zero_of_indep {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (model : FiniteBanditModel K) (reward : Omega -> RewardTrace Rat) (b : Fin K) (t : Nat) (hmeas : @Measurable Omega Real mOmega inferInstance (fun omega : Omega => (((reward omega t - model.mean b : Rat) : Real)))) (h_indep : ProbabilityTheory.Indep (MeasurableSpace.comap (fun omega : Omega => (((reward omega t - model.mean b : Rat) : Real))) inferInstance) mcond mu) (h_integral : MeasureTheory.integral mu (fun omega : Omega => (((reward omega t - model.mean b : Rat) : Real))) = 0) : Filter.EventuallyEq (MeasureTheory.ae mu) (MeasureTheory.condExp mcond mu (fun omega : Omega => (((reward omega t - model.mean b : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Shifted-history specialization of `centeredReward_condExp_eq_zero_of_indep`. This is the first compiled conditional mean-zero source for the fixed-commit ETC history filtration. It still assumes the centered reward coordinate is independent of the shifted generated history sigma-algebra and has integral zero; later product-law work should discharge those two assumptions.

theorem centeredReward_condExp_historyFiltrationSucc_eq_zero_of_indep {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega t)) (b : Fin K) (t : Nat) (h_indep : ProbabilityTheory.Indep (MeasurableSpace.comap (fun omega : Omega => (((reward omega t - model.mean b : Rat) : Real))) inferInstance) (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) mu) (h_integral : MeasureTheory.integral mu (fun omega : Omega => (((reward omega t - model.mean b : Rat) : Real))) = 0) : Filter.EventuallyEq (MeasureTheory.ae mu) (MeasureTheory.condExp (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) mu (fun omega : Omega => (((reward omega t - model.mean b : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Future centered reward coordinates are independent of the reward-only past sigma-algebra generated by earlier coordinates, provided the reward trace coordinates are mutually independent. This is a product-law/history-independence bridge for the conditional mean-zero route. It deliberately targets only the reward-coordinate past `iSup`; adding the deterministic action generators from the local history filtration is a separate wrapper.

theorem indep_centeredReward_succ_pastReward_iSup_of_iIndepFun_reward {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) (model : FiniteBanditModel K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega t)) (h_reward_indep : ProbabilityTheory.iIndepFun (fun t omega => reward omega t) mu) (b : Fin K) (i : Nat) : ProbabilityTheory.Indep (MeasurableSpace.comap (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real))) inferInstance) (iSup fun j : Nat => iSup fun _h : j <= i => MeasurableSpace.comap (fun omega : Omega => reward omega j) inferInstance) mu

For a fixed-commit ETC action trace, the shifted generated history filtration is contained in the reward-only past sigma-algebra. The action generators are deterministic singleton preimages, hence either `univ` or `empty`; the reward generators at filtration level `i` are exactly coordinates `j <= i`. This is the missing deterministic-action bridge from the reward-only past independence leaf to the local `History.historyFiltrationSucc`.

theorem historyFiltrationSucc_actionWithCommit_le_pastReward_iSup {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] (spec : ETC.Spec K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega t)) (i : Nat) : (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward i : MeasurableSpace Omega) <= (iSup fun j : Nat => iSup fun _h : j <= i => MeasurableSpace.comap (fun omega : Omega => reward omega j) inferInstance)

Future centered reward coordinates are independent of the full fixed-commit shifted history filtration when reward coordinates are mutually independent. This extends `indep_centeredReward_succ_pastReward_iSup_of_iIndepFun_reward` from the reward-only past to `History.historyFiltrationSucc` by the deterministic action-generator inclusion above.

theorem indep_centeredReward_succ_historyFiltrationSucc_of_iIndepFun_reward {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega t)) (h_reward_indep : ProbabilityTheory.iIndepFun (fun t omega => reward omega t) mu) (b : Fin K) (i : Nat) : ProbabilityTheory.Indep (MeasurableSpace.comap (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real))) inferInstance) (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward i) mu

One-step conditional mean-zero wrapper for Mathlib's conditional tail API. Mathlib asks for the summand at `i + 1` to be conditionally controlled against filtration level `i`. This theorem specializes the generic independence-based conditional expectation wrapper to that index shape.

theorem centeredReward_succ_condExp_historyFiltrationSucc_eq_zero_of_indep {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega t)) (b : Fin K) (i : Nat) (h_indep : ProbabilityTheory.Indep (MeasurableSpace.comap (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real))) inferInstance) (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward i) mu) (h_integral : MeasureTheory.integral mu (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real))) = 0) : Filter.EventuallyEq (MeasureTheory.ae mu) (MeasureTheory.condExp (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward i) mu (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

One-step conditional mean-zero source from reward-coordinate independence. This combines the full fixed-commit history independence theorem with the existing `condExp_indep_eq` wrapper. It still leaves the zero-integral identity as an explicit side condition, supplied separately by exact-mean or bounded source leaves.

theorem centeredReward_succ_condExp_historyFiltrationSucc_eq_zero_of_iIndepFun_reward {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega t)) (h_reward_indep : ProbabilityTheory.iIndepFun (fun t omega => reward omega t) mu) (b : Fin K) (i : Nat) (h_integral : MeasureTheory.integral mu (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real))) = 0) : Filter.EventuallyEq (MeasureTheory.ae mu) (MeasureTheory.condExp (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward i) mu (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Unconditional sub-Gaussianity plus independence from the conditioning sigma-algebra gives conditional sub-Gaussianity. This is a Mathlib-shaped source for later sampled reward-law witnesses. It uses `Kernel.HasSubgaussianMGF.of_rat`: for each rational exponent the conditional MGF is the unconditional MGF by `condExp_indep_eq`, and Mathlib extends the bound to all real exponents by continuity/density.

theorem hasCondSubgaussianMGF_of_indep_comap {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (X : Omega -> Real) (c : NNReal) (hmeasX : @Measurable Omega Real mOmega inferInstance X) (h_subG : ProbabilityTheory.HasSubgaussianMGF X c mu) (h_indep : ProbabilityTheory.Indep (MeasurableSpace.comap X inferInstance) mcond mu) : ProbabilityTheory.HasCondSubgaussianMGF mcond hm X c mu

One-step conditional sub-Gaussian source from reward-coordinate independence. This is the sampled centered-reward MGF analogue of `centeredReward_succ_condExp_historyFiltrationSucc_eq_zero_of_iIndepFun_reward`: unconditional sub-Gaussianity of the future centered reward, together with `iIndepFun` reward coordinates, gives the conditional MGF witness against the fixed-commit shifted history filtration.

theorem centeredReward_succ_hasCondSubgaussianMGF_historyFiltrationSucc_of_iIndepFun_reward {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega t)) (h_reward_indep : ProbabilityTheory.iIndepFun (fun t omega => reward omega t) mu) (b : Fin K) (i : Nat) (c : NNReal) (h_subG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real))) c mu) : ProbabilityTheory.HasCondSubgaussianMGF (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward i) ((History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward).le i) (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real))) c mu

If the fixed ETC trace at time `t` pulls neither arm `a` nor the selected best arm, the centered pairwise reward-difference summand is identically zero and therefore has a zero-variance sub-Gaussian MGF. This is a small reward-law source for the independent/zeroth MGF side only; it does not cover the sampled-arm times where the reward coordinate appears.

theorem centeredPairwiseRewardDiff_hasSubgaussianMGF_of_action_miss {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsZeroOrProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (a : Fin K) (t : Nat) (h_ne_a : ETC.actionWithCommit spec commitArm t ≠ a) (h_ne_best : ETC.actionWithCommit spec commitArm t ≠ model.bestArm) : ProbabilityTheory.HasSubgaussianMGF (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega) 0 mu

If the fixed ETC trace at time `t` pulls neither arm `a` nor the selected best arm, the centered pairwise reward-difference summand is conditionally sub-Gaussian with zero variance proxy with respect to any sub-sigma-algebra. This discharges only the zero summand cases of the conditional MGF field.

theorem centeredPairwiseRewardDiff_hasCondSubgaussianMGF_of_action_miss {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (m : MeasurableSpace Omega) (hm : m ≤ mOmega) (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (a : Fin K) (t : Nat) (h_ne_a : ETC.actionWithCommit spec commitArm t ≠ a) (h_ne_best : ETC.actionWithCommit spec commitArm t ≠ model.bestArm) : ProbabilityTheory.HasCondSubgaussianMGF m hm (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega) 0 mu

History-filtration specialization of the zero-summand conditional MGF source. For conditional concentration over the shifted generated history filtration, the summand at process time `t` is conditionally sub-Gaussian with zero variance whenever `actionWithCommit t` is neither the comparison arm nor the best arm.

theorem centeredPairwiseRewardDiff_hasCondSubgaussianMGF_historyFiltrationSucc_of_action_miss {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (a : Fin K) (t : Nat) (h_ne_a : ETC.actionWithCommit spec commitArm t ≠ a) (h_ne_best : ETC.actionWithCommit spec commitArm t ≠ model.bestArm) : ProbabilityTheory.HasCondSubgaussianMGF (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) ((History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward).le t) (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega) 0 mu

Sampled comparison-arm conditional MGF transfer. When the fixed ETC trace pulls the comparison arm `a` at time `t`, the centered pairwise reward-difference summand is exactly the centered reward `reward t - mean a`, so any conditional MGF witness for that centered reward transfers to the pairwise summand.

theorem centeredPairwiseRewardDiff_hasCondSubgaussianMGF_of_action_eq_arm {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (m : MeasurableSpace Omega) (hm : m ≤ mOmega) (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (a : Fin K) (t : Nat) (c : NNReal) (hne : a = model.bestArm -> False) (h_action : ETC.actionWithCommit spec commitArm t = a) (h_subG : ProbabilityTheory.HasCondSubgaussianMGF m hm (fun omega : Omega => (((reward omega t - model.mean a : Rat) : Real))) c mu) : ProbabilityTheory.HasCondSubgaussianMGF m hm (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega) c mu

Sampled best-arm conditional MGF transfer. When the fixed ETC trace pulls `model.bestArm` at time `t`, the centered pairwise reward-difference summand is the negative centered best-arm reward `mean bestArm - reward t`. This theorem consumes that negative-direction conditional MGF witness explicitly.

theorem centeredPairwiseRewardDiff_hasCondSubgaussianMGF_of_action_eq_bestArm {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (m : MeasurableSpace Omega) (hm : m ≤ mOmega) (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (a : Fin K) (t : Nat) (c : NNReal) (hne : a = model.bestArm -> False) (h_action : ETC.actionWithCommit spec commitArm t = model.bestArm) (h_subG : ProbabilityTheory.HasCondSubgaussianMGF m hm (fun omega : Omega => (((model.mean model.bestArm - reward omega t : Rat) : Real))) c mu) : ProbabilityTheory.HasCondSubgaussianMGF m hm (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega) c mu

Shifted-history specialization of the sampled comparison-arm conditional MGF transfer.

theorem centeredPairwiseRewardDiff_hasCondSubgaussianMGF_historyFiltrationSucc_of_action_eq_arm {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (a : Fin K) (t : Nat) (c : NNReal) (hne : a = model.bestArm -> False) (h_action : ETC.actionWithCommit spec commitArm t = a) (h_subG : ProbabilityTheory.HasCondSubgaussianMGF (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) ((History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward).le t) (fun omega : Omega => (((reward omega t - model.mean a : Rat) : Real))) c mu) : ProbabilityTheory.HasCondSubgaussianMGF (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) ((History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward).le t) (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega) c mu

Shifted-history specialization of the sampled best-arm conditional MGF transfer.

theorem centeredPairwiseRewardDiff_hasCondSubgaussianMGF_historyFiltrationSucc_of_action_eq_bestArm {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (a : Fin K) (t : Nat) (c : NNReal) (hne : a = model.bestArm -> False) (h_action : ETC.actionWithCommit spec commitArm t = model.bestArm) (h_subG : ProbabilityTheory.HasCondSubgaussianMGF (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) ((History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward).le t) (fun omega : Omega => (((model.mean model.bestArm - reward omega t : Rat) : Real))) c mu) : ProbabilityTheory.HasCondSubgaussianMGF (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) ((History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward).le t) (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega) c mu

Action-case assembly for sampled centered-reward conditional MGF witnesses. This is the conditional analogue of `ETC.centeredPairwiseRewardDiff_hasSubgaussianMGF_of_centeredReward`: if the reward coordinate pulled by the fixed ETC trace has the appropriate centered conditional MGF witness, then the concrete centered pairwise reward-difference summand has the corresponding action-selected variance proxy. The miss case is closed by the zero-summand theorem, and the best-arm case uses the sign-flipped conditional MGF witness.

theorem centeredPairwiseRewardDiff_hasCondSubgaussianMGF_of_centeredReward {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (m : MeasurableSpace Omega) (hm : m ≤ mOmega) (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (cReward : Fin K -> Nat -> NNReal) (a : Fin K) (t : Nat) (hne : a = model.bestArm -> False) (h_subG : forall b : Fin K, ETC.actionWithCommit spec commitArm t = b -> ProbabilityTheory.HasCondSubgaussianMGF m hm (fun omega : Omega => (((reward omega t - model.mean b : Rat) : Real))) (cReward b t) mu) : ProbabilityTheory.HasCondSubgaussianMGF m hm (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega) (ETC.centeredPairwiseRewardDiffVarianceProxy spec model commitArm cReward a t) mu

Shifted-history specialization of the action-case conditional MGF assembly from sampled centered-reward witnesses.

theorem centeredPairwiseRewardDiff_hasCondSubgaussianMGF_historyFiltrationSucc_of_centeredReward {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (cReward : Fin K -> Nat -> NNReal) (a : Fin K) (t : Nat) (hne : a = model.bestArm -> False) (h_subG : forall b : Fin K, ETC.actionWithCommit spec commitArm t = b -> ProbabilityTheory.HasCondSubgaussianMGF (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) ((History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward).le t) (fun omega : Omega => (((reward omega t - model.mean b : Rat) : Real))) (cReward b t) mu) : ProbabilityTheory.HasCondSubgaussianMGF (History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward t) ((History.historyFiltrationSucc (fun _omega : Omega => ETC.actionWithCommit spec commitArm) reward (fun _t : Nat => measurable_const) hreward).le t) (fun omega => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega) (ETC.centeredPairwiseRewardDiffVarianceProxy spec model commitArm cReward a t) mu

Reward-level conditional sub-Gaussian source contract for the fixed-commit ETC centered-diff route. This contract is one layer closer to a concrete reward law than `CenteredDiffCondSubGaussianWitnesses`: it asks for conditional MGF witnesses for the sampled reward coordinate centered at the arm actually pulled by `actionWithCommit`, plus the zeroth unconditional witness and the final tail budget. The constructor below turns it into the centered-diff witness package.

structure CenteredRewardCondSubGaussianWitnesses {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] [MeasureTheory.IsZeroOrProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (tail : Fin K -> ENNReal) where

Witness package for the concrete centered reward-difference conditional sub-Gaussian ETC tail route. This is a project-local conditional reward-law surface: it records the filtration, strong adaptedness, zeroth unconditional MGF witness, later conditional MGF witnesses, and tail domination needed to produce the fixed ETC pairwise empirical-mean tail contract.

structure CenteredDiffCondSubGaussianWitnesses {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] [MeasureTheory.IsZeroOrProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (tail : Fin K -> ENNReal) where

Build the centered-diff conditional witness package from reward-level sampled conditional MGF witnesses. This bridges the remaining action-case gap between raw reward-law conditional MGF facts and the already compiled centered-diff conditional tail consumer.

noncomputable def centeredDiffCondSubGaussianWitnesses_of_centeredRewardCondSubGaussianWitnesses {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] [MeasureTheory.IsZeroOrProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (tail : Fin K -> ENNReal) (w : ETC.CenteredRewardCondSubGaussianWitnesses mu spec model commitArm reward tail) : ETC.CenteredDiffCondSubGaussianWitnesses mu spec model commitArm reward tail where

Consume a centered reward-difference conditional witness package to build the fixed-commit ETC pairwise empirical-mean tail contract. This is the first compiled conditional reward-law bridge for the ETC route. It uses the generated centered-diff event inclusion plus the Mathlib-backed conditional sub-Gaussian finite-prefix wrapper, while keeping the actual conditional MGF and adaptedness facts explicit in the witness package.

theorem pairwiseEmpMeanTailContract_of_centeredDiffCondSubGaussianWitnesses {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] [MeasureTheory.IsZeroOrProbabilityMeasure mu] (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (tail : Fin K -> ENNReal) (hexplorationPulls_pos : 0 < spec.explorationPulls) (w : ETC.CenteredDiffCondSubGaussianWitnesses mu spec model commitArm reward tail) : ETC.PairwiseEmpMeanTailContract mu spec model commitArm reward tail