LeanMachineLearning exposition

Learning.history_succ๐Ÿ”—

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

history_succ๐Ÿ”—

LemmaLearning.history_succ
Details

No docstring.

๐Ÿ”—theorem
Learning.history_succ.{u_1, u_2, u_3} {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ} (n : โ„•) :
  history A Y (n + 1) =
    โ‡‘(MeasurableEquiv.symm
          (MeasurableEquiv.IicSuccProd
            (fun x =>
              match x with
              | Nat => ๐“ ร— ๐“จ)
            n)) โˆ˜
      fun ฯ‰ => (history A Y n ฯ‰, step A Y (n + 1) ฯ‰)
Learning.history_succ.{u_1, u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {A : โ„• โ†’ ฮฉ โ†’ ๐“}
  {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ} (n : โ„•) :
  history A Y (n + 1) =
    โ‡‘(MeasurableEquiv.symm
          (MeasurableEquiv.IicSuccProd
            (fun x =>
              match x with
              | Nat => ๐“ ร— ๐“จ)
            n)) โˆ˜
      fun ฯ‰ =>
      (history A Y n ฯ‰,
        step A Y (n + 1) ฯ‰)

Code

lemma history_succ (n : โ„•) :
    history A Y (n + 1) =
      (MeasurableEquiv.IicSuccProd (fun โ„• โ†ฆ ๐“ ร— ๐“จ) n).symm โˆ˜
        (fun ฯ‰ โ†ฆ (history A Y n ฯ‰, step A Y (n + 1) ฯ‰))
Type uses (3)
Used by (2)

Actions: Source ยท Open Issue

Proof
by
  funext ฯ‰
  symm
  exact (MeasurableEquiv.IicSuccProd (fun _ โ†ฆ ๐“ ร— ๐“จ) n).symm_apply_apply (history A Y (n + 1) ฯ‰)

Dependency graph

Type dependencies (3)

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

IicSuccProd๐Ÿ”—

DefinitionMeasurableEquiv.IicSuccProd
Details

Measurable equivalence between a product up to n + 1 and the pair of the product up to n and the space at n + 1.

๐Ÿ”—def
MeasurableEquiv.IicSuccProd.{u_3} (X : โ„• โ†’ Type u_3)
  [(n : โ„•) โ†’ MeasurableSpace (X n)] (n : โ„•) :
  ((i : โ†ฅ(Finset.Iic (n + 1))) โ†’ X โ†‘i) โ‰ƒแต
    ((i : โ†ฅ(Finset.Iic n)) โ†’ X โ†‘i) ร— X (n + 1)
MeasurableEquiv.IicSuccProd.{u_3}
  (X : โ„• โ†’ Type u_3)
  [(n : โ„•) โ†’ MeasurableSpace (X n)]
  (n : โ„•) :
  ((i : โ†ฅ(Finset.Iic (n + 1))) โ†’ X โ†‘i) โ‰ƒแต
    ((i : โ†ฅ(Finset.Iic n)) โ†’ X โ†‘i) ร—
      X (n + 1)

Code

def _root_.MeasurableEquiv.IicSuccProd (X : โ„• โ†’ Type*) [โˆ€ n, MeasurableSpace (X n)] (n : โ„•) :
    MeasurableEquiv (ฮ  i : Iic (n + 1), X i) ((ฮ  i : Iic n, X i) ร— X (n + 1)) :=
  (MeasurableEquiv.IicProdIoc (Nat.le_succ n)).symm.trans
    (MeasurableEquiv.prodCongr (MeasurableEquiv.refl _) (MeasurableEquiv.piSingleton n).symm)
Used by (11)

Actions: Source ยท Open Issue

step๐Ÿ”—

DefinitionLearning.step
Details

Step of the algorithm-environment sequence: the action-feedback pair at time n.

๐Ÿ”—def
Learning.step.{u_1, u_2, u_3} {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} (A : โ„• โ†’ ฮฉ โ†’ ๐“) (Y : โ„• โ†’ ฮฉ โ†’ ๐“จ) (n : โ„•) (ฯ‰ : ฮฉ) : ๐“ ร— ๐“จ
Learning.step.{u_1, u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} (A : โ„• โ†’ ฮฉ โ†’ ๐“)
  (Y : โ„• โ†’ ฮฉ โ†’ ๐“จ) (n : โ„•) (ฯ‰ : ฮฉ) : ๐“ ร— ๐“จ

Code

def step (A : โ„• โ†’ ฮฉ โ†’ ๐“) (Y : โ„• โ†’ ฮฉ โ†’ ๐“จ) (n : โ„•) (ฯ‰ : ฮฉ) : ๐“ ร— ๐“จ :=
  (A n ฯ‰, Y n ฯ‰)
Used by (12)

Actions: Source ยท Open Issue