LeanMachineLearning exposition

Learning.IT.feedback🔗

Minimal Lean file

feedback🔗

DefinitionLearning.IT.feedback
Details

feedback n is the feedback at time n. This is a random variable on the measurable space ℕ → 𝓐 × 𝓨.

🔗def
Learning.IT.feedback.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ)
  (h : ℕ → 𝓐 × 𝓨) : 𝓨
Learning.IT.feedback.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ)
  (h : ℕ → 𝓐 × 𝓨) : 𝓨

Code

def feedback (n : ℕ) (h : ℕ → 𝓐 × 𝓨) : 𝓨 := (h n).2
Used by (16)

Actions: Source · Open Issue