LeanMachineLearning exposition

Bandits.ArrayModel.indepFun_snd_apply_aux๐Ÿ”—

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

indepFun_snd_apply_aux๐Ÿ”—

LemmaBandits.ArrayModel.indepFun_snd_apply_aux
Details

No docstring.

๐Ÿ”—theorem
Bandits.ArrayModel.indepFun_snd_apply_aux.{u_1, u_2} {๐“ : Type u_1}
  {R : Type u_2} {m๐“ : MeasurableSpace ๐“} {mR : MeasurableSpace R}
  [DecidableEq ๐“] [Nonempty R] (ฮฝ : ProbabilityTheory.Kernel ๐“ R)
  [ProbabilityTheory.IsMarkovKernel ฮฝ] (a : ๐“) (m : โ„•) :
  ProbabilityTheory.IndepFun (fun ฯ‰ => Prod.snd ฯ‰ m a)
    (fun ฯ‰ =>
      (Prod.fst ฯ‰, fun k b =>
        if b = a then
          if m โ‰  0 then Prod.snd ฯ‰ (min k (m - 1)) b
          else Nonempty.some โ‹ฏ
        else Prod.snd ฯ‰ k b))
    (arrayMeasure ฮฝ)
Bandits.ArrayModel.indepFun_snd_apply_aux.{u_1,
    u_2}
  {๐“ : Type u_1} {R : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {mR : MeasurableSpace R} [DecidableEq ๐“]
  [Nonempty R]
  (ฮฝ : ProbabilityTheory.Kernel ๐“ R)
  [ProbabilityTheory.IsMarkovKernel ฮฝ]
  (a : ๐“) (m : โ„•) :
  ProbabilityTheory.IndepFun
    (fun ฯ‰ => Prod.snd ฯ‰ m a)
    (fun ฯ‰ =>
      (Prod.fst ฯ‰, fun k b =>
        if b = a then
          if m โ‰  0 then
            Prod.snd ฯ‰ (min k (m - 1)) b
          else Nonempty.some โ‹ฏ
        else Prod.snd ฯ‰ k b))
    (arrayMeasure ฮฝ)

Code

lemma indepFun_snd_apply_aux (ฮฝ : Kernel ๐“ R) [IsMarkovKernel ฮฝ] (a : ๐“) (m : โ„•) :
    (fun ฯ‰ โ†ฆ ฯ‰.2 m a) โŸ‚แตข[arrayMeasure ฮฝ]
      (fun ฯ‰ โ†ฆ (ฯ‰.1, fun k b โ†ฆ if b = a then if m โ‰  0 then ฯ‰.2 (min k (m - 1)) b
        else Nonempty.some inferInstance else ฯ‰.2 k b))
Type uses (3)
Body uses (2)
Used by (2)

Actions: Source ยท Open Issue

Proof
by
  unfold arrayMeasure
  let ฮผโ‚ : Measure (โ„• โ†’ I) := Measure.infinitePi fun _ โ†ฆ volume
  let ฮผโ‚‚ : Measure (โ„• โ†’ ๐“ โ†’ R) := Measure.infinitePi fun _ โ†ฆ Measure.infinitePi ฮฝ
  -- Independence within ฮผโ‚‚: coordinates ฯ‰ i are independent
  have h_indepโ‚‚ : iIndepFun (fun i (ฯ‰ : โ„• โ†’ ๐“ โ†’ R) โ†ฆ ฯ‰ i) ฮผโ‚‚ :=
    iIndepFun_infinitePi (fun _ โ†ฆ measurable_id)
  -- Independence within each infinitePi ฮฝ: coordinates f b are independent
  have h_indep_inner : iIndepFun (fun (b : ๐“) (f : ๐“ โ†’ R) โ†ฆ f b) (Measure.infinitePi ฮฝ) :=
    iIndepFun_infinitePi (fun _ โ†ฆ measurable_id)
  rw [indepFun_iff_measure_inter_preimage_eq_mul]
  intro s t hs ht
  let X : (โ„• โ†’ I) ร— (โ„• โ†’ ๐“ โ†’ R) โ†’ R := fun ฯ‰ โ†ฆ ฯ‰.2 m a
  let Y : (โ„• โ†’ I) ร— (โ„• โ†’ ๐“ โ†’ R) โ†’ (โ„• โ†’ I) ร— (โ„• โ†’ ๐“ โ†’ R) :=
    fun ฯ‰ โ†ฆ (ฯ‰.1, fun k b โ†ฆ if b = a then if m โ‰  0 then ฯ‰.2 (min k (m - 1)) b
      else Nonempty.some inferInstance else ฯ‰.2 k b)
  have hX_meas : Measurable X :=
    (measurable_pi_apply a).comp ((measurable_pi_apply m).comp measurable_snd)
  have hY_meas : Measurable Y := by
    change Measurable (fun ฯ‰ : (โ„• โ†’ I) ร— (โ„• โ†’ ๐“ โ†’ R) โ†ฆ
      (ฯ‰.1, fun k b โ†ฆ if b = a then if m โ‰  0 then ฯ‰.2 (min k (m - 1)) b
        else Nonempty.some inferInstance else ฯ‰.2 k b))
    refine Measurable.prod measurable_fst ?_
    refine measurable_pi_lambda _ (fun k โ†ฆ ?_)
    refine measurable_pi_lambda _ (fun b โ†ฆ ?_)
    by_cases hb : b = a
    ยท simp only [hb, โ†“reduceIte]
      by_cases hm : m โ‰  0
      ยท simp only [ne_eq, hm, not_false_eq_true, โ†“reduceIte]
        exact (measurable_pi_apply a).comp
          ((measurable_pi_apply (min k (m - 1))).comp measurable_snd)
      ยท simp only [hm, โ†“reduceIte]
        exact measurable_const
    ยท simp only [hb, โ†“reduceIte]
      exact (measurable_pi_apply b).comp ((measurable_pi_apply k).comp measurable_snd)
  change (ฮผโ‚.prod ฮผโ‚‚) (X โปยน' s โˆฉ Y โปยน' t) = (ฮผโ‚.prod ฮผโ‚‚) (X โปยน' s) * (ฮผโ‚.prod ฮผโ‚‚) (Y โปยน' t)
  -- Use Fubini on ฮผโ‚.prod ฮผโ‚‚
  rw [Measure.prod_apply (hs.preimage hX_meas),
    Measure.prod_apply (ht.preimage hY_meas),
    Measure.prod_apply ((hs.preimage hX_meas).inter (ht.preimage hY_meas))]
  -- X only depends on ฯ‰โ‚‚, so its fiber is constant in ฯ‰โ‚
  have hX_fst : โˆ€ ฯ‰โ‚, ฮผโ‚‚ (Prod.mk ฯ‰โ‚ โปยน' (X โปยน' s)) = ฮผโ‚‚ ((fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a) โปยน' s) := fun _ โ†ฆ rfl
  simp_rw [hX_fst]
  -- The LHS integral: fiber of X โˆฉ Y at ฯ‰โ‚
  -- Key: X depends only on ฯ‰โ‚‚ m a, while Y's dependence on ฯ‰โ‚‚ avoids (m, a)
  -- Define the "truncation" map on ฯ‰โ‚‚
  let trunc : (โ„• โ†’ ๐“ โ†’ R) โ†’ (โ„• โ†’ ๐“ โ†’ R) :=
    fun ฯ‰โ‚‚ k b โ†ฆ if b = a then if m โ‰  0 then ฯ‰โ‚‚ (min k (m - 1)) b
      else Nonempty.some inferInstance else ฯ‰โ‚‚ k b
  -- The fiber of Y at ฯ‰โ‚ only depends on trunc(ฯ‰โ‚‚)
  have hY_fiber : โˆ€ ฯ‰โ‚, Prod.mk ฯ‰โ‚ โปยน' (Y โปยน' t) = (fun ฯ‰โ‚‚ โ†ฆ (ฯ‰โ‚, trunc ฯ‰โ‚‚)) โปยน' t := fun _ โ†ฆ rfl
  -- The fiber of X โˆฉ Y factors
  have hXY_fiber : โˆ€ ฯ‰โ‚, Prod.mk ฯ‰โ‚ โปยน' (X โปยน' s โˆฉ Y โปยน' t) =
      ((fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a) โปยน' s) โˆฉ ((fun ฯ‰โ‚‚ โ†ฆ (ฯ‰โ‚, trunc ฯ‰โ‚‚)) โปยน' t) := fun _ โ†ฆ rfl
  simp_rw [hXY_fiber, hY_fiber]
  -- Now we use independence in ฮผโ‚‚: (ฯ‰โ‚‚ m a) is independent of (trunc ฯ‰โ‚‚)
  -- because trunc only uses indices (k, a) with k < m, and (k, b) with b โ‰  a
  have h_trunc_meas : Measurable trunc := by
    refine measurable_pi_lambda _ (fun k โ†ฆ ?_)
    refine measurable_pi_lambda _ (fun b โ†ฆ ?_)
    simp only [trunc]
    by_cases hb : b = a
    ยท simp only [hb, โ†“reduceIte]
      by_cases hm : m = 0
      ยท simp only [hm]
        exact measurable_const
      ยท simp only [ne_eq, hm, not_false_eq_true, โ†“reduceIte]
        exact (measurable_pi_apply a).comp (measurable_pi_apply (min k (m - 1)))
    ยท simp only [hb, โ†“reduceIte]
      exact (measurable_pi_apply b).comp (measurable_pi_apply k)
  -- Key independence: (ฯ‰โ‚‚ m a) โŸ‚ trunc because trunc only uses coordinates โ‰  (m, a)
  have h_indep_trunc : IndepFun (fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a) trunc ฮผโ‚‚ := by
    -- Factor trunc through proj which extracts the relevant coordinates
    let proj : (โ„• โ†’ ๐“ โ†’ R) โ†’ ((โ„• โ†’ R) ร— (โ„• โ†’ {b : ๐“ // b โ‰  a} โ†’ R)) := fun ฯ‰โ‚‚ โ†ฆ
      (fun k โ†ฆ if m โ‰  0 then ฯ‰โ‚‚ (min k (m - 1)) a else Nonempty.some inferInstance,
      fun k โŸจb, _โŸฉ โ†ฆ ฯ‰โ‚‚ k b)
    have h_trunc_proj : โˆ€ ฯ‰โ‚‚, trunc ฯ‰โ‚‚ = (fun p k b โ†ฆ
        if h : b = a then if m โ‰  0 then p.1 k
          else Nonempty.some inferInstance else p.2 k โŸจb, hโŸฉ) (proj ฯ‰โ‚‚) := by
      intro ฯ‰โ‚‚; ext k b; simp only [trunc, proj]; by_cases hb : b = a <;> simp [hb]; grind
    have h_proj_meas : Measurable proj := by
      refine Measurable.prod ?_ ?_
      ยท refine measurable_pi_lambda _ fun k โ†ฆ ?_
        by_cases hm : m โ‰  0
        ยท simp only [proj, ne_eq, hm, not_false_eq_true, โ†“reduceIte]
          exact (measurable_pi_apply a).comp (measurable_pi_apply (min k (m - 1)))
        ยท simp [proj, hm]
      ยท exact measurable_pi_lambda _ (fun k โ†ฆ measurable_pi_lambda _ (fun โŸจb, _โŸฉ โ†ฆ
          (measurable_pi_apply b).comp (measurable_pi_apply k)))
    have h_g_meas : Measurable (fun p : (โ„• โ†’ R) ร— (โ„• โ†’ {b : ๐“ // b โ‰  a} โ†’ R) โ†ฆ
        (fun k b โ†ฆ if h : b = a then if m โ‰  0 then p.1 k else Nonempty.some inferInstance
          else p.2 k โŸจb, hโŸฉ)) := by
      refine measurable_pi_lambda _ (fun k โ†ฆ measurable_pi_lambda _ (fun b โ†ฆ ?_))
      by_cases hb : b = a
      ยท simp only [hb, โ†“reduceDIte]
        by_cases hm : m โ‰  0
        ยท simp only [ne_eq, hm, not_false_eq_true]
          exact (measurable_pi_apply k).comp measurable_fst
        ยท simp [hm]
      ยท simp only [hb, โ†“reduceDIte]
        exact (measurable_pi_apply (โŸจb, hbโŸฉ : {b : ๐“ // b โ‰  a})).comp
          ((measurable_pi_apply k).comp measurable_snd)
    -- Show (ฯ‰โ‚‚ m a) โŸ‚ proj: proj uses coordinates disjoint from (m, a)
    have h_indep_proj : IndepFun (fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a) proj ฮผโ‚‚ := by
      have h_row_bound (hm : m โ‰  0) : โˆ€ k, min k (m - 1) < m := by
        intro k
        calc min k (m - 1) โ‰ค m - 1 := Nat.min_le_right k (m - 1)
          _ < m := Nat.sub_lt (by grind) Nat.one_pos
      rw [indepFun_iff_measure_inter_preimage_eq_mul]
      intro s t' hs ht'
      -- rows_lt_m extracts column a at rows < m, other_cols extracts columns โ‰  a
      let rows_lt_m : (โ„• โ†’ ๐“ โ†’ R) โ†’ (Iio m โ†’ R) := fun ฯ‰โ‚‚ โŸจj, _โŸฉ โ†ฆ ฯ‰โ‚‚ j a
      let other_cols : (โ„• โ†’ ๐“ โ†’ R) โ†’ (โ„• โ†’ {b : ๐“ // b โ‰  a} โ†’ R) := fun ฯ‰โ‚‚ k โŸจb, _โŸฉ โ†ฆ ฯ‰โ‚‚ k b
      have h_proj_factor : โˆ€ ฯ‰โ‚‚, proj ฯ‰โ‚‚ =
          ((fun r k โ†ฆ if hm : m โ‰  0 then r โŸจmin k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)โŸฉ
            else Nonempty.some inferInstance) (rows_lt_m ฯ‰โ‚‚),
           other_cols ฯ‰โ‚‚) := by
        intro ฯ‰โ‚‚; ext1
        ยท ext k
          by_cases hm : m โ‰  0
          ยท simp [proj, rows_lt_m, hm]
          ยท simp [proj, hm]
        ยท rfl
      -- Use iIndepFun structure of the doubly-indexed infinite product
      have h_iindep : iIndepFun (fun (p : โ„• ร— ๐“) ฯ‰ โ†ฆ ฯ‰ p.1 p.2) ฮผโ‚‚ :=
        iIndepFun_uncurry_infinitePi' (X := fun _ _ โ†ฆ id) (fun _ โ†ฆ ฮฝ) (by fun_prop)
      have h_rows_meas : Measurable rows_lt_m :=
        measurable_pi_lambda _ (fun โŸจj, _โŸฉ โ†ฆ (measurable_pi_apply a).comp (measurable_pi_apply j))
      have h_other_meas : Measurable other_cols :=
        measurable_pi_lambda _ (fun k โ†ฆ measurable_pi_lambda _ (fun โŸจb, _โŸฉ โ†ฆ
          (measurable_pi_apply b).comp (measurable_pi_apply k)))
      -- Show (ฯ‰โ‚‚ m a) โŸ‚ (rows_lt_m, other_cols) via indep_iSup_of_disjoint
      have h_indep_combined : IndepFun (fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a)
          (fun ฯ‰โ‚‚ โ†ฆ (rows_lt_m ฯ‰โ‚‚, other_cols ฯ‰โ‚‚)) ฮผโ‚‚ := by
        rw [IndepFun_iff_Indep]
        have h_comap_le : (MeasurableSpace.pi.prod MeasurableSpace.pi).comap
            (fun ฯ‰โ‚‚ โ†ฆ (rows_lt_m ฯ‰โ‚‚, other_cols ฯ‰โ‚‚)) โ‰ค
            โจ† (p : {p : โ„• ร— ๐“ // p โ‰  (m, a)}), mR.comap (fun ฯ‰ โ†ฆ ฯ‰ p.val.1 p.val.2) := by
          rw [MeasurableSpace.comap_prodMk]
          refine sup_le ?_ ?_
          ยท rw [MeasurableSpace.comap_pi]
            refine iSup_le (fun โŸจj, hjโŸฉ โ†ฆ ?_)
            have h_ne : (j, a) โ‰  (m, a) := fun h โ†ฆ (Finset.mem_Iio.mp hj).ne (Prod.mk.inj h).1
            exact le_iSup_of_le โŸจ(j, a), h_neโŸฉ le_rfl
          ยท rw [MeasurableSpace.comap_pi]
            refine iSup_le (fun k โ†ฆ ?_)
            rw [MeasurableSpace.comap_pi]
            refine iSup_le (fun โŸจb, hbโŸฉ โ†ฆ ?_)
            have h_ne : (k, b) โ‰  (m, a) := fun h โ†ฆ hb (Prod.mk.inj h).2
            exact le_iSup_of_le โŸจ(k, b), h_neโŸฉ le_rfl
        refine indep_of_indep_of_le_right ?_ h_comap_le
        have h_disjoint : Disjoint ({(m, a)} : Set (โ„• ร— ๐“)) {p | p โ‰  (m, a)} := by simp
        have h_le : โˆ€ p : โ„• ร— ๐“, mR.comap (fun ฯ‰ : โ„• โ†’ ๐“ โ†’ R โ†ฆ ฯ‰ p.1 p.2) โ‰ค
            MeasurableSpace.pi (m := fun _ โ†ฆ MeasurableSpace.pi) := fun p โ†ฆ
          Measurable.comap_le ((measurable_pi_apply p.2).comp (measurable_pi_apply p.1))
        have h_iindep' : iIndep (fun p : โ„• ร— ๐“ โ†ฆ mR.comap (fun ฯ‰ : โ„• โ†’ ๐“ โ†’ R โ†ฆ ฯ‰ p.1 p.2)) ฮผโ‚‚ :=
          h_iindep.iIndep
        have h_indep := indep_iSup_of_disjoint h_le h_iindep' h_disjoint
        convert h_indep using 2
        ยท simp only [Set.mem_singleton_iff, iSup_iSup_eq_left]
        ยท simp only [ne_eq, Set.mem_setOf_eq, iSup_subtype']
      have h_proj_preimage : proj โปยน' t' = (fun ฯ‰โ‚‚ โ†ฆ (rows_lt_m ฯ‰โ‚‚, other_cols ฯ‰โ‚‚)) โปยน'
          {p | ((fun r k โ†ฆ if hm : m โ‰  0 then
            r โŸจmin k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)โŸฉ
            else Nonempty.some inferInstance) p.1, p.2) โˆˆ t'}
          := by ext ฯ‰โ‚‚; simp only [Set.mem_preimage, Set.mem_setOf_eq, h_proj_factor]
      rw [indepFun_iff_measure_inter_preimage_eq_mul] at h_indep_combined
      rw [h_proj_preimage]
      let T : Set ((Iio m โ†’ R) ร— (โ„• โ†’ {b : ๐“ // b โ‰  a} โ†’ R)) :=
        {p | ((fun r k โ†ฆ if hm : m โ‰  0 then
          r โŸจmin k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)โŸฉ
          else Nonempty.some inferInstance) p.1, p.2) โˆˆ t'}
      have hT_meas : MeasurableSet T := by
        refine ht'.preimage (Measurable.prod ?_ measurable_snd)
        refine measurable_pi_lambda _ (fun k โ†ฆ ?_)
        by_cases hm : m โ‰  0
        ยท simp only [ne_eq, hm, not_false_eq_true, โ†“reduceDIte]
          exact (measurable_pi_apply (โŸจmin k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)โŸฉ :
            Iio m)).comp measurable_fst
        ยท simp [hm]
      change ฮผโ‚‚ ((fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a) โปยน' s โˆฉ (fun ฯ‰โ‚‚ โ†ฆ (rows_lt_m ฯ‰โ‚‚, other_cols ฯ‰โ‚‚)) โปยน' T) =
        ฮผโ‚‚ ((fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a) โปยน' s) *
        ฮผโ‚‚ ((fun ฯ‰โ‚‚ โ†ฆ (rows_lt_m ฯ‰โ‚‚, other_cols ฯ‰โ‚‚)) โปยน' T)
      exact h_indep_combined s T hs hT_meas
    have h_eq : trunc = (fun p k b โ†ฆ if h : b = a then if m โ‰  0 then p.1 k
        else Nonempty.some inferInstance else p.2 k โŸจb, hโŸฉ) โˆ˜ proj := by
      funext ฯ‰โ‚‚; exact h_trunc_proj ฯ‰โ‚‚
    rw [h_eq]
    exact h_indep_proj.comp measurable_id h_g_meas
  rw [indepFun_iff_measure_inter_preimage_eq_mul] at h_indep_trunc
  have h_const : โˆ€ ฯ‰โ‚, ฮผโ‚‚ (((fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a) โปยน' s) โˆฉ ((fun ฯ‰โ‚‚ โ†ฆ (ฯ‰โ‚, trunc ฯ‰โ‚‚)) โปยน' t)) =
      ฮผโ‚‚ ((fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a) โปยน' s) * ฮผโ‚‚ ((fun ฯ‰โ‚‚ โ†ฆ (ฯ‰โ‚, trunc ฯ‰โ‚‚)) โปยน' t) := fun ฯ‰โ‚ โ†ฆ
    h_indep_trunc s _ hs (ht.preimage (by fun_prop))
  simp_rw [h_const]
  let c := ฮผโ‚‚ ((fun ฯ‰โ‚‚ โ†ฆ ฯ‰โ‚‚ m a) โปยน' s)
  change โˆซโป x, c * ฮผโ‚‚ ((fun ฯ‰โ‚‚ โ†ฆ (x, trunc ฯ‰โ‚‚)) โปยน' t) โˆ‚ฮผโ‚ =
    (โˆซโป _, c โˆ‚ฮผโ‚) * โˆซโป x, ฮผโ‚‚ ((fun ฯ‰โ‚‚ โ†ฆ (x, trunc ฯ‰โ‚‚)) โปยน' t) โˆ‚ฮผโ‚
  have h_preimage : โˆ€ x, (fun ฯ‰โ‚‚ โ†ฆ (x, trunc ฯ‰โ‚‚)) โปยน' t = trunc โปยน' (Prod.mk x โปยน' t) := fun _ โ†ฆ rfl
  simp_rw [h_preimage]
  have h_map : โˆ€ x, ฮผโ‚‚ (trunc โปยน' (Prod.mk x โปยน' t)) = (ฮผโ‚‚.map trunc) (Prod.mk x โปยน' t) := by
    intro x; rw [Measure.map_apply h_trunc_meas (ht.preimage (by fun_prop))]
  simp_rw [h_map]
  rw [lintegral_const_mul _ (measurable_measure_prodMk_left_finite ht),
    lintegral_const, measure_univ, mul_one]

Dependency graph

Type dependencies (3)

probSpace๐Ÿ”—

DefinitionBandits.ArrayModel.probSpace
Details

Probability space for the array model of stochastic bandits.

๐Ÿ”—def
Bandits.ArrayModel.probSpace.{u_1, u_2} (๐“ : Type u_1) (R : Type u_2) :
  Type (max u_1 u_2)
Bandits.ArrayModel.probSpace.{u_1, u_2}
  (๐“ : Type u_1) (R : Type u_2) :
  Type (max u_1 u_2)

Code

def probSpace : Type _ := (โ„• โ†’ I) ร— (โ„• โ†’ ๐“ โ†’ R)
Used by (64)

Actions: Source ยท Open Issue

instMeasurableSpaceProbSpace๐Ÿ”—

InstanceBandits.ArrayModel.instMeasurableSpaceProbSpace
Details

No docstring.

๐Ÿ”—def
Bandits.ArrayModel.instMeasurableSpaceProbSpace.{u_3, u_4}
  {๐“ : Type u_3} {R : Type u_4} [MeasurableSpace R] :
  MeasurableSpace (probSpace ๐“ R)
Bandits.ArrayModel.instMeasurableSpaceProbSpace.{u_3,
    u_4}
  {๐“ : Type u_3} {R : Type u_4}
  [MeasurableSpace R] :
  MeasurableSpace (probSpace ๐“ R)

Code

instance {๐“ R : Type*} [MeasurableSpace R] : MeasurableSpace (probSpace ๐“ R)
Type uses (1)
Used by (41)

Actions: Source ยท Open Issue

Proof
inferInstanceAs (MeasurableSpace ((โ„• โ†’ I) ร— (โ„• โ†’ ๐“ โ†’ R)))

arrayMeasure๐Ÿ”—

DefinitionBandits.ArrayModel.arrayMeasure
Details

Probability measure for the array model of stochastic bandits.

๐Ÿ”—def
Bandits.ArrayModel.arrayMeasure.{u_1, u_2} {๐“ : Type u_1} {R : Type u_2}
  {m๐“ : MeasurableSpace ๐“} {mR : MeasurableSpace R}
  (ฮฝ : ProbabilityTheory.Kernel ๐“ R) :
  MeasureTheory.Measure (probSpace ๐“ R)
Bandits.ArrayModel.arrayMeasure.{u_1, u_2}
  {๐“ : Type u_1} {R : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {mR : MeasurableSpace R}
  (ฮฝ : ProbabilityTheory.Kernel ๐“ R) :
  MeasureTheory.Measure (probSpace ๐“ R)

Code

noncomputable
def arrayMeasure (ฮฝ : Kernel ๐“ R) : Measure (probSpace ๐“ R) :=
  (Measure.infinitePi fun _ โ†ฆ volume).prod (streamMeasure ฮฝ)
Type uses (2)
Body uses (1)
Used by (29)

Actions: Source ยท Open Issue

All dependencies, transitively (1)

streamMeasure๐Ÿ”—

DefinitionBandits.streamMeasure
Details

Measure of an infinite stream of rewards from each action.

๐Ÿ”—def
Bandits.streamMeasure.{u_1, u_2} {๐“ : Type u_1} {R : Type u_2}
  {m๐“ : MeasurableSpace ๐“} {mR : MeasurableSpace R}
  (ฮฝ : ProbabilityTheory.Kernel ๐“ R) : MeasureTheory.Measure (โ„• โ†’ ๐“ โ†’ R)
Bandits.streamMeasure.{u_1, u_2}
  {๐“ : Type u_1} {R : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {mR : MeasurableSpace R}
  (ฮฝ : ProbabilityTheory.Kernel ๐“ R) :
  MeasureTheory.Measure (โ„• โ†’ ๐“ โ†’ R)

Code

noncomputable
def streamMeasure (ฮฝ : Kernel ๐“ R) : Measure (โ„• โ†’ ๐“ โ†’ R) :=
  Measure.infinitePi fun _ โ†ฆ Measure.infinitePi ฮฝ
Used by (56)

Actions: Source ยท Open Issue