LeanMachineLearning exposition

Learning.IsBayesAlgEnvSeq.integrable_uncurry_actionMean_comp🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

integrable_uncurry_actionMean_comp🔗

LemmaLearning.IsBayesAlgEnvSeq.integrable_uncurry_actionMean_comp
Details

No docstring.

🔗theorem
Learning.IsBayesAlgEnvSeq.integrable_uncurry_actionMean_comp.{u_1, u_2,
    u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω] [Countable 𝓐]
  [MeasurableSingletonClass 𝓐] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f)
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P]
  {l u : ℝ}
  (hm : ∀ (e : 𝓔) (a : 𝓐), ∫ (x : ℝ), id x ∂κ (e, a) ∈ Set.Icc l u) :
  MeasureTheory.Integrable (fun ω => actionMean κ E (f ω) ω) P
Learning.IsBayesAlgEnvSeq.integrable_uncurry_actionMean_comp.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω]
  [Countable 𝓐]
  [MeasurableSingletonClass 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} (hE : Measurable E)
  {f : Ω → 𝓐} (hf : Measurable f)
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P]
  {l u : ℝ}
  (hm :
    ∀ (e : 𝓔) (a : 𝓐),
      ∫ (x : ℝ), id x ∂κ (e, a) ∈
        Set.Icc l u) :
  MeasureTheory.Integrable
    (fun ω => actionMean κ E (f ω) ω) P

Code

lemma integrable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐]
    {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f)
    {P : Measure Ω} [IsFiniteMeasure P] {l u : ℝ} (hm : ∀ e a, (κ (e, a))[id] ∈ (Set.Icc l u)) :
    Integrable (fun ω ↦ actionMean κ E (f ω) ω) P
Type uses (1)
Body uses (1)
Used by (3)

Actions: Source · Open Issue

Proof
by
  refine ⟨(measurable_uncurry_actionMean_comp hE hf).aestronglyMeasurable, ?_⟩
  apply HasFiniteIntegral.of_bounded
  filter_upwards with ω using abs_le_max_abs_abs (hm (E ω) (f ω)).1 (hm (E ω) (f ω)).2

Dependency graph

Type dependencies (1)

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