The means of the feedback distribution

Main definitions

• Environment.means

Main results

theorem ProbabilityTheory.HasCondDistrib.condExp_comp_eq {Ω : Type u_1} {β : Type u_2} {𝓨 : Type u_3} {mΩ : MeasurableSpace Ω} {mβ : MeasurableSpace β} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {X : Ω → β} {Y : Ω → 𝓨} {κ : Kernel β 𝓨} [IsFiniteKernel κ] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (h : HasCondDistrib Y X κ P) (hX : Measurable X) {g : 𝓨 → F} (hg : MeasureTheory.StronglyMeasurable g) (hint : MeasureTheory.Integrable (fun (ω : Ω) => g (Y ω)) P) : P[fun (ω : Ω) => g (Y ω) | MeasurableSpace.comap X mβ] =ᵐ[P] fun (ω : Ω) => ∫ (y : 𝓨), g y ∂κ (X ω)

noncomputable def Learning.Environment.measure {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : ProbabilityTheory.Kernel 𝓐 𝓨

The kernel that gives the measure of the feedback distribution as a function of the action chosen at time n.

Equations

• env.measure O A Y n ω = (env.feedback n).sectR (Learning.history O A Y n ω, O n ω)

noncomputable def Learning.Environment.means {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (k : 𝓐) (n : ℕ) (ω : Ω) : 𝓨

The means of the feedback distribution as a function of the action chosen at time n.

Equations

• env.means O A Y k n ω = ∫ (x : 𝓨), id x ∂(env.measure O A Y n ω) k

@[simp]

theorem Learning.means_zero {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (k : 𝓐) (ω : Ω) : env.means O A Y k 0 ω = ∫ (x : 𝓨), id x ∂env.ν0 (O 0 ω, k)

@[simp]

theorem Learning.means_of_isObliviousEnv {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {env : Environment 𝓞 𝓐 𝓨} [IsObliviousEnv env] (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (k : 𝓐) (n : ℕ) (ω : Ω) : env.means O A Y k n ω = ∫ (x : 𝓨), id x ∂(feedbackCondAction env n) k

theorem Learning.means_obliviousEnv {Ω : Type u_1} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] (ν : ℕ → ProbabilityTheory.Kernel 𝓐 𝓨) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)] {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (k : 𝓐) (n : ℕ) (ω : Ω) : (obliviousEnv ν).means O A Y k n ω = ∫ (x : 𝓨), id x ∂(ν n) k

theorem Learning.means_stationaryEnv {Ω : Type u_1} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] (ν : ProbabilityTheory.Kernel 𝓐 𝓨) [ProbabilityTheory.IsMarkovKernel ν] {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (k : 𝓐) (n : ℕ) (ω : Ω) : (stationaryEnv ν).means O A Y k n ω = ∫ (x : 𝓨), id x ∂ν k

theorem Learning.IsAlgEnvSeq.stronglyMeasurable_means {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [SecondCountableTopology 𝓨] [OpensMeasurableSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) (n : ℕ) : MeasureTheory.StronglyMeasurable (env.means O A Y k n)

theorem Learning.IsAlgEnvSeq.measurable_means {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) (n : ℕ) : Measurable (env.means O A Y k n)

theorem Learning.IsAlgEnvSeq.adapted_means_filtrationAction {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtrationAction fun (n : ℕ) (ω : Ω) => env.means O A Y (A n ω) n ω

theorem Learning.IsAlgEnvSeq.stronglyAdapted_means_filtrationAction {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.StronglyAdapted h.filtrationAction fun (n : ℕ) (ω : Ω) => env.means O A Y (A n ω) n ω

theorem Learning.IsAlgEnvSeq.adapted_means {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtration fun (n : ℕ) (ω : Ω) => env.means O A Y (A n ω) n ω

theorem Learning.IsAlgEnvSeq.condExp_feedback_comp {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {𝓩 : Type u_5} [NormedAddCommGroup 𝓩] [NormedSpace ℝ 𝓩] [CompleteSpace 𝓩] [StandardBorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) {g : 𝓨 → 𝓩} (hg : MeasureTheory.StronglyMeasurable g) (hint : MeasureTheory.Integrable (fun (ω : Ω) => g (Y n ω)) P) : P[fun (ω : Ω) => g (Y n ω) | ↑h.filtrationAction n] =ᵐ[P] fun (ω : Ω) => ∫ (x : 𝓨), g x ∂(env.feedback n) ((history O A Y n ω, O n ω), A n ω)

theorem Learning.IsAlgEnvSeq.condExp_feedback {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [BorelSpace 𝓨] [SecondCountableTopology 𝓨] [CompleteSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) (hint : MeasureTheory.Integrable (Y n) P) : P[Y n | ↑h.filtrationAction n] =ᵐ[P] fun (ω : Ω) => env.means O A Y (A n ω) n ω

theorem Learning.IsAlgEnvSeq.memLp_means_action {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) {n : ℕ} {p : ENNReal} (hp1 : 1 ≤ p) (hp_top : p ≠ ⊤) (hint : MeasureTheory.MemLp (Y n) p P) : MeasureTheory.MemLp (fun (ω : Ω) => env.means O A Y (A n ω) n ω) p P

theorem Learning.IsAlgEnvSeq.integrable_means_action {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [SecondCountableTopology 𝓨] [OpensMeasurableSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) {n : ℕ} (hint : MeasureTheory.Integrable (Y n) P) : MeasureTheory.Integrable (fun (ω : Ω) => env.means O A Y (A n ω) n ω) P