LeanMachineLearning exposition

Learning.IT.measurable_action_filtrationActionπŸ”—

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_action_filtrationActionπŸ”—

LemmaLearning.IT.measurable_action_filtrationAction
Details

No docstring.

πŸ”—theorem
Learning.IT.measurable_action_filtrationAction.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (n : β„•) : Measurable (action n)
Learning.IT.measurable_action_filtrationAction.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : β„•) :
  Measurable (action n)

Code

lemma measurable_action_filtrationAction (n : β„•) :
    Measurable[filtrationAction 𝓐 𝓨 n] (action n)
Type uses (2)
Body uses (1)

Actions: Source Β· Open Issue

Proof
by
  rw [measurable_iff_comap_le]
  simp only [filtrationAction]
  split_ifs with hn
  Β· simp [hn]
  Β· exact le_sup_of_le_right le_rfl

Dependency graph

Type dependencies (2)

filtrationActionπŸ”—

DefinitionLearning.IT.filtrationAction
Details

Filtration generated by the history at time n-1 together with the action at time n.

πŸ”—def
Learning.IT.filtrationAction.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration β„• inferInstance
Learning.IT.filtrationAction.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration β„• inferInstance

Code

def filtrationAction (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
    Filtration β„• (inferInstance : MeasurableSpace (β„• β†’ 𝓐 Γ— 𝓨)) where
  seq n := if n = 0 then MeasurableSpace.comap (action 0) inferInstance
    else IT.filtration 𝓐 𝓨 (n - 1) βŠ” MeasurableSpace.comap (action n) inferInstance
  mono' n m hnm := by
    simp only
    by_cases hn : n = 0
    Β· by_cases hm : m = 0
      Β· simp [hn, hm]
      Β· simp only [hn, ↓reduceIte, hm]
        refine le_sup_of_le_left ?_
        rw [← measurable_iff_comap_le]
        suffices Measurable[IT.filtration 𝓐 𝓨 0] (action 0) from
          this.mono ((IT.filtration 𝓐 𝓨).mono zero_le) le_rfl
        exact adapted_action 0
    have hm : m β‰  0 := by grind
    simp only [hn, hm, ↓reduceIte]
    have hnm' : n - 1 ≀ m - 1 := by grind
    simp only [sup_le_iff]
    constructor
    Β· refine le_sup_of_le_left ?_
      exact (IT.filtration 𝓐 𝓨).mono hnm'
    Β· rcases eq_or_lt_of_le hnm with rfl | hlt
      Β· exact le_sup_of_le_right le_rfl
      refine le_sup_of_le_left ?_
      rw [← measurable_iff_comap_le]
      have h_le : n ≀ m - 1 := by grind
      suffices Measurable[IT.filtration 𝓐 𝓨 n] (action n) from
        this.mono ((IT.filtration 𝓐 𝓨).mono h_le) le_rfl
      exact adapted_action n
  le' n := by
    by_cases hn : n = 0
    Β· simp only [hn, ↓reduceIte]
      rw [← measurable_iff_comap_le]
      fun_prop
    simp only [hn, ↓reduceIte, sup_le_iff]
    constructor
    Β· exact (IT.filtration 𝓐 𝓨).le _
    Β· rw [← measurable_iff_comap_le]
      fun_prop
Body uses (4)
Used by (7)

Actions: Source Β· Open Issue

actionπŸ”—

DefinitionLearning.IT.action
Details

action n is the action pulled at time n. This is a random variable on the measurable space β„• β†’ 𝓐 Γ— 𝓨.

πŸ”—def
Learning.IT.action.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2} (n : β„•)
  (h : β„• β†’ 𝓐 Γ— 𝓨) : 𝓐
Learning.IT.action.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} (n : β„•)
  (h : β„• β†’ 𝓐 Γ— 𝓨) : 𝓐

Code

def action (n : β„•) (h : β„• β†’ 𝓐 Γ— 𝓨) : 𝓐 := (h n).1
Used by (31)

Actions: Source Β· Open Issue

All dependencies, transitively (3)

filtrationπŸ”—

DefinitionLearning.IT.filtration
Details

Filtration of the algorithm Seq.

πŸ”—def
Learning.IT.filtration.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration β„• inferInstance
Learning.IT.filtration.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration β„• inferInstance

Code

protected def filtration (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
    Filtration β„• (inferInstance : MeasurableSpace (β„• β†’ 𝓐 Γ— 𝓨)) :=
  MeasureTheory.Filtration.piLE (X := fun _ ↦ 𝓐 Γ— 𝓨)
Used by (13)

Actions: Source Β· Open Issue

adapted_actionπŸ”—

LemmaLearning.IT.adapted_action
Details

No docstring.

πŸ”—theorem
Learning.IT.adapted_action.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted (IT.filtration 𝓐 𝓨) action
Learning.IT.adapted_action.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted
    (IT.filtration 𝓐 𝓨) action

Code

lemma adapted_action : Adapted (IT.filtration 𝓐 𝓨) action
Type uses (2)
Body uses (4)
Used by (3)

Actions: Source Β· Open Issue

Proof
by
  intro n
  rw [filtration_eq_comap, action_eq_eval_comp_hist]
  exact measurable_comp_comap _ (by fun_prop)

measurable_actionπŸ”—

LemmaLearning.IT.measurable_action
Details

No docstring.

πŸ”—theorem
Learning.IT.measurable_action.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : β„•) :
  Measurable (action n)
Learning.IT.measurable_action.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : β„•) :
  Measurable (action n)

Code

lemma measurable_action (n : β„•) : Measurable (action n (𝓐
Type uses (1)
Used by (14)

Actions: Source Β· Open Issue

Proof
𝓐) (𝓨 := 𝓨)) := by
  unfold action; fun_prop