Add AlgorithmDensity

LeanMachineLearning.lean

@@ -17,10 +17,13 @@ public import LeanMachineLearning.Probability.Independence.IndepInfinitePi
 public import LeanMachineLearning.Probability.Integrable
 public import LeanMachineLearning.Probability.Kernel.Basic
 public import LeanMachineLearning.Probability.Kernel.Composition.MapComap
+public import LeanMachineLearning.Probability.Kernel.Composition.MeasureCompProd
 public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj
 public import LeanMachineLearning.Probability.Kernel.KernelSub
 public import LeanMachineLearning.Probability.Moments.SubGaussian
+public import LeanMachineLearning.Probability.WithDensity
 public import LeanMachineLearning.SequentialLearning.Algorithm
+public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
 public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
 public import LeanMachineLearning.SequentialLearning.Deterministic

LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Paulo Rauber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paulo Rauber
+-/
+module
+
+public import Mathlib.Probability.Kernel.Composition.MeasureCompProd
+
+@[expose] public section
+
+open ProbabilityTheory
+
+namespace MeasureTheory.Measure
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β}
+
+section AbsolutelyContinuous
+
+lemma AbsolutelyContinuous.compProd_left_apply {γ : Type*} {mγ : MeasurableSpace γ}
+    [IsSFiniteKernel η] {a : α} (hac : κ a ≪ η a) (ξ : Kernel (α × β) γ) :
+    (κ ⊗ₖ ξ) a ≪ (η ⊗ₖ ξ) a := by
+  by_cases hκ : IsSFiniteKernel κ
+  · by_cases hξ : IsSFiniteKernel ξ
+    · simp_rw [Kernel.compProd_apply_eq_compProd_sectR, hac.compProd_left _]
+    · simp [Kernel.compProd_of_not_isSFiniteKernel_right _ _ hξ]
+  · simp [Kernel.compProd_of_not_isSFiniteKernel_left _ _ hκ]
+
+end AbsolutelyContinuous
+
+end MeasureTheory.Measure

LeanMachineLearning/Probability/WithDensity.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2026 Paulo Rauber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paulo Rauber
+-/
+module
+
+public import Mathlib.Probability.Kernel.CompProdEqIff
+public import Mathlib.Probability.Kernel.Composition.MeasureComp
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory
+
+open scoped ENNReal
+
+variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+variable {μ : Measure α}
+
+namespace MeasureTheory
+
+lemma map_withDensity_comp {g : α → γ} {f : γ → ℝ≥0∞} (hg : Measurable g) (hf : Measurable f) :
+    (μ.withDensity (f ∘ g)).map g = (μ.map g).withDensity f := by
+  ext s hs
+  rw [Measure.map_apply hg hs, withDensity_apply _ (hg hs), withDensity_apply _ hs,
+    setLIntegral_map hs hf hg]
+  rfl
+
+lemma map_equiv_withDensity {e : α ≃ᵐ β} {f : α → ℝ≥0∞} (hf : Measurable f) :
+    (μ.withDensity f).map e = (μ.map e).withDensity (f ∘ e.symm) := by
+  simp_rw [← map_withDensity_comp e.measurable (hf.comp e.symm.measurable),
+    Function.comp_assoc, MeasurableEquiv.symm_comp_self]
+  rfl
+
+lemma map_swap_withDensity_comp_snd {μ : Measure (α × β)} {f : β → ℝ≥0∞} (hf : Measurable f) :
+    (μ.withDensity (fun ab ↦ f ab.2)).map Prod.swap =
+      (μ.map Prod.swap).withDensity (fun ba ↦ f ba.1) := by
+  rw [← map_withDensity_comp measurable_swap (by fun_prop)]
+  rfl
+
+end MeasureTheory
+
+namespace MeasureTheory.Measure
+
+lemma compProd_withDensity_left [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ] {f : α → ℝ≥0∞}
+    (hf : Measurable f) : (μ.withDensity f) ⊗ₘ κ = (μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1) := by
+  refine ext_of_lintegral _ fun g hg ↦ ?_
+  calc ∫⁻ ab, g ab ∂((μ.withDensity f) ⊗ₘ κ)
+      = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂(μ.withDensity f) :=
+        lintegral_compProd hg
+    _ = ∫⁻ a, f a * ∫⁻ b, g (a, b) ∂κ a ∂μ :=
+        lintegral_withDensity_eq_lintegral_mul _ hf hg.lintegral_kernel_prod_right'
+    _ = ∫⁻ a, ∫⁻ b, f a * g (a, b) ∂κ a ∂μ :=
+        lintegral_congr fun a ↦ (lintegral_const_mul _ (by fun_prop)).symm
+    _ = ∫⁻ ab, (fun ab ↦ f ab.1) ab * g ab ∂(μ ⊗ₘ κ) :=
+        (lintegral_compProd ((hf.comp measurable_fst).mul hg)).symm
+    _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1)) :=
+        (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_fst) hg).symm
+
+lemma compProd_withDensity_withDensity [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ]
+    {f : α → ℝ≥0∞} {g : α → β → ℝ≥0∞} (hf : Measurable f) (hg : Measurable (Function.uncurry g))
+    [IsSFiniteKernel (κ.withDensity g)] :
+    (μ.withDensity f) ⊗ₘ (κ.withDensity g) =
+      (μ ⊗ₘ κ).withDensity (fun ac ↦ f ac.1 * g ac.1 ac.2) := by
+  rw [compProd_withDensity hg, compProd_withDensity_left hf]
+  exact (withDensity_mul _ (hf.comp measurable_fst) hg).symm
+
+lemma compProd_eq_compProd_withDensity_comp_snd [SFinite μ] {κ η : Kernel α β} [IsSFiniteKernel κ]
+    [IsSFiniteKernel η] {f : β → ℝ≥0∞} (hf : Measurable f)
+    (h : κ =ᵐ[μ] η.withDensity (fun _ b ↦ f b)) :
+    μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun ab ↦ f ab.2) := by
+  /- A proof based on `compProd_congr` requires `IsSFiniteKernel (η.withDensity fun _ b ↦ f b)`. -/
+  refine ext_of_lintegral _ fun g hg ↦ ?_
+  calc ∫⁻ ab, g ab ∂(μ ⊗ₘ κ)
+      = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂μ :=
+        lintegral_compProd hg
+    _ = ∫⁻ a, ∫⁻ b, g (a, b) ∂((η a).withDensity f) ∂μ := by
+        apply lintegral_congr_ae
+        filter_upwards [h] with a ha
+        rw [ha, Kernel.withDensity_apply _ (by fun_prop)]
+    _ = ∫⁻ a, ∫⁻ b, f b * g (a, b) ∂η a ∂μ := by
+        congr with a
+        exact lintegral_withDensity_eq_lintegral_mul _ hf (by fun_prop)
+    _ = ∫⁻ ab, f ab.2 * g ab ∂(μ ⊗ₘ η) :=
+        (lintegral_compProd ((hf.comp measurable_snd).mul hg)).symm
+    _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ η).withDensity (fun ab ↦ f ab.2)) :=
+        (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_snd) hg).symm
+
+end MeasureTheory.Measure
+
+namespace ProbabilityTheory.Kernel
+
+lemma comp_withDensity_eq_withDensity_comp {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ℝ≥0∞}
+    (hf : Measurable f) : (κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ = (κ ∘ₘ μ).withDensity f := by
+  refine Measure.ext_of_lintegral _ fun g hg ↦ ?_
+  calc ∫⁻ b, g b ∂((κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ)
+      = ∫⁻ a, ∫⁻ b, g b ∂(κ.withDensity (fun _ b ↦ f b)) a ∂μ :=
+        Measure.lintegral_bind (measurable _).aemeasurable hg.aemeasurable
+    _ = ∫⁻ a, ∫⁻ b, f b * g b ∂κ a ∂μ := by
+        congr with a
+        exact lintegral_withDensity _ (by fun_prop) _ hg
+    _ = ∫⁻ b, f b * g b ∂(κ ∘ₘ μ) :=
+        (Measure.lintegral_bind (measurable _).aemeasurable (hf.mul hg).aemeasurable).symm
+    _ = ∫⁻ b, g b ∂((κ ∘ₘ μ).withDensity f) :=
+        (lintegral_withDensity_eq_lintegral_mul _ hf hg).symm
+
+lemma compProd_withDensity_left {κ : Kernel α β} {η : Kernel (α × β) γ} {f : α → β → ℝ≥0∞}
+    [IsSFiniteKernel κ] [IsSFiniteKernel η] [IsSFiniteKernel (κ.withDensity f)]
+    (hf : Measurable (Function.uncurry f)) :
+    (κ.withDensity f) ⊗ₖ η = (κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1) := by
+  ext a : 1
+  calc ((κ.withDensity f) ⊗ₖ η) a
+      = (κ a).withDensity (f a) ⊗ₘ η.sectR a := by
+        rw [compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ hf]
+    _ = ((κ a) ⊗ₘ (η.sectR a)).withDensity (fun bc ↦ f a bc.1) :=
+        Measure.compProd_withDensity_left (by fun_prop)
+    _ = ((κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1)) a := by
+        rw [← compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ (by fun_prop)]
+
+lemma withDensity_rnDeriv_eq' {κ η : Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β]
+    [IsFiniteKernel κ] [IsFiniteKernel η] (h : ∀ a, κ a ≪ η a) :
+    η.withDensity (κ.rnDeriv η) = κ :=
+  Kernel.ext fun a ↦ withDensity_rnDeriv_eq (h a)
+
+end ProbabilityTheory.Kernel

LeanMachineLearning/SequentialLearning/Algorithm.lean

@@ -19,11 +19,13 @@ an algorithm interacting with an environment.
 
 * `Algorithm 𝓐 𝓨`: a stochastic, sequential algorithm.
 * `Environment 𝓐 𝓨`: a stochastic environment.
-* `IsAlgEnvSeq A 𝓨' alg env P`: an algorithm-environment sequence. That is, a sequence of
+* `IsAlgEnvSeq A 𝓨 alg env P`: an algorithm-environment sequence. That is, a sequence of
   actions `A` and feedback `Y` that have the correct conditional distributions to be generated by
   an algorithm `alg` interacting with an environment `env`, defined on a probability space `(Ω, P)`.
 * `IsAlgEnvSeqUntil A Y alg env P N`: `A` and `Y` form an algorithm-environment sequence until
   time `N`.
+* `prod_left alg`: an `Algorithm 𝓐 (𝓧 × 𝓨)` obtained from an algorithm `alg : Algorithm 𝓐 𝓨` by
+  ignoring the `𝓧` component of each observation.
 
 ## Notes
 
@@ -55,6 +57,13 @@ structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace
 instance (alg : Algorithm 𝓐 𝓨) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n
 instance (alg : Algorithm 𝓐 𝓨) : IsProbabilityMeasure alg.p0 := alg.hp0
 
+/-- An algorithm with observations in `𝓧 × 𝓨` obtained from an algorithm with observations in `𝓨`
+by ignoring the `𝓧` component of each observation. -/
+def Algorithm.prod_left (𝓧 : Type*) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) :
+    Algorithm 𝓐 (𝓧 × 𝓨) where
+  policy n := (alg.policy n).comap (fun h i ↦ ((h i).1, (h i).2.2)) (by fun_prop)
+  p0 := alg.p0
+
 /-- A stochastic environment. -/
 -- ANCHOR: Environment
 structure Environment (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
@@ -190,6 +199,35 @@ lemma IsAlgEnvSeqUntil.hasCondDistrib_step (h : IsAlgEnvSeqUntil A Y alg env P N
       (stepKernel alg env n) P :=
   HasCondDistrib.prod (h.hasCondDistrib_action n hn) (h.hasCondDistrib_feedback n hn)
 
+lemma IsAlgEnvSeq.hasLaw_hist_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw (hist A Y 0)
+    ((P.map (step A Y 0)).map (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ 𝓐 × 𝓨)).symm) P where
+  aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback 0).aemeasurable
+  map_eq := by
+    have he : (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ 𝓐 × 𝓨)).symm ∘ step A Y 0 =
+        hist A Y 0 := by
+      funext _ ⟨0, _⟩
+      rfl
+    rw [← he]
+    have hA := h.measurable_action
+    have hY := h.measurable_feedback
+    exact (Measure.map_map (by fun_prop) (by fun_prop)).symm
+
+lemma IsAlgEnvSeq.hasLaw_hist_succ (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+  HasLaw (hist A Y (n + 1))
+    ((P.map (hist A Y n) ⊗ₘ condDistrib (step A Y (n + 1)) (hist A Y n) P).map
+        (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm) P where
+  aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback (n + 1)).aemeasurable
+  map_eq := by
+    have he : (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm ∘
+        (fun ω ↦ (hist A Y n ω, step A Y (n + 1) ω)) = hist A Y (n + 1) := by
+      funext ω
+      exact (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm_apply_apply (hist A Y (n + 1) ω)
+    have hA := h.measurable_action
+    have hY := h.measurable_feedback
+    rw [← he, ← Measure.map_map (by fun_prop) (by fun_prop)]
+    congr
+    exact (compProd_map_condDistrib (by fun_prop)).symm
+
 end IsAlgEnvSeq
 
 /-- Filtration generated by the history up to time `n`. -/

LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2026 Paulo Rauber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paulo Rauber
+-/
+module
+
+public import LeanMachineLearning.Probability.Kernel.Composition.MeasureCompProd
+public import LeanMachineLearning.Probability.WithDensity
+public import LeanMachineLearning.SequentialLearning.Algorithm
+
+/-!
+# 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_hist_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₀`.
+
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Finset
+
+open scoped ENNReal
+
+namespace Learning
+
+variable {𝓐 𝓨 : Type*} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
+
+namespace Algorithm
+
+/-- 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 AbsolutelyContinuous (alg alg₀ : Algorithm 𝓐 𝓨) : Prop where
+  p0 : alg.p0 ≪ alg₀.p0
+  policy n h : alg.policy n h ≪ alg₀.policy n h
+
+@[inherit_doc AbsolutelyContinuous]
+scoped notation:50 alg " ≪ₐ " alg₀ => AbsolutelyContinuous alg alg₀
+
+/-- 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`. -/
+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
+
+@[fun_prop]
+lemma measurable_density [MeasurableSpace.CountablyGenerated 𝓐] (alg alg₀ : Algorithm 𝓐 𝓨) (n : ℕ) :
+    Measurable (alg.density alg₀ n) := by
+  induction n with
+  | zero => simp_rw [density]; fun_prop
+  | succ n ih => simp_rw [density]; fun_prop
+
+end Algorithm
+
+namespace IsAlgEnvSeq
+
+variable {Ω : Type*} [MeasurableSpace Ω]
+variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨]
+variable {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨}
+variable {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
+variable {P : Measure Ω} [IsFiniteMeasure P]
+
+variable {Ω₀ : Type*} [MeasurableSpace Ω₀]
+variable {alg₀ : Algorithm 𝓐 𝓨}
+variable {A₀ : ℕ → Ω₀ → 𝓐} {Y₀ : ℕ → Ω₀ → 𝓨}
+variable {P₀ : Measure Ω₀} [IsProbabilityMeasure P₀]
+
+open scoped Algorithm
+
+lemma absolutelyContinuous_map_hist (h : IsAlgEnvSeq A Y alg env P)
+    (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
+    P.map (IsAlgEnvSeq.hist A Y n) ≪ P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n) := by
+  induction n with
+  | zero =>
+    rw [h.hasLaw_hist_zero.map_eq, h₀.hasLaw_hist_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 =>
+    rw [(h.hasLaw_hist_succ n).map_eq, (h₀.hasLaw_hist_succ n).map_eq]
+    apply Measure.AbsolutelyContinuous.map _ (by fun_prop)
+    rw [Measure.compProd_congr (h.hasCondDistrib_step n).condDistrib_eq,
+        Measure.compProd_congr (h₀.hasCondDistrib_step n).condDistrib_eq]
+    apply Measure.AbsolutelyContinuous.compProd ih
+    filter_upwards with h' using Measure.AbsolutelyContinuous.compProd_left_apply (hc.policy n h') _
+
+lemma hasLaw_hist_withDensity (h : IsAlgEnvSeq A Y alg env P) (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀)
+   (hc : alg ≪ₐ alg₀) (n : ℕ) : HasLaw (IsAlgEnvSeq.hist A Y n)
+      ((P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where
+  aemeasurable :=
+    (IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable
+  map_eq := by
+    induction n with
+    | zero =>
+      rw [h.hasLaw_hist_zero.map_eq, h₀.hasLaw_hist_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
+      rw [(h.hasLaw_hist_succ n).map_eq, (h₀.hasLaw_hist_succ n).map_eq,
+          Measure.compProd_congr (h.hasCondDistrib_step n).condDistrib_eq,
+          Measure.compProd_congr (h₀.hasCondDistrib_step n).condDistrib_eq, ih, hs,
+          Measure.compProd_withDensity_withDensity (by fun_prop) (by fun_prop)]
+      exact map_equiv_withDensity (by fun_prop)
+
+end IsAlgEnvSeq
+
+end Learning