BanditRLProof.Algorithms.UCBRealStationaryMeasurePreservingSource

Conditional distributions pull back through a measure-preserving map.

theorem condDistrib_comp_measurePreserving {Alpha : Type u} {Beta : Type v} {Output : Type w} {Source : Type x} [MeasurableSpace Alpha] [MeasurableSpace Beta] [MeasurableSpace Output] [StandardBorelSpace Output] [Nonempty Output] [MeasurableSpace Source] (mu : Measure Source) [IsFiniteMeasure mu] (nu : Measure Alpha) [IsFiniteMeasure nu] (source : Source -> Alpha) (hsource : MeasurePreserving source mu nu) (X : Alpha -> Beta) (Y : Alpha -> Output) (hX : Measurable X) (hY : Measurable Y) : condDistrib (Y ∘ source) (X ∘ source) mu =ᵐ[mu.map (X ∘ source)] condDistrib Y X nu

Canonical UCB action trace composed with an external stream source.

noncomputable def measurePreservingArmStreamAction {Omega : Type u} {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (source : Omega -> ArmRewardStream K) : Omega -> ActionTrace (Fin K)

Canonical selected-reward trace composed with an external stream source.

noncomputable def measurePreservingArmStreamReward {Omega : Type u} {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (source : Omega -> ArmRewardStream K) : Omega -> RewardTrace Real

A measure-preserving source of canonical arm streams produces every field of the local stationary UCB compatibility bundle on the external sample space.

theorem realStationaryUCBSequence_comp_measurePreserving_armStream {Omega : Type u} {K : Nat} [NeZero K] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (source : Omega -> ArmRewardStream K) (hsource : MeasurePreserving source mu (armStreamMeasure nu)) : RealStationaryUCBSequence mu hK c sigma2 nu (measurePreservingArmStreamAction hK c sigma2 source) (measurePreservingArmStreamReward hK c sigma2 source)

Canonical UCB action on a stream product with auxiliary noise.

noncomputable def productNoiseArmStreamAction {K : Nat} [NeZero K] {Aux : Type u} (hK : 0 < K) (c : Real) (sigma2 : NNReal) : ArmRewardStream K × Aux -> ActionTrace (Fin K)

Canonical selected reward on a stream product with auxiliary noise.

noncomputable def productNoiseArmStreamReward {K : Nat} [NeZero K] {Aux : Type u} (hK : 0 < K) (c : Real) (sigma2 : NNReal) : ArmRewardStream K × Aux -> RewardTrace Real

Product-first projection is a concrete external stationary UCB source.

theorem realStationaryUCBSequence_productNoise_armStream {K : Nat} [NeZero K] {Aux : Type u} [MeasurableSpace Aux] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (auxMu : Measure Aux) [IsProbabilityMeasure auxMu] : RealStationaryUCBSequence ((armStreamMeasure nu).prod auxMu) hK c sigma2 nu (productNoiseArmStreamAction hK c sigma2) (productNoiseArmStreamReward hK c sigma2)

Product law for finite Real arm streams and independent auxiliary noise.

noncomputable def finiteArmProductNoiseMeasure {K : Nat} {Aux : Type u} [MeasurableSpace Aux] (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (auxMu : Measure Aux) : Measure (ArmRewardStream K × Aux)

Armwise-bounded laws give the canonical logarithmic expected-regret envelope on a product sample space carrying arbitrary independent auxiliary noise.

theorem productNoiseArmwiseBoundedFiniteArmExpectedRegret_nonneg_and_le {K : Nat} [NeZero K] {Aux : Type u} [MeasurableSpace Aux] (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (auxMu : Measure Aux) [IsProbabilityMeasure auxMu] (hbound : forall arm, Filter.Eventually (fun x : Real => Set.Icc (lo arm) (hi arm) x) (ae (armLaw arm))) (n : Nat) : let sigma2 := Concentration.finiteArmPositiveVarianceProxy (fun arm => Concentration.intervalVarianceProxy (lo arm) (hi arm)) 0 <= realStationaryArmwiseBoundedFiniteArmExpectedRegret (finiteArmProductNoiseMeasure armLaw hprob auxMu) armLaw (productNoiseArmStreamAction hK 4 sigma2) n /\ realStationaryArmwiseBoundedFiniteArmExpectedRegret (finiteArmProductNoiseMeasure armLaw hprob auxMu) armLaw (productNoiseArmStreamAction hK 4 sigma2) n <= realStationaryArmwiseBoundedFiniteArmModelCoefficient armLaw hprob lo hi * (1 + Real.log ((n + 1 : Nat) : Real))

The expected regret per round of product-noise stationary UCB with armwise bounded finite Real reward laws tends to zero.

theorem productNoiseArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero {K : Nat} [NeZero K] {Aux : Type u} [MeasurableSpace Aux] (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (auxMu : Measure Aux) [IsProbabilityMeasure auxMu] (hbound : forall arm, Filter.Eventually (fun x : Real => Set.Icc (lo arm) (hi arm) x) (ae (armLaw arm))) : let sigma2 := Concentration.finiteArmPositiveVarianceProxy (fun arm => Concentration.intervalVarianceProxy (lo arm) (hi arm)) Tendsto (realStationaryArmwiseBoundedFiniteArmExpectedAverageRegret (finiteArmProductNoiseMeasure armLaw hprob auxMu) armLaw (productNoiseArmStreamAction hK 4 sigma2)) atTop (nhds 0)