LeanMachineLearning

Bandits.identDistrib_rewardByCountUntil_add_one_condπŸ”—

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 arrays rewardByCountUntil A R (t + 1) and rewardByCountUntil A R t have the same law: they differ only in the entry (b, k), which is R t in the first and an auxiliary reward in the second, and both are independent of the rest of the array with law Ξ½ b.

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.IdentDistrib (Learning.rewardByCountUntil A R (t + 1)) (Learning.rewardByCountUntil A R t)
  (P[|{x | A t x = b ∧ Learning.pullCount A b t x = k}].prod (streamMeasure ν))
  (P[|{x | A t x = b ∧ Learning.pullCount A b t x = k}].prod (streamMeasure ν))
Two functions defined on two (possibly different) measure spaces are identically distributed if their image measures coincide.
Code
lemma identDistrib_rewardByCountUntil_add_one_cond (h : IsAlgEnvSeq O A R alg (stationaryEnv Ξ½) P)
    (t : β„•) (b : 𝓐) (k : β„•) :
    IdentDistrib (rewardByCountUntil A R (t + 1)) (rewardByCountUntil A R t)
      ((P[|{x | A t x = b ∧ pullCount A b t x = k}]).prod (streamMeasure ν))
      ((P[|{x | A t x = b ∧ pullCount A b t x = k}]).prod (streamMeasure ν))
Proof
by
  have hA := h.measurable_action
  have hR := h.measurable_feedback
  set E₁ := {x | A t x = b ∧ pullCount A b t x = k} with hE₁
  have hE₁_meas : MeasurableSet E₁ := measurableSet_action_eq_and_pullCount_eq hA t b k
  by_cases hP : P E₁ = 0
  Β· rw [cond_eq_zero.2 (Or.inr hP), Measure.zero_prod]
    exact ⟨(measurable_rewardByCountUntil hA hR _).aemeasurable,
      (measurable_rewardByCountUntil hA hR _).aemeasurable, by simp⟩
  have : IsProbabilityMeasure (P[|E₁]) := cond_isProbabilityMeasure hP
  set ΞΌ' := (P[|E₁]).prod (streamMeasure Ξ½) with hΞΌ'
  have h_ae : βˆ€α΅ Ο‰ βˆ‚ΞΌ', A t Ο‰.1 = b ∧ pullCount A b t Ο‰.1 = k := by
    rw [ae_iff]
    have h_set : {Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ) | Β¬ (A t Ο‰.1 = b ∧ pullCount A b t Ο‰.1 = k)}
        = Eβ‚αΆœ Γ—Λ’ Set.univ := by
      ext Ο‰
      simp [hE₁]
    rw [h_set, hΞΌ', Measure.prod_prod, cond_apply hE₁_meas, Set.inter_compl_self, measure_empty,
      mul_zero, zero_mul]
  set W : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ) β†’ 𝓐 Γ— β„• β†’ ℝ :=
    fun Ο‰ ↦ Function.update (rewardByCountUntil A R t Ο‰) (b, k) 0 with hW
  have hWm : Measurable W := measurable_update_left.comp (measurable_rewardByCountUntil hA hR t)
  have h1 : rewardByCountUntil A R (t + 1)
      =ᡐ[ΞΌ'] fun Ο‰ ↦ Function.update (W Ο‰) (b, k) (R t Ο‰.1) := by
    filter_upwards [h_ae] with ω hω
    obtain ⟨hb, hk⟩ := hΟ‰
    simp only [hW, rewardByCountUntil_add_one, Function.update_idem, hb, hk]
  have h2 : rewardByCountUntil A R t
      =ᡐ[ΞΌ'] fun Ο‰ ↦ Function.update (W Ο‰) (b, k) (Ο‰.2 (k + 1) b) := by
    filter_upwards [h_ae] with ω hω
    obtain ⟨hb, hk⟩ := hΟ‰
    simp only [hW, Function.update_idem]
    rw [← rewardByCountUntil_apply_of_pullCount_le hk.le, Function.update_eq_self]
  -- both `(W, R t)` and `(W, Ο‰.2 (k + 1) b)` have law `(ΞΌ'.map W).prod (Ξ½ b)`
  have hW : HasLaw W (ΞΌ'.map W) ΞΌ' := hWm.hasLaw_map ΞΌ'
  have h1' : HasLaw (fun Ο‰ ↦ Function.update (W Ο‰) (b, k) (R t Ο‰.1))
      (((ΞΌ'.map W).prod (Ξ½ b)).map
        fun q : (𝓐 Γ— β„• β†’ ℝ) Γ— ℝ ↦ Function.update q.1 (b, k) q.2) ΞΌ' :=
    ((measurable_update' (a := (b, k))).hasLaw_map _).comp
      ((indepFun_update_rewardByCountUntil_reward h t b k).hasLaw_prod hW
        (hasLaw_reward_cond_prod h t b k hP))
  have h2' : HasLaw (fun Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ) ↦ Function.update (W Ο‰) (b, k) (Ο‰.2 (k + 1) b))
      (((ΞΌ'.map W).prod (Ξ½ b)).map
        fun q : (𝓐 Γ— β„• β†’ ℝ) Γ— ℝ ↦ Function.update q.1 (b, k) q.2) ΞΌ' :=
    ((measurable_update' (a := (b, k))).hasLaw_map _).comp
      ((indepFun_update_rewardByCountUntil_eval hA hR _ t b k).hasLaw_prod hW
        (hasLaw_snd_apply_prod_streamMeasure _ _ _ _))
  exact ((IdentDistrib.of_ae_eq (measurable_rewardByCountUntil hA hR _).aemeasurable h1).trans
    (h1'.identDistrib h2')).trans
    (IdentDistrib.of_ae_eq (measurable_rewardByCountUntil hA hR _).aemeasurable h2).symm

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, 64 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.