Lean module · Frontier
BanditRLProof.Algorithms.StochasticGradientBanditTwoArmInitialRecurrence
This module closes the source-round t = 1 base case for the two exponential recurrences used in Theorem 1 of Baudry--Johnson--Vary--Pike-Burke--Rebeschini (NeurIPS 2025). The generated initial pair kernel samples from the untouched source parameter theta_1 = 0, hence its action law is uniform on Fin 2; consuming that pair produces theta_2.
Module map
Imports
BanditRLProof.Algorithms.StochasticGradientBanditTwoArmRecurrence
Imported by
BanditRLProof, BanditRLProof.Algorithms.StochasticGradientBanditTwoArmPathIntegrability
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.StochasticGradientBandit.softmaxProbability_zeroInitialization_finTwo
Compiled
Zero initialization gives the exact source probability `p_1 = 1 / 2` on both arms.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.softmaxProbability_zeroInitialization_finTwoReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem softmaxProbability_zeroInitialization_finTwo (selected : Fin 2) : softmaxProbability (fun _ : Fin 2 => 0) selected = (1 : Real) / 2
theorem
BanditRLProof.StochasticGradientBandit.integral_twoArmInitialPairKernel_exp_forwardIncrement_le
Compiled
Source-round `t = 1` forward exponential base recurrence. The left side is `E[exp(2 * theta_{1,2})]`, because `theta_{1,1} = 0` and the initial pair contributes exactly `eta * sourceIncrement`.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.integral_twoArmInitialPairKernel_exp_forwardIncrement_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_twoArmInitialPairKernel_exp_forwardIncrement_le {Env : Type v} [MeasurableSpace Env] (eta Delta : Real) (heta : 0 <= eta) (environment : Thompson.MeasurableHistoryEnvironment Env (Fin 2) Real) (env : Env) (mean : Fin 2 -> Real) (hreward : forall selected, ∀ᵐ reward ∂environment.initialFeedback (env, selected), |reward| <= 1) (hmean : forall selected, integral (environment.initialFeedback (env, selected)) id = mean selected) (hgap : mean 0 - mean 1 = Delta) : integral (Thompson.measurableEnvironmentInitialPairKernel (historyAlgorithm (fun _ : Fin 2 => 0) eta) environment env) (fun pair : Fin 2 × Real => Real.exp (2 * eta * sourceIncrement (fun _ : Fin 2 => (1 : Real) / 2) pair.2 pair.1 0)) <= 1 + (eta * Delta + eta ^ 2 * sourceC eta) / 2
theorem
BanditRLProof.StochasticGradientBandit.integral_twoArmInitialPairKernel_exp_inverseIncrement_le
Compiled
Source-round `t = 1` inverse exponential base recurrence. This is the initial value of the inverse-odds potential used to telescope the expected squared failure mass.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.integral_twoArmInitialPairKernel_exp_inverseIncrement_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_twoArmInitialPairKernel_exp_inverseIncrement_le {Env : Type v} [MeasurableSpace Env] (eta Delta : Real) (heta : 0 <= eta) (environment : Thompson.MeasurableHistoryEnvironment Env (Fin 2) Real) (env : Env) (mean : Fin 2 -> Real) (hreward : forall selected, ∀ᵐ reward ∂environment.initialFeedback (env, selected), |reward| <= 1) (hmean : forall selected, integral (environment.initialFeedback (env, selected)) id = mean selected) (hgap : mean 0 - mean 1 = Delta) : integral (Thompson.measurableEnvironmentInitialPairKernel (historyAlgorithm (fun _ : Fin 2 => 0) eta) environment env) (fun pair : Fin 2 × Real => Real.exp (-2 * eta * sourceIncrement (fun _ : Fin 2 => (1 : Real) / 2) pair.2 pair.1 0)) <= 1 - eta / 2 * (Delta - eta * sourceC eta)