From e8e5e5445d4b0e73fc2d38fc0e4caef2d793827a Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Mon, 15 Jun 2026 12:13:11 +0200
Subject: [PATCH] review lemma vs theorem

---
 .../Online/Bandit/RewardByCountMeasure.lean               | 2 +-
 .../Probability/Independence/CondDistrib.lean             | 2 +-
 .../Probability/Independence/IndepInfinitePi.lean         | 2 +-
 .../Probability/Kernel/IonescuTulcea/Traj.lean            | 8 ++++----
 LeanMachineLearning/SequentialLearning/FiniteActions.lean | 4 ++--
 .../SequentialLearning/IonescuTulceaSpace.lean            | 8 ++++----
 6 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
index 44e91fdc..0b615176 100644
--- a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
+++ b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
@@ -157,7 +157,7 @@ lemma reward_cond_stepsUntil [StandardBorelSpace Ω] [Countable 𝓐]
 
 /-- The conditional distribution of the reward received at the `m`-th pull of action `a`
 given the time at which number of pulls is `m` is the constant kernel with value `ν a`. -/
-theorem condDistrib_rewardByCount_stepsUntil [StandardBorelSpace Ω] [Countable 𝓐]
+lemma condDistrib_rewardByCount_stepsUntil [StandardBorelSpace Ω] [Countable 𝓐]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : 𝓐) (m : ℕ) (hm : m ≠ 0) :
     condDistrib (rewardByCount A R a m) (fun ω ↦ stepsUntil A a m ω.1) 𝔓
       =ᵐ[(𝔓).map (fun ω ↦ stepsUntil A a m ω.1)] Kernel.const _ (ν a) := by
diff --git a/LeanMachineLearning/Probability/Independence/CondDistrib.lean b/LeanMachineLearning/Probability/Independence/CondDistrib.lean
index 78696b15..25d8470a 100644
--- a/LeanMachineLearning/Probability/Independence/CondDistrib.lean
+++ b/LeanMachineLearning/Probability/Independence/CondDistrib.lean
@@ -212,7 +212,7 @@ lemma FiniteMeasure.sub_def (μ ν : FiniteMeasure α) :
   rfl
 
 @[simp, norm_cast]
-theorem FiniteMeasure.toMeasure_sub (μ ν : FiniteMeasure α) : ↑(μ - ν) = (↑μ - ↑ν : Measure α) :=
+lemma FiniteMeasure.toMeasure_sub (μ ν : FiniteMeasure α) : ↑(μ - ν) = (↑μ - ↑ν : Measure α) :=
   rfl
 
 instance : CanonicallyOrderedAdd (FiniteMeasure α) where
diff --git a/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean b/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean
index 78ffa84a..d73ec59e 100644
--- a/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean
+++ b/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean
@@ -19,7 +19,7 @@ namespace MeasurableSpace
 variable {δ : Type*} {X : δ → Type*} [m : ∀ a, MeasurableSpace (X a)] {α : Type*}
 
 -- Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
-theorem comap_pi {g : α → ∀ a, X a} : pi.comap g = ⨆ a, (m a).comap (fun x ↦ g x a) := by
+lemma comap_pi {g : α → ∀ a, X a} : pi.comap g = ⨆ a, (m a).comap (fun x ↦ g x a) := by
   simp_rw [pi, comap_iSup, comap_comp, comp_def]
 
 end MeasurableSpace
diff --git a/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean b/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean
index 098fb002..d63260e3 100644
--- a/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean
+++ b/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean
@@ -67,7 +67,7 @@ lemma MeasurableEquiv.coe_refl {α : Type*} {mα : MeasurableSpace α} :
     (MeasurableEquiv.refl α : α → α) = id := rfl
 
 set_option backward.isDefEq.respectTransparency false in
-theorem hasLaw_Iic_of_forall_hasCondDistrib' [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
+lemma hasLaw_Iic_of_forall_hasCondDistrib' [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
     {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N n : ℕ}
     (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P)
     (hn : n ≤ N) :
@@ -121,7 +121,7 @@ theorem hasLaw_Iic_of_forall_hasCondDistrib' [∀ n, StandardBorelSpace (X n)] [
     congr
     simp [MeasurableEquiv.coe_refl]
 
-theorem hasLaw_Iic_of_forall_hasCondDistrib [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
+lemma hasLaw_Iic_of_forall_hasCondDistrib [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
     {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P)
     (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P)
     (n : ℕ) :
@@ -136,7 +136,7 @@ lemma trajMeasure_map_frestrictLe (n : ℕ) :
   rw [trajMeasure, ← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc,
     Kernel.deterministic_comp_eq_map, traj_map_frestrictLe]
 
-theorem eq_trajMeasure_map_frestrictLe [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
+lemma eq_trajMeasure_map_frestrictLe [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
     {Y : (n : ℕ) → Ω → X n}
     (h0 : HasLaw (Y 0) μ₀ P) {N : ℕ}
     (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) :
@@ -146,7 +146,7 @@ theorem eq_trajMeasure_map_frestrictLe [∀ n, StandardBorelSpace (X n)] [∀ n,
 
 -- todo: switch to `HasLaw`
 /-- Uniqueness of `trajMeasure`. -/
-theorem eq_trajMeasure [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
+lemma eq_trajMeasure [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
     {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ n, Measurable (Y n))
     (h0 : HasLaw (Y 0) μ₀ P)
     (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) :
diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
index e6b9fc54..369e862b 100644
--- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean
+++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
@@ -641,7 +641,7 @@ lemma measurableSet_stepsUntil_eq [MeasurableSingletonClass 𝓐]
   exact measurable_comap_indicator_stepsUntil_eq hA hR' a m n
 
 /-- `stepsUntil a m` is a stopping time with respect to the filtration `filtrationAction`. -/
-theorem isStoppingTime_stepsUntil_filtrationAction [MeasurableSingletonClass 𝓐]
+lemma isStoppingTime_stepsUntil_filtrationAction [MeasurableSingletonClass 𝓐]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m : ℕ) :
     IsStoppingTime (IsAlgEnvSeq.filtrationAction hA hR') (stepsUntil A a m) := by
   refine isStoppingTime_of_measurableSet_eq fun n ↦ ?_
@@ -980,7 +980,7 @@ section CopiedFromPR
 
 open Set
 
-theorem _root_.MeasureTheory.StronglyMeasurable.div₀' {𝓐 β : Type*}
+lemma _root_.MeasureTheory.StronglyMeasurable.div₀' {𝓐 β : Type*}
     {m𝓐 : MeasurableSpace 𝓐} [TopologicalSpace β]
     [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β]
     [TopologicalSpace.PseudoMetrizableSpace β]
diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
index 9825e1fa..d36d9ef8 100644
--- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
+++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
@@ -50,7 +50,7 @@ variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'
   {P : Measure Ω} [IsProbabilityMeasure P] {P' : Measure Ω'} [IsProbabilityMeasure P']
   {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨} {N : ℕ}
 
-theorem eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) :
+lemma eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) :
     P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = trajMeasure alg env := by
   rw [trajMeasure]
   have h := Kernel.eq_trajMeasure (Y := fun n ω ↦ (A₁ n ω, R₁ n ω)) (P := P)
@@ -75,14 +75,14 @@ lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil
 
 /-- The law of the sequence of actions and observations generated by an algorithm-environment pair
 is unique: it does not depend on the probability space used. -/
-theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
+lemma isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
     (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
     P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by
   rw [eq_trajMeasure_of_isAlgEnvSeq h1, eq_trajMeasure_of_isAlgEnvSeq h2]
 
 /-- The law of the sequence of actions and observations generated by an algorithm-environment pair
 is unique: it does not depend on the probability space used. -/
-lemma IsAlgEnvSeq.identDistrib_trajectory (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
+theorem IsAlgEnvSeq.identDistrib_trajectory (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
     (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
     IdentDistrib (fun ω n ↦ (A₁ n ω, R₁ n ω)) (fun ω' n ↦ (A₂ n ω', R₂ n ω')) P P' where
   aemeasurable_fst := (measurable_pi_iff.2 fun n ↦ (h1.measurable_action n).prodMk
@@ -91,7 +91,7 @@ lemma IsAlgEnvSeq.identDistrib_trajectory (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
     (h2.measurable_feedback n)).aemeasurable
   map_eq := isAlgEnvSeq_unique h1 h2
 
-theorem isAlgEnvSeqUntil_unique (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N)
+lemma isAlgEnvSeqUntil_unique (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N)
     (h2 : IsAlgEnvSeqUntil A₂ R₂ alg env P' N) :
     P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
       P'.map (fun ω (n : Iic N) ↦ (A₂ n ω, R₂ n ω)) := by