LeanMachineLearning exposition

Learning.IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil๐Ÿ”—

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

action_ae_eq_of_IsAlgEnvSeqUntil๐Ÿ”—

LemmaLearning.IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil
Details

No docstring.

๐Ÿ”—theorem
Learning.IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil.{u_1, u_2,
    u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3} {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {env : Environment ๐“ ๐“จ}
  {P : MeasureTheory.Measure ฮฉ} [MeasureTheory.IsFiniteMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ} {n N : โ„•} [MeasurableEq ๐“]
  [h_det : IsDeterministicAlg alg]
  (h : IsAlgEnvSeqUntil A Y alg env P N) (hn : n < N) :
  A (n + 1) =แต[P] fun ฯ‰ => nextAction alg n (history A Y n ฯ‰)
Learning.IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil.{u_1,
    u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3}
  {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ}
  {env : Environment ๐“ ๐“จ}
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsFiniteMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  {n N : โ„•} [MeasurableEq ๐“]
  [h_det : IsDeterministicAlg alg]
  (h : IsAlgEnvSeqUntil A Y alg env P N)
  (hn : n < N) :
  A (n + 1) =แต[P] fun ฯ‰ =>
    nextAction alg n (history A Y n ฯ‰)

Code

lemma action_ae_eq_of_IsAlgEnvSeqUntil [MeasurableEq ๐“]
    [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeqUntil A Y alg env P N) (hn : n < N) :
    A (n + 1) =แต[P] fun ฯ‰ โ†ฆ nextAction alg n (history A Y n ฯ‰)
Type uses (6)
Body uses (3)
Used by (2)

Actions: Source ยท Open Issue

Proof
by
  have h_eq := (h.hasCondDistrib_action n hn)
  rw [policy_eq_deterministic alg n] at h_eq
  exact ae_eq_of_hasCondDistrib_deterministic (measurable_nextAction _ _) (by fun_prop)
    (by fun_prop) h_eq

Dependency graph

Type dependencies (6)

Algorithm๐Ÿ”—

StructureLearning.Algorithm
Details

A stochastic, sequential algorithm.

๐Ÿ”—structure
Learning.Algorithm.{u_4, u_5} (๐“ : Type u_4) (๐“จ : Type u_5)
  [MeasurableSpace ๐“] [MeasurableSpace ๐“จ] : Type (max u_4 u_5)
Learning.Algorithm.{u_4, u_5}
  (๐“ : Type u_4) (๐“จ : Type u_5)
  [MeasurableSpace ๐“]
  [MeasurableSpace ๐“จ] : Type (max u_4 u_5)

Code

structure Algorithm (๐“ ๐“จ : Type*) [MeasurableSpace ๐“] [MeasurableSpace ๐“จ] where
  /-- Policy or sampling rule: distribution of the next action. -/
  policy : (n : โ„•) โ†’ Kernel (Iic n โ†’ ๐“ ร— ๐“จ) ๐“
  /-- The policy is a Markov kernel. -/
  [h_policy : โˆ€ n, IsMarkovKernel (policy n)]
  /-- Distribution of the first action. -/
  p0 : Measure ๐“
  /-- The first action distribution is a probability measure. -/
  [hp0 : IsProbabilityMeasure p0]
Used by (216)

Actions: Source ยท Open Issue

Environment๐Ÿ”—

StructureLearning.Environment
Details

A stochastic environment.

๐Ÿ”—structure
Learning.Environment.{u_4, u_5} (๐“ : Type u_4) (๐“จ : Type u_5)
  [MeasurableSpace ๐“] [MeasurableSpace ๐“จ] : Type (max u_4 u_5)
Learning.Environment.{u_4, u_5}
  (๐“ : Type u_4) (๐“จ : Type u_5)
  [MeasurableSpace ๐“]
  [MeasurableSpace ๐“จ] : Type (max u_4 u_5)

Code

structure Environment (๐“ ๐“จ : Type*) [MeasurableSpace ๐“] [MeasurableSpace ๐“จ] where
  /-- Distribution of the next observation as function of the past history. -/
  feedback : (n : โ„•) โ†’ Kernel ((Iic n โ†’ ๐“ ร— ๐“จ) ร— ๐“) ๐“จ
  /-- The feedback kernels are Markov kernels. -/
  [h_feedback : โˆ€ n, IsMarkovKernel (feedback n)]
  /-- Distribution of the first observation given the first action. -/
  ฮฝ0 : Kernel ๐“ ๐“จ
  /-- The initial observation kernel is a Markov kernel. -/
  [hp0 : IsMarkovKernel ฮฝ0]
Used by (128)

Actions: Source ยท Open Issue

IsDeterministicAlg๐Ÿ”—

Type ClassLearning.IsDeterministicAlg
Details

An algorithm is deterministic if its initial action and subsequent actions are determined by measurable functions (and not possibly random kernels).

๐Ÿ”—type class
Learning.IsDeterministicAlg.{u_1, u_2} {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  (alg : Algorithm ๐“ ๐“จ) : Prop
Learning.IsDeterministicAlg.{u_1, u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ}
  (alg : Algorithm ๐“ ๐“จ) : Prop

Code

class IsDeterministicAlg (alg : Algorithm ๐“ ๐“จ) : Prop where
  exists_action0 : โˆƒ action0, alg.p0 = Measure.dirac action0
  exists_nextAction n : โˆƒ (nextAction : (Iic n โ†’ ๐“ ร— ๐“จ) โ†’ ๐“) (h_meas : Measurable nextAction),
    alg.policy n = Kernel.deterministic nextAction h_meas
Type uses (1)
Used by (14)

Actions: Source ยท Open Issue

IsAlgEnvSeqUntil๐Ÿ”—

StructureLearning.IsAlgEnvSeqUntil
Details

An algorithm-environment sequence: a sequence of actions and feedbacks generated by an algorithm interacting with an environment.

๐Ÿ”—structure
Learning.IsAlgEnvSeqUntil.{u_1, u_2, u_3} {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {mฮฉ : MeasurableSpace ฮฉ} (A : โ„• โ†’ ฮฉ โ†’ ๐“) (Y : โ„• โ†’ ฮฉ โ†’ ๐“จ)
  (alg : Algorithm ๐“ ๐“จ) (env : Environment ๐“ ๐“จ)
  (P : MeasureTheory.Measure ฮฉ) [MeasureTheory.IsFiniteMeasure P]
  (N : โ„•) : Prop
Learning.IsAlgEnvSeqUntil.{u_1, u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ}
  {mฮฉ : MeasurableSpace ฮฉ} (A : โ„• โ†’ ฮฉ โ†’ ๐“)
  (Y : โ„• โ†’ ฮฉ โ†’ ๐“จ) (alg : Algorithm ๐“ ๐“จ)
  (env : Environment ๐“ ๐“จ)
  (P : MeasureTheory.Measure ฮฉ)
  [MeasureTheory.IsFiniteMeasure P]
  (N : โ„•) : Prop

Code

structure IsAlgEnvSeqUntil
    (A : โ„• โ†’ ฮฉ โ†’ ๐“) (Y : โ„• โ†’ ฮฉ โ†’ ๐“จ) (alg : Algorithm ๐“ ๐“จ) (env : Environment ๐“ ๐“จ)
    (P : Measure ฮฉ) [IsFiniteMeasure P] (N : โ„•) : Prop where
  /-- The action sequence is measurable. -/
  measurable_action n : Measurable (A n) := by fun_prop
  /-- The feedback sequence is measurable. -/
  measurable_feedback n : Measurable (Y n) := by fun_prop
  /-- The first action has the correct law. -/
  hasLaw_action_zero : HasLaw (fun ฯ‰ โ†ฆ (A 0 ฯ‰)) alg.p0 P
  /-- The first feedback has the correct conditional distribution. -/
  hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (A 0) env.ฮฝ0 P
  /-- The next action has the correct conditional distribution given the history. -/
  hasCondDistrib_action n (hn : n < N) :
    HasCondDistrib (A (n + 1)) (history A Y n) (alg.policy n) P
  /-- The next feedback has the correct conditional distribution given the history and
  next action. -/
  hasCondDistrib_feedback n (hn : n < N) :
    HasCondDistrib (Y (n + 1)) (fun ฯ‰ โ†ฆ (history A Y n ฯ‰, A (n + 1) ฯ‰))
      (env.feedback n) P
Type uses (3)
Used by (22)

Actions: Source ยท Open Issue

nextAction๐Ÿ”—

DefinitionLearning.nextAction
Details

The next action of a deterministic algorithm after step n.

๐Ÿ”—def
Learning.nextAction.{u_1, u_2} {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  (alg : Algorithm ๐“ ๐“จ) [h_det : IsDeterministicAlg alg] (n : โ„•) :
  (โ†ฅ(Finset.Iic n) โ†’ ๐“ ร— ๐“จ) โ†’ ๐“
Learning.nextAction.{u_1, u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ}
  (alg : Algorithm ๐“ ๐“จ)
  [h_det : IsDeterministicAlg alg]
  (n : โ„•) : (โ†ฅ(Finset.Iic n) โ†’ ๐“ ร— ๐“จ) โ†’ ๐“

Code

noncomputable
def nextAction (alg : Algorithm ๐“ ๐“จ) [h_det : IsDeterministicAlg alg] (n : โ„•) :
    (Iic n โ†’ ๐“ ร— ๐“จ) โ†’ ๐“ :=
  (h_det.exists_nextAction n).choose
Type uses (2)
Used by (9)

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