LeanMachineLearning exposition

Learning.IsBayesAlgEnvSeq.hasCondDistrib_env_historyπŸ”—

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

hasCondDistrib_env_historyπŸ”—

LemmaLearning.IsBayesAlgEnvSeq.hasCondDistrib_env_history
Details

No docstring.

πŸ”—theorem
Learning.IsBayesAlgEnvSeq.hasCondDistrib_env_history.{u_1, u_2, u_3,
    u_4, u_5}
  {𝓐 : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  {𝓔 : Type u_3} [MeasurableSpace 𝓔] [StandardBorelSpace 𝓐] [Nonempty 𝓐]
  [StandardBorelSpace 𝓨] [Nonempty 𝓨] {Q : MeasureTheory.Measure 𝓔}
  {ΞΊ : ProbabilityTheory.Kernel (𝓔 Γ— 𝓐) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ΞΊ] {Ξ© : Type u_4}
  [MeasurableSpace Ξ©] {E : Ξ© β†’ 𝓔} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨}
  {alg : Algorithm 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©}
  [MeasureTheory.IsProbabilityMeasure P] {Ξ©β‚€ : Type u_5}
  [MeasurableSpace Ξ©β‚€] {Eβ‚€ : Ξ©β‚€ β†’ 𝓔} {Aβ‚€ : β„• β†’ Ξ©β‚€ β†’ 𝓐} {Yβ‚€ : β„• β†’ Ξ©β‚€ β†’ 𝓨}
  {algβ‚€ : Algorithm 𝓐 𝓨} {Pβ‚€ : MeasureTheory.Measure Ξ©β‚€}
  [MeasureTheory.IsProbabilityMeasure Pβ‚€] [StandardBorelSpace 𝓔]
  [Nonempty 𝓔] [MeasureTheory.IsProbabilityMeasure Q]
  (h : IsBayesAlgEnvSeq Q ΞΊ alg E A Y P)
  (hβ‚€ : IsBayesAlgEnvSeq Q ΞΊ algβ‚€ Eβ‚€ Aβ‚€ Yβ‚€ Pβ‚€)
  (hc : Algorithm.AbsolutelyContinuous alg algβ‚€) (n : β„•) :
  ProbabilityTheory.HasCondDistrib E (history A Y n)
    𝓛[Eβ‚€ | history Aβ‚€ Yβ‚€ n; Pβ‚€] P
Learning.IsBayesAlgEnvSeq.hasCondDistrib_env_history.{u_1,
    u_2, u_3, u_4, u_5}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  {𝓔 : Type u_3} [MeasurableSpace 𝓔]
  [StandardBorelSpace 𝓐] [Nonempty 𝓐]
  [StandardBorelSpace 𝓨] [Nonempty 𝓨]
  {Q : MeasureTheory.Measure 𝓔}
  {ΞΊ : ProbabilityTheory.Kernel (𝓔 Γ— 𝓐) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ΞΊ]
  {Ξ© : Type u_4} [MeasurableSpace Ξ©]
  {E : Ξ© β†’ 𝓔} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨}
  {P : MeasureTheory.Measure Ξ©}
  [MeasureTheory.IsProbabilityMeasure P]
  {Ξ©β‚€ : Type u_5} [MeasurableSpace Ξ©β‚€]
  {Eβ‚€ : Ξ©β‚€ β†’ 𝓔} {Aβ‚€ : β„• β†’ Ξ©β‚€ β†’ 𝓐}
  {Yβ‚€ : β„• β†’ Ξ©β‚€ β†’ 𝓨} {algβ‚€ : Algorithm 𝓐 𝓨}
  {Pβ‚€ : MeasureTheory.Measure Ξ©β‚€}
  [MeasureTheory.IsProbabilityMeasure Pβ‚€]
  [StandardBorelSpace 𝓔] [Nonempty 𝓔]
  [MeasureTheory.IsProbabilityMeasure Q]
  (h : IsBayesAlgEnvSeq Q ΞΊ alg E A Y P)
  (hβ‚€ :
    IsBayesAlgEnvSeq Q ΞΊ algβ‚€ Eβ‚€ Aβ‚€ Yβ‚€ Pβ‚€)
  (hc :
    Algorithm.AbsolutelyContinuous alg
      algβ‚€)
  (n : β„•) :
  ProbabilityTheory.HasCondDistrib E
    (history A Y n)
    𝓛[Eβ‚€ | history Aβ‚€ Yβ‚€ n; Pβ‚€] P

Code

lemma hasCondDistrib_env_history (h : IsBayesAlgEnvSeq Q ΞΊ alg E A Y P)
    (hβ‚€ : IsBayesAlgEnvSeq Q ΞΊ algβ‚€ Eβ‚€ Aβ‚€ Yβ‚€ Pβ‚€) (hc : alg β‰ͺₐ algβ‚€) (n : β„•) :
    HasCondDistrib E (history A Y n) (condDistrib Eβ‚€ (history Aβ‚€ Yβ‚€ n) Pβ‚€) P where
  aemeasurable
Type uses (4)
Body uses (9)
Used by (1)

Actions: Source Β· Open Issue

Proof
((measurable_history h.measurable_action
    h.measurable_feedback n).prodMk h.measurable_param).aemeasurable
  map_eq := by
    have hA := h.measurable_action
    have hY := h.measurable_feedback
    have hAβ‚€ := hβ‚€.measurable_action
    have hYβ‚€ := hβ‚€.measurable_feedback
    have hEβ‚€ := hβ‚€.measurable_param
    rw [← map_swap_compProd_map_condDistrib (by fun_prop), h.hasLaw_env.map_eq,
      Measure.compProd_eq_compProd_withDensity_comp_snd (by fun_prop)
        (h.condDistrib_history_eq_condDistrib_hist_withDensity hβ‚€ hc n),
      map_swap_withDensity_comp_snd (by fun_prop),
      ← hβ‚€.hasLaw_env.map_eq, map_swap_compProd_map_condDistrib (by fun_prop),
      ← compProd_map_condDistrib (by fun_prop), ← Measure.compProd_withDensity_left (by fun_prop),
      ← (hasLaw_history_withDensity h hβ‚€ hc n).map_eq]

Dependency graph

Type dependencies (4)

AlgorithmπŸ”—

StructureLearning.Algorithm
Details

A stochastic, sequential algorithm.

πŸ”—structure
Learning.Algorithm.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : Type (max u_4 u_5)
Learning.Algorithm.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] : Type (max u_4 u_5)

Code

structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
  /-- Policy or sampling rule: distribution of the next action. -/
  policy : (n : β„•) β†’ Kernel (Iic n β†’ 𝓐 Γ— 𝓨) 𝓐
  /-- The policy is a Markov kernel. -/
  [h_policy : βˆ€ n, IsMarkovKernel (policy n)]
  /-- Distribution of the first action. -/
  p0 : Measure 𝓐
  /-- The first action distribution is a probability measure. -/
  [hp0 : IsProbabilityMeasure p0]
Used by (216)

Actions: Source Β· Open Issue

IsBayesAlgEnvSeqπŸ”—

StructureLearning.IsBayesAlgEnvSeq
Details

IsBayesAlgEnvSeq Q ΞΊ alg E A Y P states that there is a measure P : Measure Ξ© such that the parameter E : Ξ© β†’ 𝓔 has law Q and that the sequences of actions A : β„• β†’ Ξ© β†’ 𝓐 and feedbacks Y : β„• β†’ Ξ© β†’ 𝓨 are generated by the algorithm alg : Algorithm 𝓐 𝓨 interacting with an underlying environment that depends on E and ΞΊ (stationaryEnv (ΞΊ.sectR (E Ο‰))).

πŸ”—structure
Learning.IsBayesAlgEnvSeq.{u_1, u_2, u_3, u_4} {𝓔 : Type u_1}
  {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ξ©]
  (Q : MeasureTheory.Measure 𝓔) (ΞΊ : ProbabilityTheory.Kernel (𝓔 Γ— 𝓐) 𝓨)
  (alg : Algorithm 𝓐 𝓨) (E : Ξ© β†’ 𝓔) (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨)
  (P : MeasureTheory.Measure Ξ©) [MeasureTheory.IsFiniteMeasure P] : Prop
Learning.IsBayesAlgEnvSeq.{u_1, u_2, u_3,
    u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {Ξ© : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] [MeasurableSpace Ξ©]
  (Q : MeasureTheory.Measure 𝓔)
  (ΞΊ : ProbabilityTheory.Kernel (𝓔 Γ— 𝓐) 𝓨)
  (alg : Algorithm 𝓐 𝓨) (E : Ξ© β†’ 𝓔)
  (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨)
  (P : MeasureTheory.Measure Ξ©)
  [MeasureTheory.IsFiniteMeasure P] : Prop

Code

structure IsBayesAlgEnvSeq
    (Q : Measure 𝓔) (ΞΊ : Kernel (𝓔 Γ— 𝓐) 𝓨) (alg : Algorithm 𝓐 𝓨)
    (E : Ξ© β†’ 𝓔) (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨)
    (P : Measure Ξ©) [IsFiniteMeasure P] : Prop where
  measurable_param : Measurable E := by fun_prop
  measurable_action n : Measurable (A n) := by fun_prop
  measurable_feedback n : Measurable (Y n) := by fun_prop
  hasLaw_env : HasLaw E Q P
  hasCondDistrib_action_zero : HasCondDistrib (A 0) E (Kernel.const _ alg.p0) P
  hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (fun Ο‰ ↦ (E Ο‰, A 0 Ο‰)) ΞΊ P
  hasCondDistrib_action n :
    HasCondDistrib (A (n + 1)) (fun Ο‰ ↦ (E Ο‰, history A Y n Ο‰))
      ((alg.policy n).prodMkLeft _) P
  hasCondDistrib_feedback n :
    HasCondDistrib (Y (n + 1)) (fun Ο‰ ↦ (history A Y n Ο‰, E Ο‰, A (n + 1) Ο‰))
      (ΞΊ.prodMkLeft _) P
Type uses (2)
Used by (22)

Actions: Source Β· Open Issue

AbsolutelyContinuousπŸ”—

StructureLearning.Algorithm.AbsolutelyContinuous
Details

For every time and history, the distribution over actions according to alg is absolutely continuous with respect to the distribution over actions according to algβ‚€.

πŸ”—structure
Learning.Algorithm.AbsolutelyContinuous.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  (alg algβ‚€ : Algorithm 𝓐 𝓨) : Prop
Learning.Algorithm.AbsolutelyContinuous.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  (alg algβ‚€ : Algorithm 𝓐 𝓨) : Prop

Code

structure AbsolutelyContinuous (alg algβ‚€ : Algorithm 𝓐 𝓨) : Prop where
  p0 : alg.p0 β‰ͺ algβ‚€.p0
  policy n h : alg.policy n h β‰ͺ algβ‚€.policy n h
Type uses (1)
Used by (7)

Actions: Source Β· Open Issue

historyπŸ”—

DefinitionLearning.history
Details

History of the algorithm-environment sequence up to time n.

πŸ”—def
Learning.history.{u_1, u_2, u_3} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) :
  β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨
Learning.history.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐)
  (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) :
  β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨

Code

def history (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) : Iic n β†’ 𝓐 Γ— 𝓨 :=
  fun i ↦ (A i Ο‰, Y i Ο‰)
Used by (72)

Actions: Source Β· Open Issue