Function evaluation environments

We define two environments, onlineEvalEnv and evalEnv, where the feedback is given by evaluating a measurable function at the chosen action. The first one allows the function to change at every time step, while the second one uses a fixed function at every time step.

Main definitions

• onlineEvalEnv g hg: A stationary environment where the feedback at time n is given by a deterministic kernel that evaluates the measurable function g n at the chosen action.
• evalEnv f hf: A stationary environment where the feedback is given by a deterministic kernel that evaluates a fixed measurable function f at the chosen action.

They both satisfy the typeclasses IsObliviousEnv and IsDeterministicEnv.

Main statements

• forall_feedback_onlineEvalEnv_ae_eq_eval_action: For almost all ω, the feedback at time n is equal to g n evaluated at the action taken at time n.
• forall_feedback_evalEnv_ae_eq_eval_action: For almost all ω, the feedback at time n is equal to f evaluated at the action taken at time n.

noncomputable def Learning.onlineEvalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (g : ℕ → 𝓐 → 𝓨) (hg : ∀ (n : ℕ), Measurable (g n)) : Environment 𝓐 𝓨

The evaluation environment where the feedback is given by evaluating a fixed measurable function f at the chosen action.

Equations

• Learning.onlineEvalEnv g hg = Learning.obliviousEnv fun (n : ℕ) => ProbabilityTheory.Kernel.deterministic (g n) ⋯

instance Learning.instIsObliviousEnvOnlineEvalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {g : ℕ → 𝓐 → 𝓨} {hg : ∀ (n : ℕ), Measurable (g n)} : IsObliviousEnv (onlineEvalEnv g hg)

instance Learning.instIsDeterministicEnvOnlineEvalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {g : ℕ → 𝓐 → 𝓨} {hg : ∀ (n : ℕ), Measurable (g n)} : IsDeterministicEnv (onlineEvalEnv g hg)

@[simp]

theorem Learning.feedbackCondAction_onlineEvalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {g : ℕ → 𝓐 → 𝓨} {hg : ∀ (n : ℕ), Measurable (g n)} (n : ℕ) : feedbackCondAction (onlineEvalEnv g hg) n = ProbabilityTheory.Kernel.deterministic (g n) ⋯

@[simp]

theorem Learning.feedbackFunZero_onlineEvalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {g : ℕ → 𝓐 → 𝓨} {hg : ∀ (n : ℕ), Measurable (g n)} [MeasurableSpace.SeparatesPoints 𝓨] : feedbackFunZero (onlineEvalEnv g hg) = g 0

@[simp]

theorem Learning.feedbackFun_onlineEvalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {g : ℕ → 𝓐 → 𝓨} {hg : ∀ (n : ℕ), Measurable (g n)} [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) : feedbackFun (onlineEvalEnv g hg) n = fun (p : (↥(Finset.Iic n) → 𝓐 × 𝓨) × 𝓐) => g (n + 1) p.2

theorem Learning.hascondDistrib_feedback_onlineEvalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {g : ℕ → 𝓐 → 𝓨} {hg : ∀ (n : ℕ), Measurable (g n)} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (Y n) (A n) (ProbabilityTheory.Kernel.deterministic (g n) ⋯) P

theorem Learning.feedback_onlineEvalEnv_ae_eq_eval_action {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {g : ℕ → 𝓐 → 𝓨} {hg : ∀ (n : ℕ), Measurable (g n)} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) (n : ℕ) : Y n =ᵐ[P] g n ∘ A n

theorem Learning.forall_feedback_onlineEvalEnv_ae_eq_eval_action {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {g : ℕ → 𝓐 → 𝓨} {hg : ∀ (n : ℕ), Measurable (g n)} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), Y n ω = g n (A n ω)

noncomputable def Learning.evalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (f : 𝓐 → 𝓨) (hf : Measurable f) : Environment 𝓐 𝓨

The evaluation environment where the feedback is given by evaluating a fixed measurable function f at the chosen action.

Equations

• Learning.evalEnv f hf = Learning.onlineEvalEnv (fun (x : ℕ) => f) ⋯

instance Learning.instIsObliviousEnvEvalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} : IsObliviousEnv (evalEnv f hf)

instance Learning.instIsDeterministicEnvEvalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} : IsDeterministicEnv (evalEnv f hf)

@[simp]

theorem Learning.feedbackCondAction_evalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} (n : ℕ) : feedbackCondAction (evalEnv f hf) n = ProbabilityTheory.Kernel.deterministic f hf

@[simp]

theorem Learning.feedbackFunZero_evalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} [MeasurableSpace.SeparatesPoints 𝓨] : feedbackFunZero (evalEnv f hf) = f

@[simp]

theorem Learning.feedbackFun_evalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) : feedbackFun (evalEnv f hf) n = fun (p : (↥(Finset.Iic n) → 𝓐 × 𝓨) × 𝓐) => f p.2

theorem Learning.hascondDistrib_feedback_evalEnv {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (Y n) (A n) (ProbabilityTheory.Kernel.deterministic f hf) P

theorem Learning.feedback_evalEnv_ae_eq_eval_action {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) (n : ℕ) : Y n =ᵐ[P] f ∘ A n

theorem Learning.forall_feedback_evalEnv_ae_eq_eval_action {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), Y n ω = f (A n ω)

theorem Learning.feedback_evalEnv_ae_eq_eval_action_comp {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {β : Type u_4} (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) {n : ℕ} (g : (↥(Finset.Iic n) → 𝓨) → β) : ∀ᵐ (ω : Ω) ∂P, (g fun (i : ↥(Finset.Iic n)) => Y (↑i) ω) = g fun (i : ↥(Finset.Iic n)) => f (A (↑i) ω)