LeanMachineLearning

Bandits.indepFun_update_rewardByCountUntil_reward๐Ÿ”—

Lemma

From the authors

Conditionally on the event that the action at time t is b and that b was pulled k times before, the array rewardByCountUntil A R t with the entry (b, k) erased is independent of the reward at time t.

Types
  • ๐“ : Type u_1m๐“ : MeasurableSpace ๐“A measurable space is a space equipped with a ฯƒ-algebra.DecidableEq ๐“MeasurableSingletonClass ๐“A typeclass mixin for MeasurableSpaces such that each singleton is measurable.Countable ๐“A type ฮฑ is countable if there exists an injective map ฮฑ โ†’ โ„•.
  • ฮฉ : Type u_2mฮฉ : MeasurableSpace ฮฉ
Given
  • O : โ„• โ†’ ฮฉ โ†’ Unit
  • A : โ„• โ†’ ฮฉ โ†’ ๐“
  • R : โ„• โ†’ ฮฉ โ†’ โ„
  • P : MeasureTheory.Measure ฮฉA measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.MeasureTheory.IsProbabilityMeasure PA measure ฮผ is called a probability measure if ฮผ univ = 1.
  • alg : Learning.Algorithm Unit ๐“ โ„A stochastic, sequential algorithm.
  • ฮฝ : ProbabilityTheory.Kernel ๐“ โ„A kernel from a measurable space ฮฑ to another measurable space ฮฒ is a measurable function ฮบ : ฮฑ โ†’ Measure ฮฒ.ProbabilityTheory.IsMarkovKernel ฮฝA kernel is a Markov kernel if every measure in its image is a probability measure.
  • t : โ„•
  • b : ๐“
  • k : โ„•
Assuming
Then
ProbabilityTheory.IndepFun (fun ฯ‰ => Function.update (Learning.rewardByCountUntil A R t ฯ‰) (b, k) 0) (fun ฯ‰ => R t ฯ‰.1)
  (P[|{x | A t x = b โˆง Learning.pullCount A b t x = k}].prod (streamMeasure ฮฝ))
Two functions are independent if the two measurable space structures they generate are independent.
Code
lemma indepFun_update_rewardByCountUntil_reward (h : IsAlgEnvSeq O A R alg (stationaryEnv ฮฝ) P)
    (t : โ„•) (b : ๐“) (k : โ„•) :
    (fun ฯ‰ โ†ฆ Function.update (rewardByCountUntil A R t ฯ‰) (b, k) 0)
      โŸ‚แตข[(P[|{x | A t x = b โˆง pullCount A b t x = k}]).prod (streamMeasure ฮฝ)]
      (fun ฯ‰ โ†ฆ R t ฯ‰.1)
Proof
by
  have hA := h.measurable_action
  have hR := h.measurable_feedback
  by_cases hP : P {x | A t x = b โˆง pullCount A b t x = k} = 0
  ยท rw [cond_eq_zero.2 (Or.inr hP), Measure.zero_prod]
    exact indepFun_zero_measure _ _
  have : IsProbabilityMeasure (P[|{x | A t x = b โˆง pullCount A b t x = k}]) :=
    cond_isProbabilityMeasure hP
  have h_indep := (indepFun_history_reward_cond h t b k).symm.fst_prod
    (ฮฝ := streamMeasure ฮฝ) (hR t) (by fun_prop)
  refine (h_indep.of_measurable_right ?_).symm
  refine Measurable.comp measurable_update_left ?_
  refine measurable_rewardByCountUntil_of t (fun i hi โ†ฆ ?_) (fun i hi โ†ฆ ?_) ?_
  ยท exact measurable_comp_comap
      (fun ฯ‰ : ฮฉ ร— (โ„• โ†’ ๐“ โ†’ โ„) โ†ฆ (((history O A R t ฯ‰.1, O t ฯ‰.1), A t ฯ‰.1), ฯ‰.2))
      (g := fun v : ((Hist Unit ๐“ โ„ t ร— Unit) ร— ๐“) ร— (โ„• โ†’ ๐“ โ†’ โ„) โ†ฆ (v.1.1.1 โŸจi, hiโŸฉ).action)
      (by fun_prop)
  ยท exact measurable_comp_comap
      (fun ฯ‰ : ฮฉ ร— (โ„• โ†’ ๐“ โ†’ โ„) โ†ฆ (((history O A R t ฯ‰.1, O t ฯ‰.1), A t ฯ‰.1), ฯ‰.2))
      (g := fun v : ((Hist Unit ๐“ โ„ t ร— Unit) ร— ๐“) ร— (โ„• โ†’ ๐“ โ†’ โ„) โ†ฆ (v.1.1.1 โŸจi, hiโŸฉ).feedback)
      (by fun_prop)
  ยท exact measurable_comp_comap
      (fun ฯ‰ : ฮฉ ร— (โ„• โ†’ ๐“ โ†’ โ„) โ†ฆ (((history O A R t ฯ‰.1, O t ฯ‰.1), A t ฯ‰.1), ฯ‰.2))
      (g := fun v : ((Hist Unit ๐“ โ„ t ร— Unit) ร— ๐“) ร— (โ„• โ†’ ๐“ โ†’ โ„) โ†ฆ v.2) measurable_snd

Meaning last changed in v4.34.0-rc2-76-g565f652 (2026-09-10), the 3th recorded change.

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file ยท open it in the Lean web editor.

Dependency graph

Audit surface: 11 project declarations, 66 external constants

โœ“ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.