`Learning.IT.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.IT.filtrationAction_eq_comap

Details

No docstring.

theorem

Learning.IT.filtrationAction_eq_comap.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (n : ℕ) (hn : n ≠ 0) :
  ↑(filtrationAction 𝓐 𝓨) n =
    MeasurableSpace.comap (fun ω => (hist (n - 1) ω, action n ω))
      inferInstance
Learning.IT.filtrationAction_eq_comap.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ)
  (hn : n ≠ 0) :
  ↑(filtrationAction 𝓐 𝓨) n =
    MeasurableSpace.comap
      (fun ω =>
        (hist (n - 1) ω, action n ω))
      inferInstance

Code

lemma filtrationAction_eq_comap (n : ℕ) (hn : n ≠ 0) :
    filtrationAction 𝓐 𝓨 n =
      MeasurableSpace.comap (fun ω ↦ (hist (n - 1) ω, action n ω)) inferInstance

Type uses (3)

Body uses (4)

Actions: Source · Open Issue

Proof

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

Dependency graph

Type dependencies (3)

`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

`hist`🔗

DefinitionLearning.IT.hist

Details

hist n is the history up to time n. This is a random variable on the measurable space ℕ → 𝓐 × 𝓨.

def

Learning.IT.hist.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ)
  (h : ℕ → 𝓐 × 𝓨) : ↥(Finset.Iic n) → 𝓐 × 𝓨
Learning.IT.hist.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} (n : ℕ) (h : ℕ → 𝓐 × 𝓨) :
  ↥(Finset.Iic n) → 𝓐 × 𝓨

Code

def hist (n : ℕ) (h : ℕ → 𝓐 × 𝓨) : Iic n → 𝓐 × 𝓨 := fun i ↦ h i

Used by (23)

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)

action

Used by (14)

Actions: Source · Open Issue

Proof

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

Learning.IT.filtrationAction_eq_comap🔗

filtrationAction_eq_comap🔗

filtrationAction🔗

hist🔗

action🔗

filtration🔗

adapted_action🔗

measurable_action🔗

`Learning.IT.filtrationAction_eq_comap`🔗

`filtrationAction_eq_comap`🔗

`filtrationAction`🔗

`hist`🔗

`action`🔗

`filtration`🔗

`adapted_action`🔗

`measurable_action`🔗