LeanMachineLearning exposition

Learning.IT.action🔗

Minimal Lean file

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