BanditRLProof.Exp3ConditionalMoments

Probability-vector contracts on an explicit finite action support.

structure FiniteActionDistribution {Action : Type u} (arms : Finset Action) (prob : Action -> Real) : Prop where

The finite action law generated by a probability vector on `arms`.

noncomputable def finiteActionMeasure {Action : Type u} [MeasurableSpace Action] (arms : Finset Action) (prob : Action -> Real) : Measure Action

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

theorem finiteActionMeasure_isProbabilityMeasure {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] (arms : Finset Action) (prob : Action -> Real) (hdist : FiniteActionDistribution arms prob) : IsProbabilityMeasure (finiteActionMeasure arms prob)

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

theorem integral_finiteActionMeasure_eq_sum {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] (arms : Finset Action) (prob : Action -> Real) (hdist : FiniteActionDistribution arms prob) (f : Action -> Real) : integral (finiteActionMeasure arms prob) f = arms.sum (fun action => prob action * f action)

An identified finite conditional action law converts any integrable history/action score into the corresponding probability-weighted finite sum.

theorem integral_historyAction_eq_integral_sum_of_condDistrib_ae_eq_finiteActionMeasure {Omega : Type u} {History : Type v} {Action : Type w} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (arms : Finset Action) (prob : History -> Action -> Real) (hdist : forall h, FiniteActionDistribution arms (prob h)) (policy : Kernel History Action) [IsMarkovKernel policy] (hpolicy : policy =ᵐ[mu.map history] fun h => finiteActionMeasure arms (prob h)) (hcond : condDistrib action history mu =ᵐ[mu.map history] policy) (score : History × Action -> Real) (hscore : Measurable score) (hIntegrable : Integrable score (mu.map history ⊗ₘ policy)) : integral mu (fun omega => score (history omega, action omega)) = integral (mu.map history) (fun h => arms.sum (fun candidate => prob h candidate * score (h, candidate)))

One-round armwise unbiasedness under the identified conditional action law.

theorem integral_importanceWeightedLoss_eq_integral_loss_of_condDistrib {Omega : Type u} {History : Type v} {Action : Type w} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (arms : Finset Action) (prob loss : History -> Action -> Real) (hdist : forall h, FiniteActionDistribution arms (prob h)) (hprob : forall h candidate, candidate ∈ arms -> 0 < prob h candidate) (policy : Kernel History Action) [IsMarkovKernel policy] (hpolicy : policy =ᵐ[mu.map history] fun h => finiteActionMeasure arms (prob h)) (hcond : condDistrib action history mu =ᵐ[mu.map history] policy) (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) (mu.map history ⊗ₘ policy)) : integral mu (fun omega => importanceWeightedLoss (prob (history omega)) (loss (history omega)) (action omega) comparator) = integral (mu.map history) (fun h => loss h comparator)

The mixed estimated-loss integral equals the true mixed-loss integral.

theorem integral_mixedImportanceWeightedLoss_eq_integral_mixedLoss_of_condDistrib {Omega : Type u} {History : Type v} {Action : Type w} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (arms : Finset Action) (prob loss : History -> Action -> Real) (hdist : forall h, FiniteActionDistribution arms (prob h)) (hprob : forall h candidate, candidate ∈ arms -> 0 < prob h candidate) (policy : Kernel History Action) [IsMarkovKernel policy] (hpolicy : policy =ᵐ[mu.map history] fun h => finiteActionMeasure arms (prob h)) (hcond : condDistrib action history mu =ᵐ[mu.map history] policy) (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) (mu.map history ⊗ₘ policy)) : integral mu (fun omega => mixedImportanceWeightedLoss arms (prob (history omega)) (loss (history omega)) (action omega)) = integral (mu.map history) (fun h => arms.sum (fun candidate => prob h candidate * loss h candidate))

A second predictable finite distribution may weight the estimator without changing the sampling law used by the conditional transport.

theorem integral_weightedImportanceWeightedLoss_eq_integral_weightedLoss_of_condDistrib {Omega : Type u} {History : Type v} {Action : Type w} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (arms : Finset Action) (prob weight loss : History -> Action -> Real) (hdist : forall h, FiniteActionDistribution arms (prob h)) (hprob : forall h candidate, candidate ∈ arms -> 0 < prob h candidate) (policy : Kernel History Action) [IsMarkovKernel policy] (hpolicy : policy =ᵐ[mu.map history] fun h => finiteActionMeasure arms (prob h)) (hcond : condDistrib action history mu =ᵐ[mu.map history] policy) (hscore : Measurable (fun z : History × Action => weightedImportanceWeightedLoss arms (prob z.1) (weight z.1) (loss z.1) z.2)) (hIntegrable : Integrable (fun z : History × Action => weightedImportanceWeightedLoss arms (prob z.1) (weight z.1) (loss z.1) z.2) (mu.map history ⊗ₘ policy)) : integral mu (fun omega => weightedImportanceWeightedLoss arms (prob (history omega)) (weight (history omega)) (loss (history omega)) (action omega)) = integral (mu.map history) (fun h => arms.sum (fun candidate => weight h candidate * loss h candidate))

The mixed estimator-square integral equals the integral of summed loss squares.

theorem integral_mixedSquaredImportanceWeightedLoss_eq_integral_sum_loss_sq_of_condDistrib {Omega : Type u} {History : Type v} {Action : Type w} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (arms : Finset Action) (prob loss : History -> Action -> Real) (hdist : forall h, FiniteActionDistribution arms (prob h)) (hprob : forall h candidate, candidate ∈ arms -> 0 < prob h candidate) (policy : Kernel History Action) [IsMarkovKernel policy] (hpolicy : policy =ᵐ[mu.map history] fun h => finiteActionMeasure arms (prob h)) (hcond : condDistrib action history mu =ᵐ[mu.map history] policy) (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) (mu.map history ⊗ₘ policy)) : integral mu (fun omega => mixedSquaredImportanceWeightedLoss arms (prob (history omega)) (loss (history omega)) (action omega)) = integral (mu.map history) (fun h => arms.sum (fun candidate => (loss h candidate) ^ 2))