LeanMachineLearning exposition

Learning.IsBayesAlgEnvSeq.actionMean🔗

Minimal Lean file

actionMean🔗

DefinitionLearning.IsBayesAlgEnvSeq.actionMean
Details

A random variable that gives the mean feedback of action a.

🔗def
Learning.IsBayesAlgEnvSeq.actionMean.{u_1, u_2, u_4} {𝓔 : Type u_1}
  {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (a : 𝓐) (ω : Ω) :
  ℝ
Learning.IsBayesAlgEnvSeq.actionMean.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐]
  (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ)
  (E : Ω → 𝓔) (a : 𝓐) (ω : Ω) : ℝ

Code

noncomputable
def actionMean (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (a : 𝓐) (ω : Ω) : ℝ := (κ (E ω, a))[id]
Used by (12)

Actions: Source · Open Issue