LeanMachineLearning exposition

Learning.IsAlgEnvSeq.filtrationAction_zero_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_zero_eq_comap🔗

LemmaLearning.IsAlgEnvSeq.filtrationAction_zero_eq_comap
Details

No docstring.

🔗theorem
Learning.IsAlgEnvSeq.filtrationAction_zero_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)} :
  ↑(filtrationAction hA hY) 0 =
    MeasurableSpace.comap (A 0) inferInstance
Learning.IsAlgEnvSeq.filtrationAction_zero_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)} :
  ↑(filtrationAction hA hY) 0 =
    MeasurableSpace.comap (A 0)
      inferInstance

Code

lemma IsAlgEnvSeq.filtrationAction_zero_eq_comap
    {hA : ∀ n, Measurable (A n)} {hY : ∀ n, Measurable (Y n)} :
    filtrationAction hA hY 0 = MeasurableSpace.comap (A 0) inferInstance
Type uses (1)
Body uses (1)

Actions: Source · Open Issue

Proof
by
  simp [filtrationAction]

Dependency graph

Type dependencies (1)

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

All dependencies, transitively (5)

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

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)