LeanMachineLearning exposition

Learning.IT.filtration🔗

Minimal Lean file

filtration🔗

DefinitionLearning.IT.filtration
Details

Filtration of the algorithm Seq.

🔗def
Learning.IT.filtration.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration ℕ inferInstance
Learning.IT.filtration.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration ℕ inferInstance

Code

protected def filtration (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
    Filtration ℕ (inferInstance : MeasurableSpace (ℕ → 𝓐 × 𝓨)) :=
  MeasureTheory.Filtration.piLE (X := fun _ ↦ 𝓐 × 𝓨)
Used by (13)

Actions: Source · Open Issue