LeanMachineLearning exposition

Learning.IsAlgEnvSeq.filtrationAction_eq_comapπŸ”—

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

filtrationAction_eq_comapπŸ”—

LemmaLearning.IsAlgEnvSeq.filtrationAction_eq_comap
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.filtrationAction_eq_comap.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} {hA : βˆ€ (n : β„•), Measurable (A n)}
  {hY : βˆ€ (n : β„•), Measurable (Y n)} (n : β„•) (hn : n β‰  0) :
  ↑(filtrationAction hA hY) n =
    MeasurableSpace.comap (fun Ο‰ => (history A Y (n - 1) Ο‰, A n Ο‰))
      inferInstance
Learning.IsAlgEnvSeq.filtrationAction_eq_comap.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨}
  {hA : βˆ€ (n : β„•), Measurable (A n)}
  {hY : βˆ€ (n : β„•), Measurable (Y n)}
  (n : β„•) (hn : n β‰  0) :
  ↑(filtrationAction hA hY) n =
    MeasurableSpace.comap
      (fun Ο‰ =>
        (history A Y (n - 1) Ο‰, A n Ο‰))
      inferInstance

Code

lemma IsAlgEnvSeq.filtrationAction_eq_comap
    {hA : βˆ€ n, Measurable (A n)} {hY : βˆ€ n, Measurable (Y n)} (n : β„•) (hn : n β‰  0) :
    filtrationAction hA hY n =
      MeasurableSpace.comap (fun Ο‰ ↦ (history A Y (n - 1) Ο‰, A n Ο‰)) inferInstance
Type uses (2)
Body uses (2)
Used by (1)

Actions: Source Β· Open Issue

Proof
by
  simp only [filtrationAction, filtration, ← MeasurableSpace.comap_prodMk, hn, ↓reduceIte]
  rfl

Dependency graph

Type dependencies (2)

filtrationActionπŸ”—

DefinitionLearning.IsAlgEnvSeq.filtrationAction
Details

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

πŸ”—def
Learning.IsAlgEnvSeq.filtrationAction.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n))
  (hY : βˆ€ (n : β„•), Measurable (Y n)) : MeasureTheory.Filtration β„• mΞ©
Learning.IsAlgEnvSeq.filtrationAction.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨}
  (hA : βˆ€ (n : β„•), Measurable (A n))
  (hY : βˆ€ (n : β„•), Measurable (Y n)) :
  MeasureTheory.Filtration β„• mΞ©

Code

def IsAlgEnvSeq.filtrationAction
    (hA : βˆ€ n, Measurable (A n)) (hY : βˆ€ n, Measurable (Y n)) :
    Filtration β„• mΞ© where
  seq n := if n = 0 then MeasurableSpace.comap (A 0) inferInstance
    else IsAlgEnvSeq.filtration hA hY (n - 1) βŠ” MeasurableSpace.comap (A 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[IsAlgEnvSeq.filtration hA hY 0] (A 0) from
          this.mono ((IsAlgEnvSeq.filtration hA hY).mono zero_le) le_rfl
        exact adapted_action hA hY 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 (IsAlgEnvSeq.filtration hA hY).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[IsAlgEnvSeq.filtration hA hY n] (A n) from
        this.mono ((IsAlgEnvSeq.filtration hA hY).mono h_le) le_rfl
      exact adapted_action hA hY 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 (IsAlgEnvSeq.filtration hA hY).le _
    Β· rw [← measurable_iff_comap_le]
      fun_prop
Body uses (2)
Used by (3)

Actions: Source Β· Open Issue

historyπŸ”—

DefinitionLearning.history
Details

History of the algorithm-environment sequence up to time n.

πŸ”—def
Learning.history.{u_1, u_2, u_3} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) :
  β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨
Learning.history.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐)
  (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) :
  β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨

Code

def history (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) : Iic n β†’ 𝓐 Γ— 𝓨 :=
  fun i ↦ (A i Ο‰, Y i Ο‰)
Used by (72)

Actions: Source Β· Open Issue

All dependencies, transitively (4)

measurable_comp_comapπŸ”—

LemmaMeasureTheory.measurable_comp_comap
Details

No docstring.

πŸ”—theorem
MeasureTheory.measurable_comp_comap.{u_1, u_2, u_3} {Ξ± : Type u_1}
  {Ξ² : Type u_2} {Ξ³ : Type u_3} {mΞ² : MeasurableSpace Ξ²}
  {mΞ³ : MeasurableSpace Ξ³} (f : Ξ± β†’ Ξ²) {g : Ξ² β†’ Ξ³} (hg : Measurable g) :
  Measurable (g ∘ f)
MeasureTheory.measurable_comp_comap.{u_1,
    u_2, u_3}
  {Ξ± : Type u_1} {Ξ² : Type u_2}
  {Ξ³ : Type u_3} {mΞ² : MeasurableSpace Ξ²}
  {mΞ³ : MeasurableSpace Ξ³} (f : Ξ± β†’ Ξ²)
  {g : Ξ² β†’ Ξ³} (hg : Measurable g) :
  Measurable (g ∘ f)

Code

lemma measurable_comp_comap (f : Ξ± β†’ Ξ²) {g : Ξ² β†’ Ξ³} (hg : Measurable g) :
    Measurable[mβ.comap f] (g ∘ f)
Used by (10)

Actions: Source Β· Open Issue

Proof
by
  rw [measurable_iff_comap_le, ← MeasurableSpace.comap_comp]
  exact MeasurableSpace.comap_mono hg.comap_le

measurable_historyπŸ”—

LemmaLearning.measurable_history
Details

No docstring.

πŸ”—theorem
Learning.measurable_history.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n))
  (hY : βˆ€ (n : β„•), Measurable (Y n)) (n : β„•) :
  Measurable (history A Y n)
Learning.measurable_history.{u_1, u_2,
    u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨}
  (hA : βˆ€ (n : β„•), Measurable (A n))
  (hY : βˆ€ (n : β„•), Measurable (Y n))
  (n : β„•) : Measurable (history A Y n)

Code

lemma measurable_history (hA : βˆ€ n, Measurable (A n))
    (hY : βˆ€ n, Measurable (Y n)) (n : β„•) :
    Measurable (history A Y n)
Type uses (1)
Used by (10)

Actions: Source Β· Open Issue

Proof
by
  unfold history
  fun_prop

filtrationπŸ”—

DefinitionLearning.IsAlgEnvSeq.filtration
Details

Filtration generated by the history up to time n.

πŸ”—def
Learning.IsAlgEnvSeq.filtration.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n))
  (hY : βˆ€ (n : β„•), Measurable (Y n)) : MeasureTheory.Filtration β„• mΞ©
Learning.IsAlgEnvSeq.filtration.{u_1, u_2,
    u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨}
  (hA : βˆ€ (n : β„•), Measurable (A n))
  (hY : βˆ€ (n : β„•), Measurable (Y n)) :
  MeasureTheory.Filtration β„• mΞ©

Code

def IsAlgEnvSeq.filtration (hA : βˆ€ n, Measurable (A n)) (hY : βˆ€ n, Measurable (Y n)) :
    Filtration β„• mΞ© where
  seq i := MeasurableSpace.comap (history A Y i) inferInstance
  mono' i j hij := by
    simp only
    rw [← measurable_iff_comap_le]
    have : history A Y i = (fun h k ↦ h ⟨k.1, by grind⟩) ∘ history A Y j := rfl
    rw [this]
    exact measurable_comp_comap _ (by fun_prop)
  le' i := by
    rw [← measurable_iff_comap_le]
    exact Learning.measurable_history hA hY i
Body uses (3)
Used by (18)

Actions: Source Β· Open Issue

adapted_actionπŸ”—

LemmaLearning.IsAlgEnvSeq.adapted_action
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.adapted_action.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n))
  (hY : βˆ€ (n : β„•), Measurable (Y n)) :
  MeasureTheory.Adapted (filtration hA hY) A
Learning.IsAlgEnvSeq.adapted_action.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨}
  (hA : βˆ€ (n : β„•), Measurable (A n))
  (hY : βˆ€ (n : β„•), Measurable (Y n)) :
  MeasureTheory.Adapted (filtration hA hY)
    A

Code

lemma IsAlgEnvSeq.adapted_action
    (hA : βˆ€ n, Measurable (A n)) (hY : βˆ€ n, Measurable (Y n)) :
    Adapted (filtration hA hY) A
Type uses (1)
Body uses (2)
Used by (3)

Actions: Source Β· Open Issue

Proof
by
  intro n
  have : A n = (fun h ↦ (h ⟨n, by simp⟩).1) ∘ (history A Y n) := by
    ext Ο‰ : 1
    simp [history]
  rw [this]
  exact measurable_comp_comap _ (by fun_prop)