Lean module · Frontier
BanditRLProof.Algorithms.StochasticGradientBanditTwoArmFixedIID
This module realizes the reward model used by the two-arm source theorem from an arm-indexed family of fixed probability laws. The environment is the stationary history environment over Unit; hence its initial and successor reward fibers are exactly the selected arm law and cannot reveal a latent, changing environment.
Module map
Imports
BanditRLProof.Algorithms.StochasticGradientBanditTwoArmPathIntegrability, BanditRLProof.Algorithms.ThompsonStationaryReward, BanditRLProof.Algorithms.UCBArmStreamFiniteArmRewardLaws
Imported by
BanditRLProof, BanditRLProof.Algorithms.StochasticGradientBanditTwoArmTheoremOne
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.StochasticGradientBandit.twoArmFixedIIDRewardKernel
Compiled
The fixed two-arm reward kernel, with a trivial environment coordinate added for the measurable-history-environment interface.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.twoArmFixedIIDRewardKernelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def twoArmFixedIIDRewardKernel (armLaw : Fin 2 -> Measure Real) : Kernel (Unit × Fin 2) Real
theorem
BanditRLProof.StochasticGradientBandit.twoArmFixedIIDRewardKernel_apply
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.twoArmFixedIIDRewardKernel_applyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem twoArmFixedIIDRewardKernel_apply (armLaw : Fin 2 -> Measure Real) (env : Unit) (arm : Fin 2) : twoArmFixedIIDRewardKernel armLaw (env, arm) = armLaw arm
theorem
BanditRLProof.StochasticGradientBandit.twoArmFixedIIDRewardKernel_isMarkov
Compiled
Pointwise probability laws make the fixed two-arm kernel Markov.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.twoArmFixedIIDRewardKernel_isMarkovReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem twoArmFixedIIDRewardKernel_isMarkov (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) : IsMarkovKernel (twoArmFixedIIDRewardKernel armLaw)
def
BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment
Compiled
The fixed-IID source environment. Conditional on the selected arm, every round uses the same arm law and ignores the observed history.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironmentReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def twoArmFixedIIDEnvironment (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) : Thompson.MeasurableHistoryEnvironment Unit (Fin 2) Real
theorem
BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_initialFeedback_apply
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_initialFeedback_applyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem twoArmFixedIIDEnvironment_initialFeedback_apply (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (env : Unit) (arm : Fin 2) : (twoArmFixedIIDEnvironment armLaw hprob).initialFeedback (env, arm) = armLaw arm
theorem
BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_feedback_apply
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_feedback_applyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem twoArmFixedIIDEnvironment_feedback_apply (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (n : Nat) (env : Unit) (history : History.FinitePairHistory (Fin 2) Real n) (arm : Fin 2) : (twoArmFixedIIDEnvironment armLaw hprob).feedback n (env, (history, arm)) = armLaw arm
theorem
BanditRLProof.StochasticGradientBandit.twoArmFixedIIDReward_aestronglyMeasurable
Compiled
Real-valued rewards need no extra measurability assumption beyond their law.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.twoArmFixedIIDReward_aestronglyMeasurableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem twoArmFixedIIDReward_aestronglyMeasurable (armLaw : Fin 2 -> Measure Real) (arm : Fin 2) : AEStronglyMeasurable (fun reward : Real => reward) (armLaw arm)
theorem
BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_contract
Compiled
Fixed probability laws supported on `[-1,1]` with the stated arm means produce the uniform bounded fixed-mean contract used by the compiled two-arm recurrences.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_contractReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem twoArmFixedIIDEnvironment_contract (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (mean : Fin 2 -> Real) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, |reward| <= 1) (hmean : forall arm, integral (armLaw arm) id = mean arm) : TwoArmBoundedFixedMeanEnvironmentContract (twoArmFixedIIDEnvironment armLaw hprob) mean
theorem
BanditRLProof.StochasticGradientBandit.integral_twoArmFixedIIDHistoryStepKernel_sourceIncrement_eq_gapCoordinate
Compiled
Equation (5) on every generated fixed-IID successor history, with the source-increment integrability premise discharged from the fixed reward-law support. This remains a one-step conditional-kernel identity; it does not perform a global tower iteration.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.StochasticGradientBandit.integral_twoArmFixedIIDHistoryStepKernel_sourceIncrement_eq_gapCoordinateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_twoArmFixedIIDHistoryStepKernel_sourceIncrement_eq_gapCoordinate (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (mean : Fin 2 -> Real) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, |reward| <= 1) (hmean : forall arm, integral (armLaw arm) id = mean arm) (initialTheta : Fin 2 -> Real) (eta : Real) (n : Nat) (history : History.FinitePairHistory (Fin 2) Real n) (gap : Fin 2 -> Real) (bestMean : Real) (coordinate : Fin 2) (hgap : forall action, gap action = bestMean - mean action) : integral (Thompson.measurableEnvironmentHistoryStepKernel (historyAlgorithm initialTheta eta) (twoArmFixedIIDEnvironment armLaw hprob) n ((), history)) (fun pair : Fin 2 × Real => sourceIncrement (softmaxProbability (historyParameter initialTheta eta n history)) pair.2 pair.1 coordinate) = softmaxProbability (historyParameter initialTheta eta n history) coordinate * (instantaneousGap (softmaxProbability (historyParameter initialTheta eta n history)) gap - gap coordinate)