3.9. SequentialLearning.AlgorithmDensity🔗

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

Module LeanMachineLearning.SequentialLearning.AlgorithmDensity contains 6 exposed declarations.

`AbsolutelyContinuous`🔗

StructureLearning.Algorithm.AbsolutelyContinuous

Details

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

structure

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

Code

structure AbsolutelyContinuous (alg alg₀ : Algorithm 𝓐 𝓨) : Prop where
  p0 : alg.p0 ≪ alg₀.p0
  policy n h : alg.policy n h ≪ alg₀.policy n h

Type uses (1)

Algorithm

Used by (7)

Actions: Source · Open Issue

`term_≪ₐ_`🔗

DefinitionLearning.Algorithm.«term_≪ₐ_»

Details

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

def

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

Code

scoped notation:50 alg " ≪ₐ " alg₀ => AbsolutelyContinuous alg alg₀

Body uses (1)

AbsolutelyContinuous

Actions: Source · Open Issue

`density`🔗

DefinitionLearning.Algorithm.density

Details

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.

def

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

Code

noncomputable
def density [MeasurableSpace.CountablyGenerated 𝓐] (alg alg₀ : Algorithm 𝓐 𝓨) :
    (n : ℕ) → (Iic n → 𝓐 × 𝓨) → ℝ≥0∞
  | 0, h => (alg.p0.rnDeriv alg₀.p0 (h ⟨0, by simp⟩).1)
  | n + 1, h =>
    let p := MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n h
    alg.density alg₀ n p.1 * (alg.policy n).rnDeriv (alg₀.policy n) p.1 p.2.1

Type uses (1)

Algorithm

Body uses (1)

IicSuccProd

Used by (5)

Actions: Source · Open Issue

`measurable_density`🔗

LemmaLearning.Algorithm.measurable_density

Details

No docstring.

theorem

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

Code

lemma measurable_density [MeasurableSpace.CountablyGenerated 𝓐] (alg alg₀ : Algorithm 𝓐 𝓨) (n : ℕ) :
    Measurable (alg.density alg₀ n)

Type uses (2)

Body uses (1)

IicSuccProd

Used by (4)

Actions: Source · Open Issue

Proof

by
  induction n with
  | zero => simp_rw [density]; fun_prop
  | succ n ih => simp_rw [density]; fun_prop

`absolutelyContinuous_map_history`🔗

LemmaLearning.IsAlgEnvSeq.absolutelyContinuous_map_history

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.absolutelyContinuous_map_history.{u_1, u_2, u_3,
    u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  {Ω : Type u_3} [MeasurableSpace Ω] {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 : Algorithm.AbsolutelyContinuous alg alg₀) (n : ℕ) :
  MeasureTheory.Measure.AbsolutelyContinuous
    (MeasureTheory.Measure.map (history A Y n) P)
    (MeasureTheory.Measure.map (history A₀ Y₀ n) P₀)
Learning.IsAlgEnvSeq.absolutelyContinuous_map_history.{u_1,
    u_2, u_3, u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  {Ω : Type u_3} [MeasurableSpace Ω]
  {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 :
    Algorithm.AbsolutelyContinuous alg
      alg₀)
  (n : ℕ) :
  MeasureTheory.Measure.AbsolutelyContinuous
    (MeasureTheory.Measure.map
      (history A Y n) P)
    (MeasureTheory.Measure.map
      (history A₀ Y₀ n) P₀)

Code

lemma absolutelyContinuous_map_history (h : IsAlgEnvSeq A Y alg env P)
    (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
    P.map (history A Y n) ≪ P₀.map (history A₀ Y₀ n)

Type uses (5)

Body uses (13)

Actions: Source · Open Issue

Proof

by
  induction n with
  | zero =>
    rw [h.hasLaw_history_zero.map_eq, h₀.hasLaw_history_zero.map_eq]
    apply Measure.AbsolutelyContinuous.map _ (by fun_prop)
    rw [h.hasLaw_step_zero.map_eq, h₀.hasLaw_step_zero.map_eq]
    exact Measure.AbsolutelyContinuous.compProd_left hc.p0 _
  | succ n ih =>
    simp_rw [history_succ]
    rw [← Measure.map_map (by fun_prop), ← Measure.map_map (by fun_prop)]
    rotate_left
    · exact (h₀.measurable_history n).prodMk (h₀.measurable_step (n + 1))
    · exact (h.measurable_history n).prodMk (h.measurable_step (n + 1))
    apply Measure.AbsolutelyContinuous.map _ (by fun_prop)
    rw [(h.hasCondDistrib_step n).map_eq, (h₀.hasCondDistrib_step n).map_eq]
    apply Measure.AbsolutelyContinuous.compProd ih
    filter_upwards with h' using Measure.AbsolutelyContinuous.compProd_left_apply (hc.policy n h') _

`hasLaw_history_withDensity`🔗

LemmaLearning.IsAlgEnvSeq.hasLaw_history_withDensity

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.hasLaw_history_withDensity.{u_1, u_2, u_3, u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  {Ω : Type u_3} [MeasurableSpace Ω] {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₀]
  [MeasurableSpace.CountablyGenerated 𝓐] (h : IsAlgEnvSeq A Y alg env P)
  (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀)
  (hc : Algorithm.AbsolutelyContinuous alg alg₀) (n : ℕ) :
  ProbabilityTheory.HasLaw (history A Y n)
    (MeasureTheory.Measure.withDensity
      (MeasureTheory.Measure.map (history A₀ Y₀ n) P₀)
      (Algorithm.density alg alg₀ n))
    P
Learning.IsAlgEnvSeq.hasLaw_history_withDensity.{u_1,
    u_2, u_3, u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  {Ω : Type u_3} [MeasurableSpace Ω]
  {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₀]
  [MeasurableSpace.CountablyGenerated 𝓐]
  (h : IsAlgEnvSeq A Y alg env P)
  (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀)
  (hc :
    Algorithm.AbsolutelyContinuous alg
      alg₀)
  (n : ℕ) :
  ProbabilityTheory.HasLaw (history A Y n)
    (MeasureTheory.Measure.withDensity
      (MeasureTheory.Measure.map
        (history A₀ Y₀ n) P₀)
      (Algorithm.density alg alg₀ n))
    P

Code

lemma hasLaw_history_withDensity (h : IsAlgEnvSeq A Y alg env P)
    (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : HasLaw (history A Y n)
      ((P₀.map (history A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where
  aemeasurable

Type uses (6)

Body uses (20)

Used by (1)

condDistrib_history_eq_condDistrib_hist_withDensity

Actions: Source · Open Issue

Proof

(h.measurable_history n).aemeasurable
  map_eq := by
    induction n with
    | zero =>
      rw [h.hasLaw_history_zero.map_eq, h₀.hasLaw_history_zero.map_eq, h.hasLaw_step_zero.map_eq,
        h₀.hasLaw_step_zero.map_eq]
      rw [← Measure.withDensity_rnDeriv_eq _ _ hc.p0,
        Measure.compProd_withDensity_left (by fun_prop)]
      exact map_equiv_withDensity (by fun_prop)
    | succ n ih =>
      let ρ h' (ar : 𝓐 × 𝓨) := Kernel.rnDeriv (alg.policy n) (alg₀.policy n) h' ar.1
      have hs : stepKernel alg env n = (stepKernel alg₀ env n).withDensity ρ := by
        rw [stepKernel, ← Kernel.withDensity_rnDeriv_eq' (hc.policy n)]
        exact Kernel.compProd_withDensity_left (Kernel.measurable_rnDeriv _ _)
      have : IsMarkovKernel ((stepKernel alg₀ env n).withDensity ρ) := by
        rw [← hs]
        infer_instance
      simp_rw [history_succ]
      rw [← Measure.map_map (by fun_prop), ← Measure.map_map (by fun_prop)]
      rotate_left
      · exact (h₀.measurable_history n).prodMk (h₀.measurable_step (n + 1))
      · exact (h.measurable_history n).prodMk (h.measurable_step (n + 1))
      rw [(h.hasCondDistrib_step n).map_eq, (h₀.hasCondDistrib_step n).map_eq, ih, hs,
        Measure.compProd_withDensity_withDensity (by fun_prop) (by fun_prop)]
      exact map_equiv_withDensity (by fun_prop)

3.9. SequentialLearning.AlgorithmDensity🔗

AbsolutelyContinuous🔗

term_≪ₐ_🔗

density🔗

measurable_density🔗

absolutelyContinuous_map_history🔗

hasLaw_history_withDensity🔗

`AbsolutelyContinuous`🔗

`term_≪ₐ_`🔗

`density`🔗

`measurable_density`🔗

`absolutelyContinuous_map_history`🔗

`hasLaw_history_withDensity`🔗