Algorithm density

We define a density function that allows obtaining the law of the history under one algorithm from the law of the history under another algorithm when they are interacting with the same environment. This also requires one algorithm to be absolutely continuous with respect to another, a concept that we also introduce here.

Main definitions

• AbsolutelyContinuous alg alg₀: alg is absolutely continuous with respect to alg₀ (also denoted alg ≪ₐ alg₀) when, in every situation, a set of actions with probability zero under alg₀ also has probability zero under alg. Intuitively, alg never acts in a way that alg₀ would never act.
• density alg alg₀ n: a density function that allows obtaining the law of the history at time n under alg from the law of the history at time n under alg₀ when they are interacting with the same environment and alg ≪ₐ alg₀.

Main results

• absolutelyContinuous_map_hist: the law of the history at time n under alg is absolutely continuous with respect to the law of the history at time n under alg₀ when they are interacting with the same environment and alg ≪ₐ alg₀.
• hasLaw_history_withDensity: the law of the history at time n under alg is the law of the history at time n under alg₀ with density alg.density alg₀ n when they are interacting with the same environment and alg ≪ₐ alg₀.

structure Learning.Algorithm.AbsolutelyContinuous {𝓐 : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] (alg alg₀ : Algorithm 𝓐 𝓨) : Prop

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₀.

• p0 : alg.p0.AbsolutelyContinuous alg₀.p0
• policy (n : ℕ) (h : ↥(Finset.Iic n) → 𝓐 × 𝓨) : ((alg.policy n) h).AbsolutelyContinuous ((alg₀.policy n) h)

def Learning.Algorithm.«term_≪ₐ_» : Lean.TrailingParserDescr

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₀.

Equations

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

noncomputable def Learning.Algorithm.density {𝓐 : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace.CountablyGenerated 𝓐] (alg alg₀ : Algorithm 𝓐 𝓨) (n : ℕ) : (↥(Finset.Iic n) → 𝓐 × 𝓨) → ENNReal

If the algorithm alg is absolutely continuous with respect to the algorithm alg₀ and they are both interacting with the same environment, then the law of the history at time n under alg is the law of the history at time n under alg₀ with density alg.density alg₀ n.

Equations

• One or more equations did not get rendered due to their size.
• alg.density alg₀ 0 h = alg.p0.rnDeriv alg₀.p0 (h ⟨0, Learning.Algorithm.density._proof_3⟩).1

theorem Learning.Algorithm.measurable_density {𝓐 : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace.CountablyGenerated 𝓐] (alg alg₀ : Algorithm 𝓐 𝓨) (n : ℕ) : Measurable (alg.density alg₀ n)

theorem Learning.IsAlgEnvSeq.absolutelyContinuous_map_history {𝓐 : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] {Ω : Type u_3} [MeasurableSpace Ω] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {Ω₀ : Type u_4} [MeasurableSpace Ω₀] {alg₀ : Algorithm 𝓐 𝓨} {A₀ : ℕ → Ω₀ → 𝓐} {Y₀ : ℕ → Ω₀ → 𝓨} {P₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure P₀] (h : IsAlgEnvSeq A Y alg env P) (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg.AbsolutelyContinuous alg₀) (n : ℕ) : (MeasureTheory.Measure.map (history A Y n) P).AbsolutelyContinuous (MeasureTheory.Measure.map (history A₀ Y₀ n) P₀)

theorem Learning.IsAlgEnvSeq.hasLaw_history_withDensity {𝓐 : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] {Ω : Type u_3} [MeasurableSpace Ω] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {Ω₀ : Type u_4} [MeasurableSpace Ω₀] {alg₀ : Algorithm 𝓐 𝓨} {A₀ : ℕ → Ω₀ → 𝓐} {Y₀ : ℕ → Ω₀ → 𝓨} {P₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure P₀] (h : IsAlgEnvSeq A Y alg env P) (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg.AbsolutelyContinuous alg₀) (n : ℕ) : ProbabilityTheory.HasLaw (history A Y n) ((MeasureTheory.Measure.map (history A₀ Y₀ n) P₀).withDensity (alg.density alg₀ n)) P