LeanMachineLearning exposition

Learning.measurable_stepsUntil🔗

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

measurable_stepsUntil🔗

LemmaLearning.measurable_stepsUntil
Details

No docstring.

🔗theorem
Learning.measurable_stepsUntil.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n)) (a : 𝓐) (m : ℕ) :
  Measurable (stepsUntil A a m)
Learning.measurable_stepsUntil.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (a : 𝓐) (m : ℕ) :
  Measurable (stepsUntil A a m)

Code

lemma measurable_stepsUntil [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (a : 𝓐) (m : ℕ) :
    Measurable (stepsUntil A a m)
Type uses (1)
Body uses (4)
Used by (4)

Actions: Source · Open Issue

Proof
by
  classical
  have h_union : {h' : Ω | ∃ s, pullCount A a (s + 1) h' = m}
      = ⋃ s : ℕ, {h' | pullCount A a (s + 1) h' = m} := by ext; simp
  have h_meas_set : MeasurableSet {h' : Ω | ∃ s, pullCount A a (s + 1) h' = m} := by
    rw [h_union]
    refine MeasurableSet.iUnion fun s ↦ (measurableSet_singleton _).preimage ?_
    exact measurable_pullCount hA a (s + 1)
  suffices Measurable fun k ↦ if h : k ∈ {k' | ∃ s, pullCount A a (s + 1) k' = m}
      then (Nat.find h : ℕ∞) else ⊤ by
    convert this with ω
    rw [stepsUntil_eq_dite a m ω]
    rfl
  refine Measurable.dite (s := {k' : Ω | ∃ s, pullCount A a (s + 1) k' = m})
    (f := fun x ↦ (Nat.find x.2 : ℕ∞)) (g := fun _ ↦ ⊤) ?_ (by fun_prop) h_meas_set
  refine Measurable.coe_nat_enat ?_
  refine measurable_find _ fun k ↦ ?_
  suffices MeasurableSet {x : Ω | pullCount A a (k + 1) x = m} by
    have : Subtype.val '' {x : {k' : Ω |
          ∃ s, pullCount A a (s + 1) k' = m} | pullCount A a (k + 1) (x : Ω) = m}
        = {x : Ω | pullCount A a (k + 1) x = m} := by
      ext x
      simp only [Set.mem_setOf_eq, Set.coe_setOf, Set.mem_image, Subtype.exists, exists_and_left,
        exists_prop, exists_eq_right_right, and_iff_left_iff_imp]
      exact fun h ↦ ⟨_, h⟩
    refine (MeasurableEmbedding.subtype_coe h_meas_set).measurableSet_image.mp ?_
    rw [this]
    exact (measurableSet_singleton _).preimage (by fun_prop)
  exact (measurableSet_singleton _).preimage (by fun_prop)

Dependency graph

Type dependencies (1)

stepsUntil🔗

DefinitionLearning.stepsUntil
Details

Number of steps until action a was pulled exactly m times.

🔗def
Learning.stepsUntil.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐) (m : ℕ) (ω : Ω) : ℕ∞
Learning.stepsUntil.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐)
  (m : ℕ) (ω : Ω) : ℕ∞

Code

noncomputable
def stepsUntil (A : ℕ → Ω → 𝓐) (a : 𝓐) (m : ℕ) (ω : Ω) : ℕ∞ :=
  sInf ((↑) '' {s | pullCount A a (s + 1) ω = m})
Body uses (1)
Used by (46)

Actions: Source · Open Issue

All dependencies, transitively (1)

pullCount🔗

DefinitionLearning.pullCount
Details

Number of times action a was chosen up to time t (excluding t).

🔗def
Learning.pullCount.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ
Learning.pullCount.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐)
  (t : ℕ) (ω : Ω) : ℕ

Code

noncomputable
def pullCount (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ :=
  #(filter (fun s ↦ A s ω = a) (range t))
Used by (146)

Actions: Source · Open Issue