Lean module · EXP3

BanditRLProof.Exp3ScoreRegularity

# Regularity of one-round EXP3 importance-weighted scores This module discharges the measurable-score and integrability premises of the generated one-round EXP3 action process. A uniform positive probability floor and measurable losses in `[0, 1]` give explicit pointwise bounds for the armwise, mixed first-moment, and mixed second-moment scores.

Module map

Source: BanditRLProof/Exp3ScoreRegularity.lean
Teaching chapter: 7. EXP3 and adversarial concentration
Declarations: 20
Placeholders: 0

Imports

BanditRLProof.Exp3ActionProcess

Imported by

BanditRLProof, BanditRLProof.Exp3RecursiveTrajectory

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

structure BanditRLProof.Exp3.BoundedMeasurableLossWithProbabilityFloor Compiled

Measurable bounded losses and a uniform exploration floor on the finite support.

structure BoundedMeasurableLossWithProbabilityFloor {History : Type u} {Action : Type v} [MeasurableSpace History] (arms : Finset Action) (prob loss : History -> Action -> Real) (epsilon : Real) : Prop where

Source line 20 Chapter context: EXP3

theorem BanditRLProof.Exp3.BoundedMeasurableLossWithProbabilityFloor.prob_pos Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem BoundedMeasurableLossWithProbabilityFloor.prob_pos {History : Type u} {Action : Type v} [MeasurableSpace History] {arms : Finset Action} {prob loss : History -> Action -> Real} {epsilon : Real} (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (history : History) (action : Action) (haction : action ∈ arms) : 0 < prob history action

Source line 33 Chapter context: EXP3

theorem BanditRLProof.Exp3.measurable_importanceWeightedLoss_score Compiled

A fixed-arm importance-weighted score is measurable on history/action pairs.

theorem measurable_importanceWeightedLoss_score {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (action : Action) (haction : action ∈ arms) : Measurable (fun sample : History × Action => importanceWeightedLoss (prob sample.1) (loss sample.1) sample.2 action)

Source line 46 Chapter context: EXP3

theorem BanditRLProof.Exp3.measurable_mixedImportanceWeightedLoss_score Compiled

The probability-mixed first-moment score is measurable.

theorem measurable_mixedImportanceWeightedLoss_score {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : Measurable (fun sample : History × Action => mixedImportanceWeightedLoss arms (prob sample.1) (loss sample.1) sample.2)

Source line 68 Chapter context: EXP3

theorem BanditRLProof.Exp3.measurable_weightedImportanceWeightedLoss_score Compiled

A score mixed by a second measurable finite distribution is measurable.

theorem measurable_weightedImportanceWeightedLoss_score {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob weight loss : History -> Action -> Real) (probSource : MeasurableFiniteActionDistribution arms prob) (weightSource : MeasurableFiniteActionDistribution arms weight) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : Measurable (fun sample : History × Action => weightedImportanceWeightedLoss arms (prob sample.1) (weight sample.1) (loss sample.1) sample.2)

Source line 87 Chapter context: EXP3

theorem BanditRLProof.Exp3.measurable_mixedSquaredImportanceWeightedLoss_score Compiled

The probability-mixed second-moment score is measurable.

theorem measurable_mixedSquaredImportanceWeightedLoss_score {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : Measurable (fun sample : History × Action => mixedSquaredImportanceWeightedLoss arms (prob sample.1) (loss sample.1) sample.2)

Source line 107 Chapter context: EXP3

theorem BanditRLProof.Exp3.norm_importanceWeightedLoss_score_le_inv_floor Compiled

A fixed-arm importance-weighted score is bounded by the reciprocal floor.

theorem norm_importanceWeightedLoss_score_le_inv_floor {History : Type u} {Action : Type v} [MeasurableSpace History] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (history : History) (chosen action : Action) (haction : action ∈ arms) : ‖importanceWeightedLoss (prob history) (loss history) chosen action‖ <= 1 / epsilon

Source line 126 Chapter context: EXP3

theorem BanditRLProof.Exp3.norm_mixedImportanceWeightedLoss_score_le_inv_floor Compiled

The mixed first-moment score is bounded by the reciprocal floor.

theorem norm_mixedImportanceWeightedLoss_score_le_inv_floor {History : Type u} {Action : Type v} [MeasurableSpace History] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (history : History) (chosen : Action) : ‖mixedImportanceWeightedLoss arms (prob history) (loss history) chosen‖ <= 1 / epsilon

Source line 148 Chapter context: EXP3

theorem BanditRLProof.Exp3.norm_weightedImportanceWeightedLoss_score_le_inv_floor Compiled

Mixing by any finite probability vector preserves the reciprocal-floor bound for the importance-weighted score.

theorem norm_weightedImportanceWeightedLoss_score_le_inv_floor {History : Type u} {Action : Type v} [MeasurableSpace History] [DecidableEq Action] (arms : Finset Action) (prob weight loss : History -> Action -> Real) (weightSource : MeasurableFiniteActionDistribution arms weight) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (history : History) (chosen : Action) : ‖weightedImportanceWeightedLoss arms (prob history) (weight history) (loss history) chosen‖ <= 1 / epsilon

Source line 186 Chapter context: EXP3

theorem BanditRLProof.Exp3.norm_mixedSquaredImportanceWeightedLoss_score_le_inv_floor_sq Compiled

The mixed second-moment score is bounded by the square reciprocal floor.

theorem norm_mixedSquaredImportanceWeightedLoss_score_le_inv_floor_sq {History : Type u} {Action : Type v} [MeasurableSpace History] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (history : History) (chosen : Action) : ‖mixedSquaredImportanceWeightedLoss arms (prob history) (loss history) chosen‖ <= (1 / epsilon) ^ 2

Source line 224 Chapter context: EXP3

theorem BanditRLProof.Exp3.integrable_importanceWeightedLoss_score Compiled

The armwise score is integrable under the generated history/action law.

theorem integrable_importanceWeightedLoss_score {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (action : Action) (haction : action ∈ arms) : Integrable (fun sample : History × Action => importanceWeightedLoss (prob sample.1) (loss sample.1) sample.2 action) (Measure.compProd historyMu (finiteActionKernel arms prob source))

Source line 268 Chapter context: EXP3

theorem BanditRLProof.Exp3.integrable_mixedImportanceWeightedLoss_score Compiled

The mixed first-moment score is integrable under the generated law.

theorem integrable_mixedImportanceWeightedLoss_score {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : Integrable (fun sample : History × Action => mixedImportanceWeightedLoss arms (prob sample.1) (loss sample.1) sample.2) (Measure.compProd historyMu (finiteActionKernel arms prob source))

Source line 292 Chapter context: EXP3

theorem BanditRLProof.Exp3.integrable_weightedImportanceWeightedLoss_score Compiled

A predictably weighted importance-weighted score is integrable under the sampling law when both finite distributions are measurable.

theorem integrable_weightedImportanceWeightedLoss_score {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob weight loss : History -> Action -> Real) (probSource : MeasurableFiniteActionDistribution arms prob) (weightSource : MeasurableFiniteActionDistribution arms weight) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : Integrable (fun sample : History × Action => weightedImportanceWeightedLoss arms (prob sample.1) (weight sample.1) (loss sample.1) sample.2) (Measure.compProd historyMu (finiteActionKernel arms prob probSource))

Source line 316 Chapter context: EXP3

theorem BanditRLProof.Exp3.integrable_mixedSquaredImportanceWeightedLoss_score Compiled

The mixed second-moment score is integrable under the generated law.

theorem integrable_mixedSquaredImportanceWeightedLoss_score {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : Integrable (fun sample : History × Action => mixedSquaredImportanceWeightedLoss arms (prob sample.1) (loss sample.1) sample.2) (Measure.compProd historyMu (finiteActionKernel arms prob source))

Source line 340 Chapter context: EXP3

theorem BanditRLProof.Exp3.integrable_importanceWeightedLoss_selected_of_isFiniteMeasure Compiled

A bounded armwise score remains integrable when the sampled action is any measurable function on a finite history measure.

theorem integrable_importanceWeightedLoss_selected_of_isFiniteMeasure {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure History) [IsFiniteMeasure mu] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (chosen : History -> Action) (hchosen : Measurable chosen) (comparator : Action) (hcomparator : comparator ∈ arms) : Integrable (fun history => importanceWeightedLoss (prob history) (loss history) (chosen history) comparator) mu

Source line 364 Chapter context: EXP3

theorem BanditRLProof.Exp3.integrable_weightedImportanceWeightedLoss_selected_of_isFiniteMeasure Compiled

A predictably weighted score remains integrable when the sampled action is an arbitrary measurable function on a finite measure.

theorem integrable_weightedImportanceWeightedLoss_selected_of_isFiniteMeasure {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure History) [IsFiniteMeasure mu] (arms : Finset Action) (prob weight loss : History -> Action -> Real) (probSource : MeasurableFiniteActionDistribution arms prob) (weightSource : MeasurableFiniteActionDistribution arms weight) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (chosen : History -> Action) (hchosen : Measurable chosen) : Integrable (fun history => weightedImportanceWeightedLoss arms (prob history) (weight history) (loss history) (chosen history)) mu

Source line 391 Chapter context: EXP3

theorem BanditRLProof.Exp3.integrable_mixedSquaredImportanceWeightedLoss_selected_of_isFiniteMeasure Compiled

A bounded mixed second-moment score remains integrable when the sampled action is any measurable function on a finite history measure.

theorem integrable_mixedSquaredImportanceWeightedLoss_selected_of_isFiniteMeasure {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure History) [IsFiniteMeasure mu] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : MeasurableFiniteActionDistribution arms prob) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (chosen : History -> Action) (hchosen : Measurable chosen) : Integrable (fun history => mixedSquaredImportanceWeightedLoss arms (prob history) (loss history) (chosen history)) mu

Source line 418 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcess_integral_importanceWeightedLoss_eq_integral_loss_of_regularity Compiled

Canonical armwise identity with score regularity inferred from bounded losses.

theorem actionProcess_integral_importanceWeightedLoss_eq_integral_loss_of_regularity {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) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) (comparator : Action) (hcomparator : comparator ∈ arms) : 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)

Source line 443 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcess_integral_mixedImportanceWeightedLoss_eq_integral_mixedLoss_of_regularity Compiled

Canonical mixed first-moment identity with score regularity inferred.

theorem actionProcess_integral_mixedImportanceWeightedLoss_eq_integral_mixedLoss_of_regularity {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) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : 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))

Source line 470 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcess_integral_mixedSquaredImportanceWeightedLoss_eq_integral_sum_loss_sq_of_regularity Compiled

Canonical mixed second-moment identity with score regularity inferred.

theorem actionProcess_integral_mixedSquaredImportanceWeightedLoss_eq_integral_sum_loss_sq_of_regularity {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) (epsilon : Real) (regularity : BoundedMeasurableLossWithProbabilityFloor arms prob loss epsilon) : 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))

Source line 496 Chapter context: EXP3