BanditRLProof.Algorithms.StochasticGradientBanditConditionalExponentialAudit

Action-dependent Equation (8) for the generated initial action/reward pair. Source-time fence: this kernel samples source round `t = 1` from the untouched parameter `initialTheta`; consuming pair zero then constructs source `theta_2`. In the source Theorem 1, `initialTheta` is the zero vector. This base bridge is therefore separate from the successor bridge below.

theorem integral_measurableEnvironmentInitialPairKernel_exp_actionReward_le_sourceEqEight_of_mean {Env : Type v} [MeasurableSpace Env] (initialTheta : Action -> Real) (eta : Real) (environment : Thompson.MeasurableHistoryEnvironment Env Action Real) (env : Env) (q mean : Action -> Real) (hreward : forall selected, ∀ᵐ reward ∂environment.initialFeedback (env, selected), |reward| <= 1) (hmean : forall selected, integral (environment.initialFeedback (env, selected)) id = mean selected) : integral (Thompson.measurableEnvironmentInitialPairKernel (historyAlgorithm initialTheta eta) environment env) (fun pair : Action × Real => Real.exp (q pair.1 * pair.2)) <= 1 + ∑ selected, softmaxProbability initialTheta selected * (q selected * mean selected + q selected ^ 2 / 2 * sourceC (|q selected| / 2))

Action-dependent Equation (8) under the actual generated SGB history-step kernel. The real reward coordinate is measurable by construction, so the only reward-law premise needed beyond the Markov-kernel contract is its almost-sure source support in `[-1, 1]`. Source-time fence: `historyParameter initialTheta eta n history` has already consumed trace pairs `0, ..., n`, so it is source `theta_{n+2}`. This successor kernel samples source round `n+2`; consuming its new pair produces `theta_{n+3}`. Consequently it does not replace the initial-pair bridge above when assembling a recurrence that begins at source `t = 1`. For the later `Fin 2` consumer with best-arm probability `p`, the positive recurrence instantiates this generic coefficient by `q 0 = 2 * eta * (1 - p)` and `q 1 = -2 * eta * p`; the inverse-odds recurrence uses the pointwise negation. Those recurrence simplifications are deliberately left to the next layer.

theorem integral_historyStepKernel_exp_actionReward_le_sourceEqEight (initialTheta : Action -> Real) (eta : Real) (environment : Thompson.HistoryEnvironment Action Real) (n : Nat) (history : History.FinitePairHistory Action Real n) (q : Action -> Real) (hreward : forall selected, ∀ᵐ reward ∂environment.feedback n (history, selected), |reward| <= 1) : integral (Thompson.historyStepKernel (historyAlgorithm initialTheta eta) environment n history) (fun pair : Action × Real => Real.exp (q pair.1 * pair.2)) <= 1 + ∑ selected, softmaxProbability (historyParameter initialTheta eta n history) selected * (q selected * integral (environment.feedback n (history, selected)) id + q selected ^ 2 / 2 * sourceC (|q selected| / 2))

Mean-surface form of the generated action-dependent Equation-(8) bound.

theorem integral_historyStepKernel_exp_actionReward_le_sourceEqEight_of_mean (initialTheta : Action -> Real) (eta : Real) (environment : Thompson.HistoryEnvironment Action Real) (n : Nat) (history : History.FinitePairHistory Action Real n) (q mean : Action -> Real) (hreward : forall selected, ∀ᵐ reward ∂environment.feedback n (history, selected), |reward| <= 1) (hmean : forall selected, integral (environment.feedback n (history, selected)) id = mean selected) : integral (Thompson.historyStepKernel (historyAlgorithm initialTheta eta) environment n history) (fun pair : Action × Real => Real.exp (q pair.1 * pair.2)) <= 1 + ∑ selected, softmaxProbability (historyParameter initialTheta eta n history) selected * (q selected * mean selected + q selected ^ 2 / 2 * sourceC (|q selected| / 2))

Environment-indexed wrapper over the jointly measurable feedback kernel used by the canonical generated trajectory.

theorem integral_measurableEnvironmentHistoryStepKernel_exp_actionReward_le_sourceEqEight_of_mean {Env : Type v} [MeasurableSpace Env] (initialTheta : Action -> Real) (eta : Real) (environment : Thompson.MeasurableHistoryEnvironment Env Action Real) (n : Nat) (env : Env) (history : History.FinitePairHistory Action Real n) (q mean : Action -> Real) (hreward : forall selected, ∀ᵐ reward ∂environment.feedback n (env, (history, selected)), |reward| <= 1) (hmean : forall selected, integral (environment.feedback n (env, (history, selected))) id = mean selected) : integral (Thompson.measurableEnvironmentHistoryStepKernel (historyAlgorithm initialTheta eta) environment n (env, history)) (fun pair : Action × Real => Real.exp (q pair.1 * pair.2)) <= 1 + ∑ selected, softmaxProbability (historyParameter initialTheta eta n history) selected * (q selected * mean selected + q selected ^ 2 / 2 * sourceC (|q selected| / 2))