Lean module · EXP3
BanditRLProof.Exp3ActionProcess
This module constructs a history-adaptive finite-action Markov kernel from measurable probability coordinates. Its canonical sample measure is the history law composed with that kernel, so the sampled action has the requested conditional distribution by Mathlib's condDistrib/compProd uniqueness theorem. The final wrappers discharge the law premises of the one-round EXP3 importance-weighted moment transport.
Module map
Imports
BanditRLProof.Exp3ConditionalMoments
Imported by
BanditRLProof, BanditRLProof.Exp3ScoreRegularity, BanditRLProof.TsallisFTRLConditionalStability
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.Exp3.MeasurableFiniteActionDistribution
Compiled
Pointwise probability-vector and coordinate-measurability contracts.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.MeasurableFiniteActionDistributionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure MeasurableFiniteActionDistribution {History : Type u} {Action : Type v} [MeasurableSpace History] (arms : Finset Action) (prob : History -> Action -> Real) : Prop where
def
BanditRLProof.Exp3.finiteActionKernel
Compiled
The history-adaptive finite action kernel generated by `prob`.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.finiteActionKernelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def finiteActionKernel {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] (arms : Finset Action) (prob : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) : Kernel History Action where
theorem
BanditRLProof.Exp3.finiteActionKernel_apply
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.finiteActionKernel_applyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem finiteActionKernel_apply {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] (arms : Finset Action) (prob : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (history : History) : finiteActionKernel arms prob source history = finiteActionMeasure arms (prob history)
def
BanditRLProof.Exp3.actionProcessMeasure
Compiled
Canonical joint history/action law generated by the adaptive policy.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcessMeasureReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def actionProcessMeasure {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) : Measure (History × Action)
def
BanditRLProof.Exp3.actionProcessHistory
Compiled
History coordinate of the generated one-round process.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcessHistoryReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def actionProcessHistory {History Action : Type*} : History × Action -> History
def
BanditRLProof.Exp3.actionProcessAction
Compiled
Sampled action coordinate of the generated one-round process.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcessActionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def actionProcessAction {History Action : Type*} : History × Action -> Action
theorem
BanditRLProof.Exp3.actionProcessHistory_measurable
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcessHistory_measurableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem actionProcessHistory_measurable {History Action : Type*} [MeasurableSpace History] [MeasurableSpace Action] : Measurable (@actionProcessHistory History Action)
theorem
BanditRLProof.Exp3.actionProcessAction_measurable
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcessAction_measurableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem actionProcessAction_measurable {History Action : Type*} [MeasurableSpace History] [MeasurableSpace Action] : Measurable (@actionProcessAction History Action)
theorem
BanditRLProof.Exp3.actionProcess_history_map_eq
Compiled
The generated process preserves the supplied history marginal.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcess_history_map_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem actionProcess_history_map_eq {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) : (actionProcessMeasure historyMu arms prob source).map actionProcessHistory = historyMu
theorem
BanditRLProof.Exp3.actionProcess_condDistrib_action_ae_eq_finiteActionKernel
Compiled
The sampled action has the generated policy as its a.e. conditional law.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcess_condDistrib_action_ae_eq_finiteActionKernelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem actionProcess_condDistrib_action_ae_eq_finiteActionKernel {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) : condDistrib actionProcessAction actionProcessHistory (actionProcessMeasure historyMu arms prob source) =ᵐ[ (actionProcessMeasure historyMu arms prob source).map actionProcessHistory] finiteActionKernel arms prob source
theorem
BanditRLProof.Exp3.finiteActionKernel_ae_eq_finiteActionMeasure
Compiled
The generated policy is pointwise the explicit finite Dirac action law.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.finiteActionKernel_ae_eq_finiteActionMeasureReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem finiteActionKernel_ae_eq_finiteActionMeasure {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] (historyMu : Measure History) (arms : Finset Action) (prob : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) : finiteActionKernel arms prob source =ᵐ[historyMu] fun history => finiteActionMeasure arms (prob history)
theorem
BanditRLProof.Exp3.actionProcess_integral_importanceWeightedLoss_eq_integral_loss
Compiled
Canonical generated-process armwise importance-weighted identity.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcess_integral_importanceWeightedLoss_eq_integral_lossReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem actionProcess_integral_importanceWeightedLoss_eq_integral_loss {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (hprob : forall history action, action ∈ arms -> 0 < prob history action) (comparator : Action) (hcomparator : comparator ∈ arms) (hscore : Measurable (fun z : History × Action => importanceWeightedLoss (prob z.1) (loss z.1) z.2 comparator)) (hIntegrable : Integrable (fun z : History × Action => importanceWeightedLoss (prob z.1) (loss z.1) z.2 comparator) (historyMu ⊗ₘ finiteActionKernel arms prob source)) : integral (actionProcessMeasure historyMu arms prob source) (fun sample => importanceWeightedLoss (prob (actionProcessHistory sample)) (loss (actionProcessHistory sample)) (actionProcessAction sample) comparator) = integral historyMu (fun history => loss history comparator)
theorem
BanditRLProof.Exp3.actionProcess_integral_mixedImportanceWeightedLoss_eq_integral_mixedLoss
Compiled
Canonical generated-process mixed first-moment identity.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcess_integral_mixedImportanceWeightedLoss_eq_integral_mixedLossReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem actionProcess_integral_mixedImportanceWeightedLoss_eq_integral_mixedLoss {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (hprob : forall history action, action ∈ arms -> 0 < prob history action) (hscore : Measurable (fun z : History × Action => mixedImportanceWeightedLoss arms (prob z.1) (loss z.1) z.2)) (hIntegrable : Integrable (fun z : History × Action => mixedImportanceWeightedLoss arms (prob z.1) (loss z.1) z.2) (historyMu ⊗ₘ finiteActionKernel arms prob source)) : integral (actionProcessMeasure historyMu arms prob source) (fun sample => mixedImportanceWeightedLoss arms (prob (actionProcessHistory sample)) (loss (actionProcessHistory sample)) (actionProcessAction sample)) = integral historyMu (fun history => arms.sum (fun action => prob history action * loss history action))
theorem
BanditRLProof.Exp3.actionProcess_integral_mixedSquaredImportanceWeightedLoss_eq_integral_sum_loss_sq
Compiled
Canonical generated-process mixed second-moment identity.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.actionProcess_integral_mixedSquaredImportanceWeightedLoss_eq_integral_sum_loss_sqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem actionProcess_integral_mixedSquaredImportanceWeightedLoss_eq_integral_sum_loss_sq {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (hprob : forall history action, action ∈ arms -> 0 < prob history action) (hscore : Measurable (fun z : History × Action => mixedSquaredImportanceWeightedLoss arms (prob z.1) (loss z.1) z.2)) (hIntegrable : Integrable (fun z : History × Action => mixedSquaredImportanceWeightedLoss arms (prob z.1) (loss z.1) z.2) (historyMu ⊗ₘ finiteActionKernel arms prob source)) : integral (actionProcessMeasure historyMu arms prob source) (fun sample => mixedSquaredImportanceWeightedLoss arms (prob (actionProcessHistory sample)) (loss (actionProcessHistory sample)) (actionProcessAction sample)) = integral historyMu (fun history => arms.sum (fun action => (loss history action) ^ 2))