LeanMachineLearning exposition

Learning.IT.hist🔗

Minimal Lean file

hist🔗

DefinitionLearning.IT.hist
Details

hist n is the history up to time n. This is a random variable on the measurable space ℕ → 𝓐 × 𝓨.

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

Code

def hist (n : ℕ) (h : ℕ → 𝓐 × 𝓨) : Iic n → 𝓐 × 𝓨 := fun i ↦ h i
Used by (23)

Actions: Source · Open Issue