Oblivious and stationary environments #
An oblivious environment is an environment in which the distribution of the next feedback depends only on the last action (and not on the past history nor on the current observation). If the kernel that gives the distribution of the next feedback given the last action is the same at every time step, then we say that the environment is stationary.
Main definitions #
We define a Prop-valued typeclass IsObliviousEnv to express that an environment is oblivious,
and we define two constructors for oblivious environments. Those constructors build environments
without observations, that is with observation type Unit.
Typeclass and related definitions:
IsObliviousEnv env: the environmentenvis oblivious.feedbackCondAction env n: the kernel representing the conditional distribution of the feedback given the action at timenin an oblivious environmentenv.
Constructors for oblivious environments:
obliviousEnv ν: an oblivious environment without observations, in which the distribution of the next feedback depends only on the last action, but in a possibly time-dependent manner, and is given by a sequence of Markov kernelsν : ℕ → Kernel 𝓐 𝓨.stationaryEnv ν: a stationary environment without observations, in which the distribution of the next feedback depends only on the last action (and not on the past history), and is given by a Markov kernelν : Kernel 𝓐 𝓨.
class
Learning.IsObliviousEnv
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(env : Environment 𝓞 𝓐 𝓨)
:
An environment is oblivious if the distribution of the next feedback depends only on the last action and not on the past history nor on the current observation.
- exists_eq_prodMkLeft : ∃ (ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨), (∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)) ∧ ∀ (n : ℕ), env.feedback n = ProbabilityTheory.Kernel.prodMkLeft (Hist 𝓞 𝓐 𝓨 n × 𝓞) (ν n)
Instances
noncomputable def
Learning.feedbackCondAction
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(env : Environment 𝓞 𝓐 𝓨)
[h_obl : IsObliviousEnv env]
(n : ℕ)
:
The kernel representing the conditional distribution of the feedback given the action
at time n in an oblivious environment.
Equations
- Learning.feedbackCondAction env n = ⋯.choose n
Instances For
instance
Learning.instIsMarkovKernelFeedbackCondAction
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(env : Environment 𝓞 𝓐 𝓨)
[IsObliviousEnv env]
(n : ℕ)
:
theorem
Learning.feedback_eq_feedbackCondAction
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(env : Environment 𝓞 𝓐 𝓨)
[IsObliviousEnv env]
(n : ℕ)
:
theorem
Learning.ν0_eq_feedbackCondAction
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(env : Environment 𝓞 𝓐 𝓨)
[IsObliviousEnv env]
:
theorem
Learning.IsObliviousEnv.hasCondDistrib_feedback_history_action
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm 𝓞 𝓐 𝓨}
{env : Environment 𝓞 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{O : ℕ → Ω → 𝓞}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
[IsObliviousEnv env]
(h : IsAlgEnvSeq O A Y alg env P)
(n : ℕ)
:
ProbabilityTheory.HasCondDistrib (Y n) (fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω))
(ProbabilityTheory.Kernel.prodMkLeft (Hist 𝓞 𝓐 𝓨 n × 𝓞) (feedbackCondAction env n)) P
theorem
Learning.IsObliviousEnv.hasCondDistrib_feedback
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm 𝓞 𝓐 𝓨}
{env : Environment 𝓞 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{O : ℕ → Ω → 𝓞}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
[IsObliviousEnv env]
(h : IsAlgEnvSeq O A Y alg env P)
(n : ℕ)
:
ProbabilityTheory.HasCondDistrib (Y n) (A n) (feedbackCondAction env n) P
theorem
Learning.IsObliviousEnv.hasLaw_feedback_cond
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm 𝓞 𝓐 𝓨}
{env : Environment 𝓞 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{O : ℕ → Ω → 𝓞}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
[IsObliviousEnv env]
(h : IsAlgEnvSeq O A Y alg env P)
(n : ℕ)
{s : Set ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐)}
(hs : MeasurableSet s)
{b : 𝓐}
(hsb : ∀ u ∈ s, u.2 = b)
(hP : P ((fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s) ≠ 0)
:
Conditionally on an event determined by the history before time n and the action at time
n, on which that action is equal to b, the feedback at time n has law
feedbackCondAction env n b.
theorem
Learning.IsObliviousEnv.indepFun_history_action_feedback_cond
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm 𝓞 𝓐 𝓨}
{env : Environment 𝓞 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{O : ℕ → Ω → 𝓞}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
[IsObliviousEnv env]
(h : IsAlgEnvSeq O A Y alg env P)
(n : ℕ)
{s : Set ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐)}
(hs : MeasurableSet s)
{b : 𝓐}
(hsb : ∀ u ∈ s, u.2 = b)
:
Conditionally on an event determined by the history before time n and the action at time
n, on which that action is constant, the feedback at time n is independent of the
history before time n and of the action at time n.
theorem
Learning.IsObliviousEnv.condIndepFun_feedback_history_action
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm 𝓞 𝓐 𝓨}
{env : Environment 𝓞 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{O : ℕ → Ω → 𝓞}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
[StandardBorelSpace 𝓞]
[Nonempty 𝓞]
[StandardBorelSpace 𝓐]
[Nonempty 𝓐]
[StandardBorelSpace 𝓨]
[Nonempty 𝓨]
[StandardBorelSpace Ω]
[IsObliviousEnv env]
(h : IsAlgEnvSeq O A Y alg env P)
(n : ℕ)
:
ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (A n) inferInstance) ⋯ (Y n)
(fun (ω : Ω) => (history O A Y n ω, O n ω)) P
The feedback at time n is conditionally independent of the history before time n and of
the observation at time n, given the action at time n.
theorem
Learning.IsObliviousEnv.condIndepFun_feedback_history_action_action
{𝓞 : Type u_1}
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm 𝓞 𝓐 𝓨}
{env : Environment 𝓞 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{O : ℕ → Ω → 𝓞}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
[StandardBorelSpace 𝓞]
[Nonempty 𝓞]
[StandardBorelSpace 𝓐]
[Nonempty 𝓐]
[StandardBorelSpace 𝓨]
[Nonempty 𝓨]
[StandardBorelSpace Ω]
[IsObliviousEnv env]
(h : IsAlgEnvSeq O A Y alg env P)
(n : ℕ)
:
ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (A n) inferInstance) ⋯ (Y n)
(fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω)) P
noncomputable def
Learning.obliviousEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨)
[∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)]
:
Environment Unit 𝓐 𝓨
An oblivious environment without observations, in which the distribution of the next feedback depends only on the last action, but in a possibly time-dependent manner.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Learning.obliviousEnv_obs
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨)
[∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)]
(x✝ : ℕ)
:
(obliviousEnv ν).obs x✝ = ProbabilityTheory.Kernel.const (Hist Unit 𝓐 𝓨 x✝) (MeasureTheory.Measure.dirac ())
@[simp]
theorem
Learning.obliviousEnv_feedback
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨)
[∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)]
(n : ℕ)
:
theorem
Learning.feedback_obliviousEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨)
[∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)]
(n : ℕ)
:
@[simp]
theorem
Learning.obs0_obliviousEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨)
[∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)]
:
@[simp]
theorem
Learning.ν0_obliviousEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨)
[∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)]
:
instance
Learning.instIsObliviousEnvUnitObliviousEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨)
[∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)]
:
@[simp]
theorem
Learning.feedbackCondAction_obliviousEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨)
[hν : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)]
(n : ℕ)
:
noncomputable def
Learning.stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ProbabilityTheory.Kernel 𝓐 𝓨)
[ProbabilityTheory.IsMarkovKernel ν]
:
Environment Unit 𝓐 𝓨
A stationary environment without observations, in which the distribution of the next feedback depends only on the last action.
Equations
- Learning.stationaryEnv ν = Learning.obliviousEnv fun (x : ℕ) => ν
Instances For
@[simp]
theorem
Learning.obs_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ProbabilityTheory.Kernel 𝓐 𝓨)
[ProbabilityTheory.IsMarkovKernel ν]
(n : ℕ)
:
(stationaryEnv ν).obs n = ProbabilityTheory.Kernel.const (Hist Unit 𝓐 𝓨 n) (MeasureTheory.Measure.dirac ())
@[simp]
theorem
Learning.feedback_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ProbabilityTheory.Kernel 𝓐 𝓨)
[ProbabilityTheory.IsMarkovKernel ν]
(n : ℕ)
:
theorem
Learning.stepKernel_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(alg : Algorithm Unit 𝓐 𝓨)
(η : ProbabilityTheory.Kernel 𝓐 𝓨)
[ProbabilityTheory.IsMarkovKernel η]
(n : ℕ)
:
stepKernel alg (stationaryEnv η) n = (ProbabilityTheory.Kernel.const (Hist Unit 𝓐 𝓨 n) (MeasureTheory.Measure.dirac ())).compProd
((alg.policy n).compProd (ProbabilityTheory.Kernel.prodMkLeft (Hist Unit 𝓐 𝓨 n × Unit) η))
@[simp]
theorem
Learning.obs0_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ProbabilityTheory.Kernel 𝓐 𝓨)
[ProbabilityTheory.IsMarkovKernel ν]
:
@[simp]
theorem
Learning.ν0_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ProbabilityTheory.Kernel 𝓐 𝓨)
[ProbabilityTheory.IsMarkovKernel ν]
:
instance
Learning.instIsObliviousEnvUnitStationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ProbabilityTheory.Kernel 𝓐 𝓨)
[ProbabilityTheory.IsMarkovKernel ν]
:
@[simp]
theorem
Learning.feedbackCondAction_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
(ν : ProbabilityTheory.Kernel 𝓐 𝓨)
[hν : ProbabilityTheory.IsMarkovKernel ν]
(n : ℕ)
:
theorem
Learning.IsAlgEnvSeq.hasCondDistrib_feedback_obliviousEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm Unit 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
{ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨}
[∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)]
(h : IsAlgEnvSeq O A Y alg (obliviousEnv ν) P)
(n : ℕ)
:
ProbabilityTheory.HasCondDistrib (Y n) (A n) (ν n) P
The conditional distribution of the feedback at time n given the action at time n
is ν n.
theorem
Learning.IsAlgEnvSeq.hasCondDistrib_feedback_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm Unit 𝓐 𝓨}
{ν : ProbabilityTheory.Kernel 𝓐 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
(h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P)
(n : ℕ)
:
ProbabilityTheory.HasCondDistrib (Y n) (A n) ν P
The conditional distribution of the feedback at time n given the action at time n is ν.
theorem
Learning.IsAlgEnvSeq.condDistrib_feedback_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm Unit 𝓐 𝓨}
{ν : ProbabilityTheory.Kernel 𝓐 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
[StandardBorelSpace 𝓨]
[Nonempty 𝓨]
(h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P)
(n : ℕ)
:
⇑𝓛[Y n | A n; P] =ᵐ[MeasureTheory.Measure.map (A n) P] ⇑ν
The conditional distribution of the feedback at time n given the action at time n is ν.
theorem
Learning.IsAlgEnvSeq.hasLaw_feedback_cond_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm Unit 𝓐 𝓨}
{ν : ProbabilityTheory.Kernel 𝓐 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
(h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P)
(n : ℕ)
{s : Set ((Hist Unit 𝓐 𝓨 n × Unit) × 𝓐)}
(hs : MeasurableSet s)
{b : 𝓐}
(hsb : ∀ u ∈ s, u.2 = b)
(hP : P ((fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s) ≠ 0)
:
Conditionally on an event determined by the history before time n and the action at time
n, on which that action is equal to b, the feedback at time n has law ν b.
theorem
Learning.IsAlgEnvSeq.indepFun_history_action_feedback_cond_stationaryEnv
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm Unit 𝓐 𝓨}
{ν : ProbabilityTheory.Kernel 𝓐 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
(h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P)
(n : ℕ)
{s : Set ((Hist Unit 𝓐 𝓨 n × Unit) × 𝓐)}
(hs : MeasurableSet s)
{b : 𝓐}
(hsb : ∀ u ∈ s, u.2 = b)
:
Conditionally on an event determined by the history before time n and the action at time
n, on which that action is constant, the feedback at time n is independent of the
history before time n and of the action at time n.
theorem
Learning.IsAlgEnvSeq.condIndepFun_feedback_history_action
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm Unit 𝓐 𝓨}
{ν : ProbabilityTheory.Kernel 𝓐 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
[StandardBorelSpace Ω]
[StandardBorelSpace 𝓐]
[Nonempty 𝓐]
[StandardBorelSpace 𝓨]
[Nonempty 𝓨]
(h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P)
(n : ℕ)
:
ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (A n) inferInstance) ⋯ (Y n)
(fun (ω : Ω) => (history O A Y n ω, O n ω)) P
The feedback at time n is conditionally independent of the history before time n
given the action at time n.
theorem
Learning.IsAlgEnvSeq.condIndepFun_feedback_history_action_action
{𝓐 : Type u_2}
{𝓨 : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{Ω : Type u_4}
{mΩ : MeasurableSpace Ω}
{alg : Algorithm Unit 𝓐 𝓨}
{ν : ProbabilityTheory.Kernel 𝓐 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
[StandardBorelSpace Ω]
[StandardBorelSpace 𝓐]
[Nonempty 𝓐]
[StandardBorelSpace 𝓨]
[Nonempty 𝓨]
(h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P)
(n : ℕ)
:
ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (A n) inferInstance) ⋯ (Y n)
(fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω)) P