Lean module · EXP3

BanditRLProof.Exp3ActionProcess

# A generated one-round EXP3 action process 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

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

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.

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

Source line 22 Chapter context: EXP3

def BanditRLProof.Exp3.finiteActionKernel Compiled

The history-adaptive finite action kernel generated by `prob`.

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

Source line 31 Chapter context: EXP3

theorem BanditRLProof.Exp3.finiteActionKernel_apply Compiled

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

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)

Source line 48 Chapter context: EXP3

def BanditRLProof.Exp3.actionProcessMeasure Compiled

Canonical joint history/action law generated by the adaptive policy.

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)

Source line 72 Chapter context: EXP3

def BanditRLProof.Exp3.actionProcessHistory Compiled

History coordinate of the generated one-round process.

def actionProcessHistory {History Action : Type*} : History × Action -> History

Source line 105 Chapter context: EXP3

def BanditRLProof.Exp3.actionProcessAction Compiled

Sampled action coordinate of the generated one-round process.

def actionProcessAction {History Action : Type*} : History × Action -> Action

Source line 109 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcessHistory_measurable Compiled

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

theorem actionProcessHistory_measurable {History Action : Type*} [MeasurableSpace History] [MeasurableSpace Action] : Measurable (@actionProcessHistory History Action)

Source line 112 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcessAction_measurable Compiled

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

theorem actionProcessAction_measurable {History Action : Type*} [MeasurableSpace History] [MeasurableSpace Action] : Measurable (@actionProcessAction History Action)

Source line 118 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcess_history_map_eq Compiled

The generated process preserves the supplied history marginal.

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

Source line 125 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcess_condDistrib_action_ae_eq_finiteActionKernel Compiled

The sampled action has the generated policy as its a.e. conditional law.

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

Source line 138 Chapter context: EXP3

theorem BanditRLProof.Exp3.finiteActionKernel_ae_eq_finiteActionMeasure Compiled

The generated policy is pointwise the explicit finite Dirac action law.

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)

Source line 160 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcess_integral_importanceWeightedLoss_eq_integral_loss Compiled

Canonical generated-process armwise importance-weighted identity.

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)

Source line 173 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcess_integral_mixedImportanceWeightedLoss_eq_integral_mixedLoss Compiled

Canonical generated-process mixed first-moment identity.

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))

Source line 208 Chapter context: EXP3

theorem BanditRLProof.Exp3.actionProcess_integral_mixedSquaredImportanceWeightedLoss_eq_integral_sum_loss_sq Compiled

Canonical generated-process mixed second-moment identity.

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))

Source line 242 Chapter context: EXP3