Update Mathlib

LeanBandits/AlgorithmBuilding.lean

@@ -5,7 +5,8 @@ Authors: Rémy Degenne
 -/
 import Mathlib.Analysis.Normed.Ring.Basic
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
-import Mathlib.Topology.Compactness.PseudometrizableLindelof
+import Mathlib.Topology.Compactness.Lindelof
+import Mathlib.Topology.Metrizable.Basic
 
 /-! # Tools to build bandit algorithms
 

LeanBandits/BanditAlgorithms/ETC.lean

@@ -375,8 +375,7 @@ lemma expectation_pullCount_le (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (
     rw [integrable_indicator_iff]
     · exact integrableOn_const
     · exact (measurableSet_singleton _).preimage (by fun_prop)
-  simp only [integral_const, measureReal_univ_eq_one, smul_eq_mul, one_mul, neg_mul,
-    add_le_add_iff_left, ge_iff_le]
+  simp only [integral_const, probReal_univ, smul_eq_mul, one_mul, neg_mul, add_le_add_iff_left]
   gcongr
   · norm_cast
     simp

LeanBandits/ForMathlib/CondDistrib.lean

@@ -202,7 +202,7 @@ theorem FiniteMeasure.toMeasure_sub (μ ν : FiniteMeasure α) : ↑(μ - ν) =
   rfl
 
 instance : CanonicallyOrderedAdd (FiniteMeasure α) where
-  le_add_self := sorry -- was not needed before?
+  le_add_self μ ν := fun s ↦ by simp
   exists_add_of_le {μ ν} hμν := by
     refine ⟨ν - μ, ?_⟩
     rw [FiniteMeasure.ext_iff_coe]
@@ -264,6 +264,7 @@ lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
     (h : condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] η.prodMkLeft _) :
     Y ⟂ᵢ[Z, hZ; μ] X := by
   refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight hX hY hZ ?_ (η := η)
+  rw [← Kernel.compProd_eq_iff, compProd_map_condDistrib (by fun_prop)] at h ⊢
   sorry
 
 /-- Law of `Y` conditioned on `X`. -/

LeanBandits/ForMathlib/IndepFun.lean

@@ -9,22 +9,45 @@ variable {α Ω Ω' E ι : Type*} [Countable ι] {mα : MeasurableSpace α}
   {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
   {mE : MeasurableSpace E} {μ ν : Measure Ω}
 
-lemma iIndepFun_nat_iff_forall_indepFun {X : ℕ → Ω → E} (hX : ∀ n, AEMeasurable (X n) μ) :
+lemma iIndepFun_nat_iff_forall_indepFun [IsProbabilityMeasure μ] {X : ℕ → Ω → E}
+    (hX : ∀ n, AEMeasurable (X n) μ) :
     iIndepFun X μ ↔ ∀ n, X (n + 1) ⟂ᵢ[μ] fun ω (i : Iic n) ↦ X i ω := by
   constructor
   · intro h n
-    have h' := h.indepFun_finset₀ {n + 1} (Iic n) (by simp) hX
-    let f : (({n + 1} : Finset ℕ) → E) → E := fun x ↦ x ⟨n + 1, by simp⟩
-    have hf : Measurable f := by unfold f; fun_prop
-    have h_eq : X (n + 1) = f ∘ (fun ω (i : ({n + 1} : Finset ℕ)) ↦ X i ω) := rfl
-    exact h'.comp (ψ := id) hf measurable_id
+    exact (h.indepFun_finset₀ {n + 1} (Iic n) (by simp) hX).comp
+      (measurable_pi_apply ⟨n + 1, by simp⟩) measurable_id
   · intro h
-    suffices ∀ n, iIndepFun ((Iic n).restrict X) μ by
-      rw [iIndepFun_iff_finset]
-      intro s
-      sorry
-    intro n
-    sorry
+    rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
+    intro s sets hsets
+    induction s using Finset.strongInductionOn with
+    | _ s ih =>
+    obtain rfl | hs := s.eq_empty_or_nonempty
+    · simp
+    · obtain hn_zero | hn_pos := (s.max' hs).eq_zero_or_pos
+      · simp [eq_singleton_iff_unique_mem.mpr ⟨hn_zero ▸ max'_mem _ hs,
+          fun j hj => Nat.le_zero.mp (hn_zero ▸ le_max' _ j hj)⟩]
+      · have hs'_le : ∀ i ∈ s.erase (s.max' hs), i ∈ Iic (s.max' hs - 1) := fun i hi =>
+          mem_Iic.mpr (Nat.lt_succ_iff.mp (Nat.succ_pred_eq_of_pos hn_pos ▸
+            lt_max'_of_mem_erase_max' _ hs hi))
+        let t : Set (Iic (s.max' hs - 1) → E) :=
+          {f | ∀ i : s.erase (s.max' hs), f ⟨i.1, hs'_le i.1 i.2⟩ ∈ sets i.1}
+        have ht : MeasurableSet t := by
+          have : t = ⋂ i : s.erase (s.max' hs), (· ⟨i.1, hs'_le i.1 i.2⟩) ⁻¹' sets i.1 := by
+            ext
+            simp [t]
+          exact this ▸ .iInter fun ⟨i, hi⟩ =>
+            (hsets i (erase_subset _ _ hi)).preimage (measurable_pi_apply _)
+        have heq : ⋂ i ∈ s.erase (s.max' hs), X i ⁻¹' sets i =
+            (fun ω (j : Iic (s.max' hs - 1)) => X j ω) ⁻¹' t := by
+          ext ω
+          simp only [Set.mem_iInter, Set.mem_preimage, t]
+          exact ⟨fun hω ⟨i, hi⟩ => hω i hi, fun hω i hi => hω ⟨i, hi⟩⟩
+        have hind := h (s.max' hs - 1)
+        rw [Nat.sub_add_cancel hn_pos] at hind
+        rw [(insert_erase (max'_mem _ hs)).symm, set_biInter_insert, heq,
+          hind.measure_inter_preimage_eq_mul _ _ (hsets _ (max'_mem _ hs)) ht, ← heq,
+          ih _ (erase_ssubset (max'_mem _ hs)) fun i hi => hsets i (erase_subset _ _ hi),
+          prod_insert (notMem_erase _ _)]
 
 -- todo: kernel version?
 lemma IndepFun_map_iff [IsFiniteMeasure μ] {X : Ω' → E} {Y : Ω' → E} {f : Ω → Ω'}

LeanBandits/ForMathlib/KernelSub.lean

@@ -250,9 +250,9 @@ lemma measurableSet_eq_zero (κ : Kernel α β) [IsFiniteKernel κ] :
   rw [h_sing]
   exact measurableSet_mutuallySingular κ κ
 
-lemma measurableSet_eq [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
-    (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
+lemma measurableSet_eq (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
     MeasurableSet {a | κ a = η a} := by
+  classical
   have h_sub : {a | κ a = η a} = {a | (κ - η) a = 0} ∩ {a | (η - κ) a = 0} := by
     ext1 a
     simp only [Set.mem_setOf_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le]

LeanBandits/ForMathlib/SubGaussian.lean

@@ -10,119 +10,10 @@ open scoped ENNReal NNReal
 
 namespace ProbabilityTheory
 
-theorem mgf_const_mul {Ω : Type*} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω}
-    {t : ℝ} (α : ℝ) : mgf (fun ω ↦ α * X ω) μ t = mgf X μ (α * t) := by
-  rw [← mgf_smul_left]
-  rfl
-
-/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`, then `X` is integrable. -/
-lemma integrable_of_mem_interior_integrableExpSet
-    {Ω : Type*} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω}
-    (h : 0 ∈ interior (integrableExpSet X μ)) :
-    Integrable X μ := by
-  simpa using integrable_pow_of_mem_interior_integrableExpSet h 1
-
-namespace Kernel.HasSubgaussianMGF
-
-variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
-  {ν : Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {c : ℝ≥0}
-
-lemma id_map_iff (hX : Measurable X) :
-    HasSubgaussianMGF X c κ ν ↔ HasSubgaussianMGF id c (κ.map X) ν := by
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · constructor
-    · intro t
-      rw [← Kernel.deterministic_comp_eq_map hX, ← Measure.comp_assoc,
-        Measure.deterministic_comp_eq_map]
-      rw [integrable_map_measure (by fun_prop) hX.aemeasurable]
-      exact h.integrable_exp_mul t
-    · simp_rw [Kernel.map_apply _ hX, mgf_id_map hX.aemeasurable]
-      exact h.mgf_le
-  · have : X = id ∘ X := rfl
-    rw [this]
-    exact .of_map hX h
-
-protected lemma const_mul (h : HasSubgaussianMGF X c κ ν) (r : ℝ) :
-    HasSubgaussianMGF (fun ω ↦ r * X ω) (⟨r ^ 2, sq_nonneg r⟩ * c) κ ν where
-  integrable_exp_mul t := by
-    simp_rw [← mul_assoc]
-    exact h.integrable_exp_mul (t * r)
-  mgf_le := by
-    filter_upwards [h.mgf_le] with ω hω t
-    specialize hω (t * r)
-    rw [mgf_const_mul, mul_comm]
-    refine hω.trans_eq ?_
-    congr 1
-    simp only [NNReal.coe_mul, NNReal.coe_mk]
-    ring
-
-end Kernel.HasSubgaussianMGF
-
 namespace HasSubgaussianMGF
 
 variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X Y : Ω → ℝ} {c cX cY : ℝ≥0}
 
-lemma id_map_iff (hX : AEMeasurable X μ) :
-    HasSubgaussianMGF X c μ ↔ HasSubgaussianMGF id c (μ.map X) := by
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · constructor
-    · intro t
-      rw [integrable_map_measure (by fun_prop) hX]
-      exact h.integrable_exp_mul t
-    · intro t
-      rw [mgf_id_map hX]
-      exact h.mgf_le t
-  · have : X = id ∘ X := rfl
-    rw [this]
-    exact .of_map hX h
-
-lemma congr_identDistrib {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ' : Measure Ω'}
-    {Y : Ω' → ℝ} (hX : HasSubgaussianMGF X c μ) (hXY : IdentDistrib X Y μ μ') :
-    HasSubgaussianMGF Y c μ' := by
-  rw [id_map_iff hXY.aemeasurable_fst] at hX
-  rwa [id_map_iff hXY.aemeasurable_snd, ← hXY.map_eq]
-
-protected lemma const_mul (h : HasSubgaussianMGF X c μ) (r : ℝ) :
-    HasSubgaussianMGF (fun ω ↦ r * X ω) (⟨r ^ 2, sq_nonneg r⟩ * c) μ := by
-  rw [HasSubgaussianMGF_iff_kernel] at h ⊢
-  exact Kernel.HasSubgaussianMGF.const_mul h r
-
-lemma sub_of_indepFun (hX : HasSubgaussianMGF X cX μ) (hY : HasSubgaussianMGF Y cY μ)
-    (hindep : IndepFun X Y μ) :
-    HasSubgaussianMGF (fun ω ↦ X ω - Y ω) (cX + cY) μ := by
-  simp_rw [sub_eq_add_neg]
-  exact hX.add_of_indepFun hY.neg hindep.neg_right
-
--- todo: name
-lemma measure_le_le (hX : HasSubgaussianMGF (fun ω ↦ X ω - μ[X]) cX μ)
-    (hY : HasSubgaussianMGF (fun ω ↦ Y ω - μ[Y]) cY μ)
-    (hindep : IndepFun X Y μ) (h_le : μ[Y] ≤ μ[X]) :
-    μ.real {ω | X ω ≤ Y ω} ≤ Real.exp (- (μ[Y] - μ[X]) ^ 2 / (2 * (cX + cY))) := by
-  calc μ.real {ω | X ω ≤ Y ω}
-  _ = μ.real {ω | (μ[X] - μ[Y]) ≤ (Y ω - μ[Y]) - (X ω - μ[X])} := by
-    congr with ω
-    grind
-  _ ≤ Real.exp (- (μ[Y] - μ[X]) ^ 2 / (2 * (cX + cY))) := by
-    refine (measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq
-      ?_
-    · rw [add_comm cX]
-      refine sub_of_indepFun hY hX ?_
-      exact hindep.symm.comp (φ := fun x ↦ x - μ[Y]) (ψ := fun x ↦ x - μ[X])
-        (by fun_prop) (by fun_prop)
-    · grind
-    · congr 2
-      grind
-
-lemma integrableExpSet_eq_univ (hX : HasSubgaussianMGF X c μ) :
-    integrableExpSet X μ = Set.univ := by
-  ext t
-  simp only [Set.mem_univ, iff_true]
-  exact hX.integrable_exp_mul t
-
-lemma integrable (hX : HasSubgaussianMGF X c μ) : Integrable X μ := by
-  refine integrable_of_mem_interior_integrableExpSet ?_
-  simp [integrableExpSet_eq_univ hX]
-
 section Sum
 
 variable {ι ι' : Type*} {X : ι → Ω → ℝ} {cX : ι → ℝ≥0} {s : Finset ι}
@@ -145,8 +36,8 @@ lemma measure_sum_le_sum_le [IsFiniteMeasure μ]
     have h_int := (hY_subG j his).integrable
     simp_rw [sub_eq_add_neg, integrable_add_const_iff] at h_int
     exact h_int
-  refine (measure_le_le (cX := ∑ i ∈ s, cX i) (cY := ∑ j ∈ t, cY j) ?_ ?_ h_indep_sum ?_).trans_eq
-    ?_
+  refine (measureReal_le_le_exp
+    (cX := ∑ i ∈ s, cX i) (cY := ∑ j ∈ t, cY j) ?_ ?_ h_indep_sum ?_).trans_eq ?_
   · suffices HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, (X i ω - μ[X i])) (∑ i ∈ s, cX i) μ by
       convert this
       rw [integral_finset_sum _ hX_int, Finset.sum_sub_distrib]

LeanBandits/ForMathlib/Traj.lean

@@ -10,87 +10,21 @@ variable {μ₀ : Measure (X 0)} [IsProbabilityMeasure μ₀]
 
 section MeasurableEquiv
 
-instance : Unique (Iic 0) := by simp only [mem_Iic, nonpos_iff_eq_zero]; exact Unique.subtypeEq 0
-
-lemma coe_default_Iic_zero : ((default : Iic 0) : ℕ) = 0 := by
-  calc _ = ((⟨0, by simp⟩ : Iic 0) : ℕ) := by congr; exact (Unique.eq_default _).symm
-    _ = _ := by simp
-
-/-- Measurable equivalence between `Iic 0 → X i` and `X 0`. -/
-def MeasurableEquiv.piIicZero (X : ℕ → Type*) [∀ n, MeasurableSpace (X n)] :
-    ((i : Iic 0) → X i) ≃ᵐ X 0 :=
-  (MeasurableEquiv.piUnique _).trans (coe_default_Iic_zero.symm ▸ MeasurableEquiv.refl _)
+lemma coe_default_Iic_zero : ((default : Iic 0) : ℕ) = 0 := rfl
 
 end MeasurableEquiv
 
 namespace ProbabilityTheory.Kernel
 
--- Probability/Kernel/IonescuTulcea/Traj.lean
-/-- Distribution of the infinite trajectory given the distribution of `X 0`. -/
-noncomputable
-def trajMeasure (μ₀ : Measure (X 0)) (κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1)))
-    [∀ n, IsMarkovKernel (κ n)] :
-    Measure (Π n, X n) :=
-  (traj κ 0) ∘ₘ (μ₀.map (MeasurableEquiv.piIicZero _).symm)
-
--- Probability/Kernel/IonescuTulcea/Traj.lean
-instance : IsProbabilityMeasure (trajMeasure μ₀ κ) := by
-  rw [trajMeasure]
-  have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piIicZero _).symm) :=
-    Measure.isProbabilityMeasure_map <| by fun_prop
-  infer_instance
-
--- Probability/Kernel/IonescuTulcea/Traj.lean
-lemma traj_map_eq_kernel {a : ℕ} : (traj κ a).map (fun x ↦ x (a + 1)) = κ a := by
-  set f : (Π n, X n) → X (a + 1) := fun x ↦ x (a + 1)
-  set g : (Π n : Iic (a + 1), X n) → X (a + 1) := fun x ↦ x ⟨a + 1, by simp⟩
-  have hf : f = g ∘ (frestrictLe (a + 1)) := by rfl
-  have hp : g ∘ IicProdIoc a (a + 1) = (piSingleton a).symm ∘ Prod.snd := by
-    ext
-    simp [g, _root_.IicProdIoc, piSingleton]
-  rw [hf, map_comp_right _ (by fun_prop) (by fun_prop), traj_map_frestrictLe, partialTraj_succ_self,
-    ← map_comp_right _ (by fun_prop) (by fun_prop), hp,
-    map_comp_right _ (by fun_prop) (by fun_prop), ← snd_eq, snd_prod,
-    ← map_comp_right _ (by fun_prop) (by fun_prop)]
-  simp
-
--- Probability/Kernel/IonescuTulcea/Traj.lean
-lemma partialTraj_compProd_kernel_eq_traj_map {a : ℕ} {x₀ : Π n : Iic 0, X n} :
-    (partialTraj κ 0 a x₀) ⊗ₘ (κ a) = (traj κ 0 x₀).map (fun x ↦ (frestrictLe a x, x (a + 1))) := by
-  set f := fun x ↦ (frestrictLe a x, x (a + 1))
-  set g := fun x ↦ (frestrictLe a x, x)
-  have hf : f = (Prod.map id (fun x ↦ x (a + 1))) ∘ g := rfl
-  rw [hf, ← Measure.map_map (by fun_prop) (by fun_prop), ← partialTraj_compProd_traj zero_le',
-    ← MeasureTheory.Measure.compProd_map (by fun_prop), traj_map_eq_kernel]
-
--- (Extract kernel lemmas from rewrites?) Probability/Kernel/IonescuTulcea/Traj.lean
-lemma trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map {a : ℕ} :
-    (trajMeasure μ₀ κ).map (frestrictLe a) ⊗ₘ κ a =
-      (trajMeasure μ₀ κ).map (fun x ↦ (frestrictLe a x, x (a + 1))) := by
-  rw [Measure.compProd_eq_comp_prod, trajMeasure, Measure.map_comp _ _ (by fun_prop),
-    traj_map_frestrictLe, Measure.comp_assoc, Measure.map_comp _ _ (by fun_prop)]
-  congr with x₀
-  rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply _ (by fun_prop),
-    partialTraj_compProd_kernel_eq_traj_map]
-
--- Probability/Kernel/IonescuTulcea/Traj.lean
-lemma condDistrib_trajMeasure_ae_eq_kernel {a : ℕ}
-    [StandardBorelSpace (X (a + 1))] [Nonempty (X (a + 1))] :
-    condDistrib (fun x ↦ x (a + 1)) (frestrictLe a) (trajMeasure μ₀ κ)
-      =ᵐ[(trajMeasure μ₀ κ).map (frestrictLe a)] κ a := by
-  apply condDistrib_ae_eq_of_measure_eq_compProd _ (by measurability)
-  exact trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map.symm
-
 lemma traj_zero_map_eval_zero :
-    (Kernel.traj κ 0).map (fun h ↦ h 0)
-      = Kernel.deterministic (MeasurableEquiv.piIicZero X)
-        (MeasurableEquiv.piIicZero X).measurable := by
-  suffices (Kernel.traj κ 0).map (fun h ↦ h 0) = (Kernel.partialTraj κ 0 0).map
-      (MeasurableEquiv.piIicZero X) by
-    rwa [Kernel.partialTraj_zero,
-      Kernel.deterministic_map _ (MeasurableEquiv.piIicZero X).measurable] at this
+    (Kernel.traj κ 0).map (fun h ↦ h (default : Iic 0))
+      = Kernel.deterministic (MeasurableEquiv.piUnique (fun i : Iic 0 ↦ X i))
+        (MeasurableEquiv.piUnique _).measurable := by
+  suffices (Kernel.traj κ 0).map (fun h ↦ h (default : Iic 0))
+      = (Kernel.partialTraj κ 0 0).map (MeasurableEquiv.piUnique (fun i : Iic 0 ↦ X i)) by
+    rwa [Kernel.partialTraj_zero, Kernel.deterministic_map] at this
+    fun_prop
   rw [← Kernel.traj_map_frestrictLe, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)]
-  congr with h
-  sorry
+  rfl
 
 end ProbabilityTheory.Kernel

LeanBandits/RewardByCountMeasure.lean

@@ -259,7 +259,7 @@ lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α
     rw [cond_of_condIndepFun (by fun_prop)]
     · exact condIndepFun_reward_stepsUntil_arm a m n hm
     · refine measurable_one.indicator ?_
-      exact measurableSet_eq_fun' (by fun_prop) (by fun_prop)
+      exact measurableSet_eq_fun (by fun_prop) (by fun_prop)
     · fun_prop
     · convert hμna using 2
       rw [Set.inter_comm]

LeanBandits/SequentialLearning/Algorithm.lean

@@ -186,7 +186,7 @@ lemma condDistrib_step [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace
     (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
     condDistrib (step (n + 1)) (hist n) (trajMeasure alg env)
       =ᵐ[(trajMeasure alg env).map (hist n)] stepKernel alg env n :=
-  Kernel.condDistrib_trajMeasure_ae_eq_kernel
+  Kernel.condDistrib_trajMeasure
 
 lemma condDistrib_action [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
@@ -214,11 +214,12 @@ lemma hasLaw_step_zero (alg : Algorithm α R) (env : Environment α R) :
   aemeasurable := Measurable.aemeasurable (by fun_prop)
   map_eq := by
     unfold step
+    rw [← coe_default_Iic_zero]
     simp only [trajMeasure, Kernel.trajMeasure]
     rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc,
       Kernel.deterministic_comp_eq_map, Kernel.traj_zero_map_eval_zero,
       Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)]
-    simp
+    exact Measure.map_id
 
 lemma hasLaw_action_zero (alg : Algorithm α R) (env : Environment α R) :
     HasLaw (action 0) alg.p0 (trajMeasure alg env) where

blueprint/lean_decls

@@ -2,7 +2,7 @@ Learning.Algorithm
 Learning.Environment
 ProbabilityTheory.Kernel.traj
 ProbabilityTheory.Kernel.trajMeasure
-ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel
+ProbabilityTheory.Kernel.condDistrib_trajMeasure
 Learning.condDistrib_action
 Learning.condDistrib_reward
 Learning.hasLaw_action_zero

blueprint/src/chapters/algorithm.tex

@@ -90,7 +90,7 @@ \section{Ionescu-Tulcea theorem}
 \begin{lemma}\label{lem:condDistrib_X_add_one}
   \uses{def:history, def:trajMeasure}
   \leanok
-  \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel}
+  \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure}
 For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t$.
 \end{lemma}