LeanMachineLearning exposition

Learning.measurable_history๐Ÿ”—

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_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

Dependency graph

Type dependencies (1)

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