LeanMachineLearning exposition

Bandits.ArrayModel.indepFun_fst_add_one_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_fst_add_one_aux๐Ÿ”—

LemmaBandits.ArrayModel.indepFun_fst_add_one_aux
Details

No docstring.

๐Ÿ”—theorem
Bandits.ArrayModel.indepFun_fst_add_one_aux.{u_1, u_2} {๐“ : Type u_1}
  {R : Type u_2} {m๐“ : MeasurableSpace ๐“} {mR : MeasurableSpace R}
  (ฮฝ : ProbabilityTheory.Kernel ๐“ R)
  [ProbabilityTheory.IsMarkovKernel ฮฝ] (n : โ„•) :
  ProbabilityTheory.IndepFun (fun ฯ‰ => Prod.fst ฯ‰ (n + 1))
    (fun ฯ‰ => (fun i => Prod.fst ฯ‰ โ†‘i, Prod.snd ฯ‰)) (arrayMeasure ฮฝ)
Bandits.ArrayModel.indepFun_fst_add_one_aux.{u_1,
    u_2}
  {๐“ : Type u_1} {R : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {mR : MeasurableSpace R}
  (ฮฝ : ProbabilityTheory.Kernel ๐“ R)
  [ProbabilityTheory.IsMarkovKernel ฮฝ]
  (n : โ„•) :
  ProbabilityTheory.IndepFun
    (fun ฯ‰ => Prod.fst ฯ‰ (n + 1))
    (fun ฯ‰ =>
      (fun i => Prod.fst ฯ‰ โ†‘i,
        Prod.snd ฯ‰))
    (arrayMeasure ฮฝ)

Code

lemma indepFun_fst_add_one_aux (ฮฝ : Kernel ๐“ R) [IsMarkovKernel ฮฝ] (n : โ„•) :
    (fun ฯ‰ โ†ฆ ฯ‰.1 (n + 1)) โŸ‚แตข[arrayMeasure ฮฝ] (fun ฯ‰ โ†ฆ (fun (i : Iic n) โ†ฆ ฯ‰.1 i, ฯ‰.2))
Type uses (3)
Body uses (2)
Used by (1)

Actions: Source ยท Open Issue

Proof
by
  let ฮผโ‚ : Measure (โ„• โ†’ I) := Measure.infinitePi fun _ โ†ฆ volume
  let ฮผโ‚‚ : Measure (โ„• โ†’ ๐“ โ†’ R) := streamMeasure ฮฝ
  -- Coordinates of ฮผโ‚ are independent
  have h_indep : iIndepFun (fun i (ฯ‰ : โ„• โ†’ I) โ†ฆ ฯ‰ i) ฮผโ‚ :=
    iIndepFun_infinitePi (fun _ โ†ฆ measurable_id)
  have h_indep_n : IndepFun (fun ฯ‰ โ†ฆ ฯ‰ (n + 1)) (fun ฯ‰ โ†ฆ fun i : Iic n โ†ฆ ฯ‰ i) ฮผโ‚ := by
    have h := h_indep.indepFun_finsetโ‚€ {n + 1} (Iic n) (by simp)
      (fun i โ†ฆ (measurable_pi_apply i).aemeasurable)
    convert h.comp (measurable_pi_apply โŸจn + 1, by simpโŸฉ) measurable_id using 1
    ยท rfl
    ยท rfl
  rw [indepFun_iff_measure_inter_preimage_eq_mul]
  intro s t hs ht
  let X : (โ„• โ†’ I) ร— (โ„• โ†’ ๐“ โ†’ R) โ†’ I := fun ฯ‰ โ†ฆ ฯ‰.1 (n + 1)
  let Y : (โ„• โ†’ I) ร— (โ„• โ†’ ๐“ โ†’ R) โ†’ (Iic n โ†’ I) ร— (โ„• โ†’ ๐“ โ†’ R) := fun ฯ‰ โ†ฆ (fun i โ†ฆ ฯ‰.1 i, ฯ‰.2)
  change (ฮผโ‚.prod ฮผโ‚‚) (X โปยน' s โˆฉ Y โปยน' t) = (ฮผโ‚.prod ฮผโ‚‚) (X โปยน' s) * (ฮผโ‚.prod ฮผโ‚‚) (Y โปยน' t)
  -- Rewrite using Fubini
  rw [Measure.prod_apply (hs.preimage (by fun_prop : Measurable X)),
    Measure.prod_apply (ht.preimage (by fun_prop : Measurable Y)),
    Measure.prod_apply ((hs.preimage (by fun_prop : Measurable X)).inter
      (ht.preimage (by fun_prop : Measurable Y)))]
  -- Compute fibers
  have hX_fst ฯ‰โ‚ : ฮผโ‚‚ (Prod.mk ฯ‰โ‚ โปยน' (X โปยน' s)) = s.indicator 1 (ฯ‰โ‚ (n + 1)) := by
    simp only [X, Set.preimage_preimage]
    by_cases h : ฯ‰โ‚ (n + 1) โˆˆ s <;> simp [h]
  have hY_fst ฯ‰โ‚ : ฮผโ‚‚ (Prod.mk ฯ‰โ‚ โปยน' (Y โปยน' t)) = ฮผโ‚‚ {y | ((fun i : Iic n โ†ฆ ฯ‰โ‚ i), y) โˆˆ t} := rfl
  have hXY ฯ‰โ‚ : ฮผโ‚‚ (Prod.mk ฯ‰โ‚ โปยน' (X โปยน' s โˆฉ Y โปยน' t)) =
      s.indicator 1 (ฯ‰โ‚ (n + 1)) * ฮผโ‚‚ {y | ((fun i : Iic n โ†ฆ ฯ‰โ‚ i), y) โˆˆ t} := by
    simp only [X, Y, Set.preimage_inter, Set.preimage_preimage]
    by_cases h : ฯ‰โ‚ (n + 1) โˆˆ s
    ยท simp [h]
      congr
    ยท simp [h]
  simp_rw [hY_fst, hX_fst, hXY]
  -- Factor the integral using independence
  let g : (Iic n โ†’ I) โ†’ ENNReal := fun x โ†ฆ ฮผโ‚‚ {y | (x, y) โˆˆ t}
  have hg_meas : Measurable g := measurable_measure_prodMk_left ht
  have hf_meas : Measurable (fun ฯ‰โ‚ : โ„• โ†’ I โ†ฆ s.indicator (1 : I โ†’ ENNReal) (ฯ‰โ‚ (n + 1))) :=
    (measurable_one.indicator hs).comp (measurable_pi_apply _)
  have hindep_fg : IndepFun (fun ฯ‰โ‚ โ†ฆ s.indicator (1 : I โ†’ ENNReal) (ฯ‰โ‚ (n + 1)))
      (fun ฯ‰โ‚ โ†ฆ g (fun i โ†ฆ ฯ‰โ‚ i)) ฮผโ‚ :=
    h_indep_n.comp (measurable_one.indicator hs) hg_meas
  have h_eq (ฯ‰โ‚ : โ„• โ†’ I) : ฮผโ‚‚ {y | ((fun i : Iic n โ†ฆ ฯ‰โ‚ i), y) โˆˆ t} = g (fun i โ†ฆ ฯ‰โ‚ i) := rfl
  simp_rw [h_eq]
  exact lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun hf_meas (by fun_prop) hindep_fg

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