Transport of algorithms and environments

Main definitions

• Round.map fo fa fy, Hist.map fo fa fy: round-wise transport of a round and a history along maps of the observation, the action and the feedback, with the special cases mapObs, mapAction and mapFeedback that transport a single component.
• Algorithm.comap alg F hF: the algorithm that transforms the pair (past rounds, current observation) by the measurable map F n at round n before applying the policy of alg.
• Algorithm.comapObs alg f: the algorithm that sees f o when the observation is o, both in the current round and in the past rounds.
• Algorithm.comapFeedback alg g: the algorithm that sees g y when the feedback of a past round is y.
• Environment.comap env F hF f hf: the environment that reads the summary F n of the past rounds and reads f a when the algorithm plays a in the current round.
• Environment.comapAction env f: the environment that reads f a when the algorithm plays a, both in the current round and in the past rounds.
• Algorithm.congr alg e𝓞 e𝓐 e𝓨, Environment.congr env e𝓞 e𝓐 e𝓨: relabelling of the observations, the actions and the feedbacks of a player along measurable equivalences.

Main statements

• IsAlgEnvSeq.hasCondDistrib_action_comapObs, IsAlgEnvSeq.hasCondDistrib_action_comapFeedback: in a run of alg.comapObs f (resp. alg.comapFeedback g) against any environment, the conditional distribution of the action given the transported history and the transported observation is alg.policy n.
• IsAlgEnvSeq.hasCondDistrib_obs_comapAction, IsAlgEnvSeq.hasCondDistrib_feedback_comapAction: in a run against env.comapAction f, the observations and feedbacks have the conditional distributions of a run of env on the transported actions.

def Learning.Round.map {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} (fo : 𝓞 → 𝓞') (fa : 𝓐 → 𝓐') (fy : 𝓨 → 𝓨') (r : Round 𝓞 𝓐 𝓨) : Round 𝓞' 𝓐' 𝓨'

Transport a round along maps of the observation, the action and the feedback.

Equations

• Learning.Round.map fo fa fy r = (fo r.obs, fa r.action, fy r.feedback)

def Learning.Hist.map {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} (fo : 𝓞 → 𝓞') (fa : 𝓐 → 𝓐') (fy : 𝓨 → 𝓨') {n : ℕ} (h : Hist 𝓞 𝓐 𝓨 n) : Hist 𝓞' 𝓐' 𝓨' n

Transport a history round-wise.

Equations

• Learning.Hist.map fo fa fy h i = Learning.Round.map fo fa fy (h i)

@[simp]

theorem Learning.Round.obs_map {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {fo : 𝓞 → 𝓞'} {fa : 𝓐 → 𝓐'} {fy : 𝓨 → 𝓨'} (r : Round 𝓞 𝓐 𝓨) : (map fo fa fy r).obs = fo r.obs

@[simp]

theorem Learning.Round.action_map {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {fo : 𝓞 → 𝓞'} {fa : 𝓐 → 𝓐'} {fy : 𝓨 → 𝓨'} (r : Round 𝓞 𝓐 𝓨) : (map fo fa fy r).action = fa r.action

@[simp]

theorem Learning.Round.feedback_map {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {fo : 𝓞 → 𝓞'} {fa : 𝓐 → 𝓐'} {fy : 𝓨 → 𝓨'} (r : Round 𝓞 𝓐 𝓨) : (map fo fa fy r).feedback = fy r.feedback

@[simp]

theorem Learning.Hist.map_apply {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {fo : 𝓞 → 𝓞'} {fa : 𝓐 → 𝓐'} {fy : 𝓨 → 𝓨'} {n : ℕ} (h : Hist 𝓞 𝓐 𝓨 n) (i : Fin n) : map fo fa fy h i = Round.map fo fa fy (h i)

@[simp]

theorem Learning.Round.map_id {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} : map id id id = id

@[simp]

theorem Learning.Hist.map_id {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {n : ℕ} : map id id id = id

theorem Learning.Round.map_comp {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓞'' : Type u_3} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓐'' : Type u_6} {𝓨 : Type u_7} {𝓨' : Type u_8} {𝓨'' : Type u_9} {fo : 𝓞 → 𝓞'} {fa : 𝓐 → 𝓐'} {fy : 𝓨 → 𝓨'} {go : 𝓞' → 𝓞''} {ga : 𝓐' → 𝓐''} {gy : 𝓨' → 𝓨''} (r : Round 𝓞 𝓐 𝓨) : map go ga gy (map fo fa fy r) = map (go ∘ fo) (ga ∘ fa) (gy ∘ fy) r

theorem Learning.Hist.map_comp {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓞'' : Type u_3} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓐'' : Type u_6} {𝓨 : Type u_7} {𝓨' : Type u_8} {𝓨'' : Type u_9} {fo : 𝓞 → 𝓞'} {fa : 𝓐 → 𝓐'} {fy : 𝓨 → 𝓨'} {go : 𝓞' → 𝓞''} {ga : 𝓐' → 𝓐''} {gy : 𝓨' → 𝓨''} {n : ℕ} (h : Hist 𝓞 𝓐 𝓨 n) : map go ga gy (map fo fa fy h) = map (go ∘ fo) (ga ∘ fa) (gy ∘ fy) h

theorem Learning.Round.measurable_map {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {fo : 𝓞 → 𝓞'} {fa : 𝓐 → 𝓐'} {fy : 𝓨 → 𝓨'} (hfo : Measurable fo) (hfa : Measurable fa) (hfy : Measurable fy) : Measurable (map fo fa fy)

theorem Learning.Hist.measurable_map {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {fo : 𝓞 → 𝓞'} {fa : 𝓐 → 𝓐'} {fy : 𝓨 → 𝓨'} (hfo : Measurable fo) (hfa : Measurable fa) (hfy : Measurable fy) (n : ℕ) : Measurable (map fo fa fy)

@[reducible, inline]

abbrev Learning.Round.mapObs {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} (f : 𝓞 → 𝓞') (r : Round 𝓞 𝓐 𝓨) : Round 𝓞' 𝓐 𝓨

Transport the observations of a round.

Equations

• Learning.Round.mapObs f r = Learning.Round.map f id id r

@[reducible, inline]

abbrev Learning.Hist.mapObs {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} (f : 𝓞 → 𝓞') {n : ℕ} (h : Hist 𝓞 𝓐 𝓨 n) : Hist 𝓞' 𝓐 𝓨 n

Transport the observations of a history.

Equations

• Learning.Hist.mapObs f h = Learning.Hist.map f id id h

@[reducible, inline]

abbrev Learning.Round.mapAction {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} (f : 𝓐 → 𝓐') (r : Round 𝓞 𝓐 𝓨) : Round 𝓞 𝓐' 𝓨

Transport the actions of a round.

Equations

• Learning.Round.mapAction f r = Learning.Round.map id f id r

@[reducible, inline]

abbrev Learning.Hist.mapAction {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} (f : 𝓐 → 𝓐') {n : ℕ} (h : Hist 𝓞 𝓐 𝓨 n) : Hist 𝓞 𝓐' 𝓨 n

Transport the actions of a history.

Equations

• Learning.Hist.mapAction f h = Learning.Hist.map id f id h

@[reducible, inline]

abbrev Learning.Round.mapFeedback {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} (f : 𝓨 → 𝓨') (r : Round 𝓞 𝓐 𝓨) : Round 𝓞 𝓐 𝓨'

Transport the feedback of a round.

Equations

• Learning.Round.mapFeedback f r = Learning.Round.map id id f r

@[reducible, inline]

abbrev Learning.Hist.mapFeedback {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} (f : 𝓨 → 𝓨') {n : ℕ} (h : Hist 𝓞 𝓐 𝓨 n) : Hist 𝓞 𝓐 𝓨' n

Transport the feedback of a history.

Equations

• Learning.Hist.mapFeedback f h = Learning.Hist.map id id f h

def Learning.Algorithm.comap {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (alg : Algorithm 𝓞 𝓐 𝓨) (F : (n : ℕ) → Hist 𝓞' 𝓐 𝓨' n × 𝓞' → Hist 𝓞 𝓐 𝓨 n × 𝓞) (hF : ∀ (n : ℕ), Measurable (F n)) : Algorithm 𝓞' 𝓐 𝓨'

The algorithm with observations in 𝓞' and feedbacks in 𝓨' obtained from alg : Algorithm 𝓞 𝓐 𝓨 by transforming the pair (past rounds, current observation) by F n at each round n before applying the policy of alg.

This is the primitive transport operation on algorithms: Algorithm.comapObs and Algorithm.comapFeedback are the special cases in which F n is a round-wise map of the observation and of the feedback.

Equations

• alg.comap F hF = { policy := fun (n : ℕ) => (alg.policy n).comap (F n) ⋯, isMarkovKernel_policy := ⋯ }

@[simp]

theorem Learning.Algorithm.policy_comap {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (alg : Algorithm 𝓞 𝓐 𝓨) {F : (n : ℕ) → Hist 𝓞' 𝓐 𝓨' n × 𝓞' → Hist 𝓞 𝓐 𝓨 n × 𝓞} (hF : ∀ (n : ℕ), Measurable (F n)) (n : ℕ) : (alg.comap F hF).policy n = (alg.policy n).comap (F n) ⋯

@[simp]

theorem Learning.Algorithm.p0_comap {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (alg : Algorithm 𝓞 𝓐 𝓨) {F : (n : ℕ) → Hist 𝓞' 𝓐 𝓨' n × 𝓞' → Hist 𝓞 𝓐 𝓨 n × 𝓞} (hF : ∀ (n : ℕ), Measurable (F n)) : (alg.comap F hF).p0 = alg.p0.comap (fun (o : 𝓞') => (F 0 (default, o)).2) ⋯

@[simp]

theorem Learning.Algorithm.comap_id {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) : alg.comap (fun (x : ℕ) => id) ⋯ = alg

theorem Learning.Algorithm.comap_comap {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓞'' : Type u_3} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {𝓨'' : Type u_9} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓞'' : MeasurableSpace 𝓞''} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {m𝓨'' : MeasurableSpace 𝓨''} (alg : Algorithm 𝓞 𝓐 𝓨) {F : (n : ℕ) → Hist 𝓞' 𝓐 𝓨' n × 𝓞' → Hist 𝓞 𝓐 𝓨 n × 𝓞} (hF : ∀ (n : ℕ), Measurable (F n)) {G : (n : ℕ) → Hist 𝓞'' 𝓐 𝓨'' n × 𝓞'' → Hist 𝓞' 𝓐 𝓨' n × 𝓞'} (hG : ∀ (n : ℕ), Measurable (G n)) : (alg.comap F hF).comap G hG = alg.comap (fun (n : ℕ) => F n ∘ G n) ⋯

def Learning.Algorithm.comapObs {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (f : 𝓞' → 𝓞) (hf : Measurable f := by fun_prop) : Algorithm 𝓞' 𝓐 𝓨

The algorithm that sees f o when the observation is o, both in the current round and in the past rounds.

Equations

• alg.comapObs f hf = alg.comap (fun (x : ℕ) (p : Learning.Hist 𝓞' 𝓐 𝓨 x × 𝓞') => (Learning.Hist.mapObs f p.1, f p.2)) ⋯

theorem Learning.Algorithm.comapObs_def {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓞' → 𝓞} (alg : Algorithm 𝓞 𝓐 𝓨) (hf : Measurable f) : alg.comapObs f hf = alg.comap (fun (x : ℕ) (p : Hist 𝓞' 𝓐 𝓨 x × 𝓞') => (Hist.mapObs f p.1, f p.2)) ⋯

@[simp]

theorem Learning.Algorithm.policy_comapObs {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓞' → 𝓞} (alg : Algorithm 𝓞 𝓐 𝓨) (hf : Measurable f) (n : ℕ) : (alg.comapObs f hf).policy n = (alg.policy n).comap (fun (p : Hist 𝓞' 𝓐 𝓨 n × 𝓞') => (Hist.mapObs f p.1, f p.2)) ⋯

@[simp]

theorem Learning.Algorithm.p0_comapObs {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓞' → 𝓞} (alg : Algorithm 𝓞 𝓐 𝓨) (hf : Measurable f) : (alg.comapObs f hf).p0 = alg.p0.comap f hf

@[simp]

theorem Learning.Algorithm.comapObs_id {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) : alg.comapObs id ⋯ = alg

theorem Learning.Algorithm.comapObs_comapObs {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓞'' : Type u_3} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓞'' : MeasurableSpace 𝓞''} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓞' → 𝓞} (alg : Algorithm 𝓞 𝓐 𝓨) (hf : Measurable f) {g : 𝓞'' → 𝓞'} (hg : Measurable g) : (alg.comapObs f hf).comapObs g hg = alg.comapObs (f ∘ g) ⋯

def Learning.Algorithm.comapFeedback {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (alg : Algorithm 𝓞 𝓐 𝓨) (g : 𝓨' → 𝓨) (hg : Measurable g := by fun_prop) : Algorithm 𝓞 𝓐 𝓨'

The algorithm that sees g y when the feedback of a past round is y.

Equations

• alg.comapFeedback g hg = alg.comap (fun (x : ℕ) (p : Learning.Hist 𝓞 𝓐 𝓨' x × 𝓞) => (Learning.Hist.mapFeedback g p.1, p.2)) ⋯

theorem Learning.Algorithm.comapFeedback_def {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {g : 𝓨' → 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (hg : Measurable g) : alg.comapFeedback g hg = alg.comap (fun (x : ℕ) (p : Hist 𝓞 𝓐 𝓨' x × 𝓞) => (Hist.mapFeedback g p.1, p.2)) ⋯

@[simp]

theorem Learning.Algorithm.policy_comapFeedback {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {g : 𝓨' → 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (hg : Measurable g) (n : ℕ) : (alg.comapFeedback g hg).policy n = (alg.policy n).comap (fun (p : Hist 𝓞 𝓐 𝓨' n × 𝓞) => (Hist.mapFeedback g p.1, p.2)) ⋯

@[simp]

theorem Learning.Algorithm.p0_comapFeedback {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {g : 𝓨' → 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (hg : Measurable g) : (alg.comapFeedback g hg).p0 = alg.p0

@[simp]

theorem Learning.Algorithm.comapFeedback_id {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) : alg.comapFeedback id ⋯ = alg

theorem Learning.Algorithm.comapFeedback_comapFeedback {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {𝓨'' : Type u_9} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {m𝓨'' : MeasurableSpace 𝓨''} (alg : Algorithm 𝓞 𝓐 𝓨) {g : 𝓨' → 𝓨} (hg : Measurable g) {g' : 𝓨'' → 𝓨'} (hg' : Measurable g') : (alg.comapFeedback g hg).comapFeedback g' hg' = alg.comapFeedback (g ∘ g') ⋯

theorem Learning.Algorithm.comapObs_comapFeedback_comm {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (alg : Algorithm 𝓞 𝓐 𝓨) {f : 𝓞' → 𝓞} (hf : Measurable f) {g : 𝓨' → 𝓨} (hg : Measurable g) : (alg.comapFeedback g hg).comapObs f hf = (alg.comapObs f hf).comapFeedback g hg

Transporting the observations and the feedbacks of an algorithm are independent operations.

def Learning.Environment.comap {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) (F : (n : ℕ) → Hist 𝓞 𝓐' 𝓨 n → Hist 𝓞 𝓐 𝓨 n) (hF : ∀ (n : ℕ), Measurable (F n)) (f : 𝓐' → 𝓐) (hf : Measurable f) : Environment 𝓞 𝓐' 𝓨

The environment that reads the summary F n of the past rounds and reads f a when the algorithm plays a in the current round.

This is the primitive transport operation on environments, dual to Algorithm.comap: Environment.comapAction is the special case in which F n is the round-wise map of the actions. Only the action can change type, since the observations and the feedbacks are outputs of the environment; F n can nonetheless forget or summarize the past rounds, as an environment that reads only the last round does.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Learning.Environment.obs_comap {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {F : (n : ℕ) → Hist 𝓞 𝓐' 𝓨 n → Hist 𝓞 𝓐 𝓨 n} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ (n : ℕ), Measurable (F n)) (hf : Measurable f) (n : ℕ) : (env.comap F hF f hf).obs n = (env.obs n).comap (F n) ⋯

@[simp]

theorem Learning.Environment.feedback_comap {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {F : (n : ℕ) → Hist 𝓞 𝓐' 𝓨 n → Hist 𝓞 𝓐 𝓨 n} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ (n : ℕ), Measurable (F n)) (hf : Measurable f) (n : ℕ) : (env.comap F hF f hf).feedback n = (env.feedback n).comap (fun (p : (Hist 𝓞 𝓐' 𝓨 n × 𝓞) × 𝓐') => ((F n p.1.1, p.1.2), f p.2)) ⋯

@[simp]

theorem Learning.Environment.obs0_comap {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {F : (n : ℕ) → Hist 𝓞 𝓐' 𝓨 n → Hist 𝓞 𝓐 𝓨 n} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ (n : ℕ), Measurable (F n)) (hf : Measurable f) : (env.comap F hF f hf).obs0 = env.obs0

@[simp]

theorem Learning.Environment.ν0_comap {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {F : (n : ℕ) → Hist 𝓞 𝓐' 𝓨 n → Hist 𝓞 𝓐 𝓨 n} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ (n : ℕ), Measurable (F n)) (hf : Measurable f) : (env.comap F hF f hf).ν0 = env.ν0.comap (fun (p : 𝓞 × 𝓐') => (p.1, f p.2)) ⋯

@[simp]

theorem Learning.Environment.comap_id {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) : env.comap (fun (x : ℕ) => id) ⋯ id ⋯ = env

theorem Learning.Environment.comap_comp {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓐'' : Type u_6} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓐'' : MeasurableSpace 𝓐''} {m𝓨 : MeasurableSpace 𝓨} {F : (n : ℕ) → Hist 𝓞 𝓐' 𝓨 n → Hist 𝓞 𝓐 𝓨 n} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ (n : ℕ), Measurable (F n)) (hf : Measurable f) {G : (n : ℕ) → Hist 𝓞 𝓐'' 𝓨 n → Hist 𝓞 𝓐' 𝓨 n} (hG : ∀ (n : ℕ), Measurable (G n)) {g : 𝓐'' → 𝓐'} (hg : Measurable g) : (env.comap F hF f hf).comap G hG g hg = env.comap (fun (n : ℕ) => F n ∘ G n) ⋯ (f ∘ g) ⋯

def Learning.Environment.comapAction {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) (f : 𝓐' → 𝓐) (hf : Measurable f := by fun_prop) : Environment 𝓞 𝓐' 𝓨

The environment that reads f a when the algorithm plays a, both in the current round and in the past rounds.

Equations

• env.comapAction f hf = env.comap (fun (x : ℕ) => Learning.Hist.mapAction f) ⋯ f hf

theorem Learning.Environment.comapAction_def {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) (f : 𝓐' → 𝓐) (hf : Measurable f) : env.comapAction f hf = env.comap (fun (x : ℕ) => Hist.mapAction f) ⋯ f hf

@[simp]

theorem Learning.Environment.obs_comapAction {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hf : Measurable f) (n : ℕ) : (env.comapAction f hf).obs n = (env.obs n).comap (Hist.mapAction f) ⋯

@[simp]

theorem Learning.Environment.feedback_comapAction {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hf : Measurable f) (n : ℕ) : (env.comapAction f hf).feedback n = (env.feedback n).comap (fun (p : (Hist 𝓞 𝓐' 𝓨 n × 𝓞) × 𝓐') => ((Hist.mapAction f p.1.1, p.1.2), f p.2)) ⋯

@[simp]

theorem Learning.Environment.obs0_comapAction {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hf : Measurable f) : (env.comapAction f hf).obs0 = env.obs0

@[simp]

theorem Learning.Environment.ν0_comapAction {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hf : Measurable f) : (env.comapAction f hf).ν0 = env.ν0.comap (fun (p : 𝓞 × 𝓐') => (p.1, f p.2)) ⋯

@[simp]

theorem Learning.Environment.comapAction_id {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) : env.comapAction id ⋯ = env

theorem Learning.Environment.comapAction_comp {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓐'' : Type u_6} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓐'' : MeasurableSpace 𝓐''} {m𝓨 : MeasurableSpace 𝓨} {f : 𝓐' → 𝓐} (env : Environment 𝓞 𝓐 𝓨) (hf : Measurable f) (g : 𝓐'' → 𝓐') (hg : Measurable g) : (env.comapAction f hf).comapAction g hg = env.comapAction (f ∘ g) ⋯

noncomputable def Learning.Algorithm.congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (alg : Algorithm 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') : Algorithm 𝓞' 𝓐' 𝓨'

Relabelling of the observations, the actions and the feedbacks of an algorithm along measurable equivalences.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Learning.Algorithm.policy_congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (alg : Algorithm 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') (n : ℕ) : (alg.congr e𝓞 e𝓐 e𝓨).policy n = ((alg.policy n).map ⇑e𝓐).comap (fun (p : Hist 𝓞' 𝓐' 𝓨' n × 𝓞') => (Hist.map (⇑e𝓞.symm) (⇑e𝓐.symm) (⇑e𝓨.symm) p.1, e𝓞.symm p.2)) ⋯

@[simp]

theorem Learning.Algorithm.p0_congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (alg : Algorithm 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') : (alg.congr e𝓞 e𝓐 e𝓨).p0 = (alg.p0.map ⇑e𝓐).comap ⇑e𝓞.symm ⋯

@[simp]

theorem Learning.Algorithm.congr_refl {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) : alg.congr (MeasurableEquiv.refl 𝓞) (MeasurableEquiv.refl 𝓐) (MeasurableEquiv.refl 𝓨) = alg

theorem Learning.Algorithm.congr_congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓞'' : Type u_3} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓐'' : Type u_6} {𝓨 : Type u_7} {𝓨' : Type u_8} {𝓨'' : Type u_9} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓞'' : MeasurableSpace 𝓞''} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓐'' : MeasurableSpace 𝓐''} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {m𝓨'' : MeasurableSpace 𝓨''} (alg : Algorithm 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') (f𝓞 : 𝓞' ≃ᵐ 𝓞'') (f𝓐 : 𝓐' ≃ᵐ 𝓐'') (f𝓨 : 𝓨' ≃ᵐ 𝓨'') : (alg.congr e𝓞 e𝓐 e𝓨).congr f𝓞 f𝓐 f𝓨 = alg.congr (e𝓞.trans f𝓞) (e𝓐.trans f𝓐) (e𝓨.trans f𝓨)

@[simp]

theorem Learning.Algorithm.congr_symm {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (alg : Algorithm 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') : (alg.congr e𝓞 e𝓐 e𝓨).congr e𝓞.symm e𝓐.symm e𝓨.symm = alg

noncomputable def Learning.Environment.congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') : Environment 𝓞' 𝓐' 𝓨'

Relabelling of the observations, the actions and the feedbacks of an environment along measurable equivalences. See also Algorithm.congr.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Learning.Environment.obs_congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') (n : ℕ) : (env.congr e𝓞 e𝓐 e𝓨).obs n = ((env.obs n).map ⇑e𝓞).comap (Hist.map ⇑e𝓞.symm ⇑e𝓐.symm ⇑e𝓨.symm) ⋯

@[simp]

theorem Learning.Environment.feedback_congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') (n : ℕ) : (env.congr e𝓞 e𝓐 e𝓨).feedback n = ((env.feedback n).map ⇑e𝓨).comap (fun (p : (Hist 𝓞' 𝓐' 𝓨' n × 𝓞') × 𝓐') => ((Hist.map (⇑e𝓞.symm) (⇑e𝓐.symm) (⇑e𝓨.symm) p.1.1, e𝓞.symm p.1.2), e𝓐.symm p.2)) ⋯

@[simp]

theorem Learning.Environment.obs0_congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') : (env.congr e𝓞 e𝓐 e𝓨).obs0 = MeasureTheory.Measure.map (⇑e𝓞) env.obs0

@[simp]

theorem Learning.Environment.ν0_congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') : (env.congr e𝓞 e𝓐 e𝓨).ν0 = (env.ν0.map ⇑e𝓨).comap (fun (p : 𝓞' × 𝓐') => (e𝓞.symm p.1, e𝓐.symm p.2)) ⋯

@[simp]

theorem Learning.Environment.congr_refl {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) : env.congr (MeasurableEquiv.refl 𝓞) (MeasurableEquiv.refl 𝓐) (MeasurableEquiv.refl 𝓨) = env

theorem Learning.Environment.congr_congr {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓞'' : Type u_3} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓐'' : Type u_6} {𝓨 : Type u_7} {𝓨' : Type u_8} {𝓨'' : Type u_9} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓞'' : MeasurableSpace 𝓞''} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓐'' : MeasurableSpace 𝓐''} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {m𝓨'' : MeasurableSpace 𝓨''} (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') (f𝓞 : 𝓞' ≃ᵐ 𝓞'') (f𝓐 : 𝓐' ≃ᵐ 𝓐'') (f𝓨 : 𝓨' ≃ᵐ 𝓨'') : (env.congr e𝓞 e𝓐 e𝓨).congr f𝓞 f𝓐 f𝓨 = env.congr (e𝓞.trans f𝓞) (e𝓐.trans f𝓐) (e𝓨.trans f𝓨)

@[simp]

theorem Learning.Environment.congr_symm {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {𝓨' : Type u_8} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐') (e𝓨 : 𝓨 ≃ᵐ 𝓨') : (env.congr e𝓞 e𝓐 e𝓨).congr e𝓞.symm e𝓐.symm e𝓨.symm = env

theorem Learning.IsAlgEnvSeq.hasCondDistrib_action_comapObs {𝓞 : Type u_1} {𝓞' : Type u_2} {𝓐 : Type u_4} {𝓨 : Type u_7} {Ω : Type u_10} {m𝓞 : MeasurableSpace 𝓞} {m𝓞' : MeasurableSpace 𝓞'} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞' 𝓐 𝓨} {f : 𝓞' → 𝓞} {hf : Measurable f} {O : ℕ → Ω → 𝓞'} (h : IsAlgEnvSeq O A Y (alg.comapObs f hf) env P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (A n) (fun (ω : Ω) => (history (fun (n : ℕ) (ω : Ω) => f (O n ω)) A Y n ω, f (O n ω))) (alg.policy n) P

The algorithm does not use the part of the observation that it ignores: the conditional distribution of its action given the transported history and observation is its own policy.

theorem Learning.IsAlgEnvSeq.hasCondDistrib_action_comapFeedback {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓨 : Type u_7} {𝓨' : Type u_8} {Ω : Type u_10} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓨' : MeasurableSpace 𝓨'} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {A : ℕ → Ω → 𝓐} {env : Environment 𝓞 𝓐 𝓨'} {g : 𝓨' → 𝓨} {hg : Measurable g} {O : ℕ → Ω → 𝓞} {Y' : ℕ → Ω → 𝓨'} (h : IsAlgEnvSeq O A Y' (alg.comapFeedback g hg) env P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (A n) (fun (ω : Ω) => (history O A (fun (n : ℕ) (ω : Ω) => g (Y' n ω)) n ω, O n ω)) (alg.policy n) P

The algorithm does not use the part of the past feedbacks that it ignores: the conditional distribution of its action given the transported history and the observation is its own policy.

theorem Learning.IsAlgEnvSeq.hasCondDistrib_obs_comapAction {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {Ω : Type u_10} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} {f : 𝓐' → 𝓐} {hf : Measurable f} {O : ℕ → Ω → 𝓞} {A' : ℕ → Ω → 𝓐'} {alg : Algorithm 𝓞 𝓐' 𝓨} (h : IsAlgEnvSeq O A' Y alg (env.comapAction f hf) P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (O n) (history O (fun (n : ℕ) (ω : Ω) => f (A' n ω)) Y n) (env.obs n) P

The environment does not use the part of the action that it ignores: the conditional distribution of the observation given the transported history is its own observation kernel.

theorem Learning.IsAlgEnvSeq.hasCondDistrib_feedback_comapAction {𝓞 : Type u_1} {𝓐 : Type u_4} {𝓐' : Type u_5} {𝓨 : Type u_7} {Ω : Type u_10} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓐' : MeasurableSpace 𝓐'} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} {f : 𝓐' → 𝓐} {hf : Measurable f} {O : ℕ → Ω → 𝓞} {A' : ℕ → Ω → 𝓐'} {alg : Algorithm 𝓞 𝓐' 𝓨} (h : IsAlgEnvSeq O A' Y alg (env.comapAction f hf) P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (Y n) (fun (ω : Ω) => ((history O (fun (n : ℕ) (ω : Ω) => f (A' n ω)) Y n ω, O n ω), f (A' n ω))) (env.feedback n) P

The environment does not use the part of the action that it ignores: the conditional distribution of the feedback given the transported history, the observation and the transported action is its own feedback kernel.