Update to 4.30.0

.github/workflows/blueprint.yml

@@ -48,8 +48,8 @@ jobs:
         uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
         with:
           build: true
-          lint: false
-          mk_all-check: false
+          lint: true
+          mk_all-check: true
 
       - name: Build Verso Documentation
         run: |

LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean

@@ -513,7 +513,7 @@ lemma expectation_pullCount_le' [Nonempty (Fin K)]
     simp only [id_eq, Nat.cast_sum]
     rw [lintegral_add_left (by fun_prop), lintegral_add_left (by fun_prop)]
     simp only [lintegral_const, measure_univ, mul_one]
-    rw [lintegral_finset_sum _ (by fun_prop), lintegral_finset_sum _ (by fun_prop)]
+    rw [lintegral_finsetSum _ (by fun_prop), lintegral_finsetSum _ (by fun_prop)]
     gcongr with k hk k hk
     · rw [← lintegral_indicator_one]
       swap; · exact h_set_2 _

LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean

@@ -628,7 +628,7 @@ lemma indepFun_fst_add_one_aux (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ
     simp only [X, Y, Set.preimage_inter, Set.preimage_preimage]
     by_cases h : ω₁ (n + 1) ∈ s
     · simp [h]
-      grind
+      congr
     · simp [h]
   simp_rw [hY_fst, hX_fst, hXY]
   -- Factor the integral using independence
@@ -1191,8 +1191,8 @@ lemma hasCondDistrib_reward' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMa
     let e : ((𝓐 × ℕ) × (Iic n → 𝓐 × R)) ≃ᵐ ((𝓐 × (Iic n → 𝓐 × R)) × ℕ) :=
     { toFun := fun x ↦ ((x.1.1, x.2), x.1.2)
       invFun := fun x ↦ ((x.1.1, x.2), x.1.2)
-      measurable_toFun := by fun_prop
-      measurable_invFun := by fun_prop }
+      measurable_toFun := by simp only [Equiv.coe_fn_mk]; fun_prop
+      measurable_invFun := by simp only [Equiv.symm_mk, Equiv.coe_fn_mk]; fun_prop }
     exact this.comp_right e
   suffices HasCondDistrib R' (fun ω ↦ (A ω, P ω)) (ν.prodMkRight _) (arrayMeasure ν) by
     have h_indep : H ⟂ᵢ[(fun ω ↦ (A ω, P ω)), (by fun_prop); arrayMeasure ν] R' :=

LeanMachineLearning/Online/Bandit/Regret.lean

@@ -75,7 +75,7 @@ lemma integral_regret_eq_sum_gap_mul_integral_pullCount
     (hA : ∀ n, Measurable (A n)) :
     P[regret ν A n] = ∑ a, gap ν a * P[fun ω ↦ (pullCount A a n ω : ℝ)] := by
   simp_rw [regret_eq_sum_pullCount_mul_gap]
-  rw [integral_finset_sum]
+  rw [integral_finsetSum]
   swap; · exact fun i _ ↦ (integrable_pullCount hA i n).mul_const _
   congr with a
   rw [integral_mul_const, mul_comm]

LeanMachineLearning/Online/Bandit/SumRewards.lean

@@ -75,7 +75,8 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le (a : 𝓐) (n : ℕ)
   classical
   rcases Set.eq_empty_or_nonempty B with h_empty | h_nonempty
   · simp [h_empty]
-  convert prob_pullCount_prod_sumRewards_mem_le a n (hs.prod hB) (ν := ν) (alg := alg) with _ _ k hk
+  convert prob_pullCount_prod_sumRewards_mem_le a n (hs.prod hB) (ν := ν) (alg := alg)
+    with _ _ _ k hk
   · ext n
     have : ∃ x, x ∈ B := h_nonempty
     simp [this]
@@ -274,7 +275,7 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐]
   classical
   rcases Set.eq_empty_or_nonempty B with h_empty | h_nonempty
   · simp [h_empty]
-  convert prob_pullCount_prod_sumRewards_mem_le h (hs.prod hB) (ν := ν) (alg := alg) with _ _ k hk
+  convert prob_pullCount_prod_sumRewards_mem_le h (hs.prod hB) (ν := ν) (alg := alg) with _ _ _ k hk
   · ext n
     have : ∃ x, x ∈ B := h_nonempty
     simp [this]

LeanMachineLearning/Probability/Independence/CondDistrib.lean

@@ -10,6 +10,11 @@ public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 public import Mathlib.Probability.Independence.Basic
 public import Mathlib.Probability.Independence.Conditional
 
+/-!
+# Lemmas about conditional distributions
+
+-/
+
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory Finset
@@ -472,7 +477,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
         · simp only [hZ, Set.setOf_true, Set.mem_setOf_eq, Set.indicator_of_mem]
           exact κ.measure_le_bound _ _
         · simp [hZ]
-      refine le_antisymm (h_le.trans ?_) (zero_le _)
+      refine le_antisymm (h_le.trans ?_) zero_le
       rw [lintegral_indicator]
       swap; · exact (measurableSet_singleton _).preimage (by fun_prop)
       simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,

LeanMachineLearning/Probability/Independence/CondIndepFun.lean

@@ -9,11 +9,11 @@ public import Mathlib.MeasureTheory.Function.FactorsThrough
 public import Mathlib.Probability.Independence.Basic
 public import Mathlib.Probability.Independence.Conditional
 
-@[expose] public section
-
 /-! # Laws of `stepsUntil` and `rewardByCount`
 -/
 
+@[expose] public section
+
 open MeasureTheory ProbabilityTheory Finset
 open scoped ENNReal NNReal
 

LeanMachineLearning/Probability/Independence/IndepFun.lean

@@ -8,6 +8,9 @@ module
 public import Mathlib.Probability.IdentDistrib
 public import Mathlib.Probability.Independence.InfinitePi
 
+/-! # Lemmas about independence
+-/
+
 @[expose] public section
 
 open MeasureTheory Finset

LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean

@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Independence.InfinitePi
 
+/-! # Lemmas about independence and infinite products
+-/
+
 @[expose] public section
 
 open MeasureTheory Measure ProbabilityTheory Set Function

LeanMachineLearning/Probability/Integrable.lean

@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.IdentDistrib
 
+/-! # Lemmas about integrable functions
+-/
+
 @[expose] public section
 
 open ProbabilityTheory

LeanMachineLearning/Probability/Kernel/Basic.lean

@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Kernel.Basic
 
+/-! # Basic lemmas about Markov kernels
+-/
+
 @[expose] public section
 
 open MeasureTheory

LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean

@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Kernel.Composition.MapComap
 
+/-! # Lemmas about map and comap of Markov kernels
+-/
+
 @[expose] public section
 
 namespace ProbabilityTheory.Kernel

LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean

@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Kernel.Composition.MeasureCompProd
 
+/-! # Lemmas about measure composition-product
+-/
+
 @[expose] public section
 
 open ProbabilityTheory

LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean

@@ -9,6 +9,9 @@ public import LeanMachineLearning.Probability.HasCondDistrib
 public import Mathlib.Probability.Kernel.IonescuTulcea.Traj
 public import Mathlib.Probability.Process.FiniteDimensionalLaws
 
+/-! # Lemmas about `traj` and `trajMeasure`
+-/
+
 @[expose] public section
 
 open Filter Finset Function MeasurableEquiv MeasurableSpace MeasureTheory Preorder ProbabilityTheory

LeanMachineLearning/Probability/Kernel/KernelSub.lean

@@ -9,7 +9,7 @@ public import Mathlib.MeasureTheory.Measure.SubFinite
 public import Mathlib.Probability.Kernel.RadonNikodym
 
 /-!
-# Kernels substraction
+# Kernel substraction
 
 -/
 

LeanMachineLearning/Probability/Moments/SubGaussian.lean

@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Probability.Moments.SubGaussian
 
+/-! # Lemmas about sub-Gaussian random variables
+-/
+
 @[expose] public section
 
 open MeasureTheory Real
@@ -114,18 +117,18 @@ lemma measure_sum_le_sum_le [IsFiniteMeasure μ]
     (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]
+      rw [integral_finsetSum _ hX_int, Finset.sum_sub_distrib]
     refine sum_of_iIndepFun ?_ hX_subG
     exact hX_indep.comp (g := fun i x ↦ x - μ[X i]) (by fun_prop)
   · suffices HasSubgaussianMGF (fun ω ↦ ∑ j ∈ t, (Y j ω - μ[Y j])) (∑ j ∈ t, cY j) μ by
       convert this
-      rw [integral_finset_sum _ hY_int, Finset.sum_sub_distrib]
+      rw [integral_finsetSum _ hY_int, Finset.sum_sub_distrib]
     refine sum_of_iIndepFun ?_ hY_subG
     exact hY_indep.comp (g := fun i x ↦ x - μ[Y i]) (by fun_prop)
-  · rwa [integral_finset_sum _ hX_int, integral_finset_sum _ hY_int]
+  · rwa [integral_finsetSum _ hX_int, integral_finsetSum _ hY_int]
   · congr
-    · rw [integral_finset_sum _ hY_int]
-    · rw [integral_finset_sum _ hX_int]
+    · rw [integral_finsetSum _ hY_int]
+    · rw [integral_finsetSum _ hX_int]
 
 lemma measure_sum_le_sum_le' [IsFiniteMeasure μ]
     (hX_indep : iIndepFun X μ) (hY_indep : iIndepFun Y μ)

LeanMachineLearning/Probability/WithDensity.lean

@@ -8,6 +8,9 @@ module
 public import Mathlib.Probability.Kernel.CompProdEqIff
 public import Mathlib.Probability.Kernel.Composition.MeasureComp
 
+/-! # Lemmas about kernels and measures with density
+-/
+
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory

LeanMachineLearning/SequentialLearning/Algorithm.lean

@@ -59,7 +59,7 @@ 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 𝓐 𝓨) :
+def Algorithm.prodLeft (𝓧 : 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

LeanMachineLearning/SequentialLearning/FiniteActions.lean

@@ -233,11 +233,16 @@ lemma adapted_pullCount_add_one [MeasurableSingletonClass 𝓐]
   rw [← measurable_iff_comap_le]
   exact measurable_comp_comap _ (measurable_pullCount' n a)
 
+lemma stronglyAdapted_pullCount_add_one [MeasurableSingletonClass 𝓐]
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) :
+    StronglyAdapted (IsAlgEnvSeq.filtration hA hR') (fun n ↦ pullCount A a (n + 1)) :=
+  (adapted_pullCount_add_one hA hR' a).stronglyAdapted
+
 lemma isPredictable_pullCount [MeasurableSingletonClass 𝓐]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) :
-    IsPredictable (IsAlgEnvSeq.filtration hA hR') (pullCount A a) := by
-  rw [isPredictable_iff_measurable_add_one]
-  refine ⟨?_, adapted_pullCount_add_one hA hR' a⟩
+    IsStronglyPredictable (IsAlgEnvSeq.filtration hA hR') (pullCount A a) := by
+  rw [IsStronglyPredictable.iff_measurable_add_one]
+  refine ⟨?_, stronglyAdapted_pullCount_add_one hA hR' a⟩
   simp only [pullCount_zero]
   fun_prop
 
@@ -385,7 +390,7 @@ lemma action_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount A a (s + 1)
   have h_spec := Nat.find_spec h_exists
   have h_spec' n := Nat.find_min h_exists (m := n)
   by_cases h_zero : Nat.find h_exists = 0
-  · simp only [h_zero, zero_add, not_lt_zero', IsEmpty.forall_iff, implies_true] at *
+  · simp only [h_zero, zero_add, not_lt_zero, IsEmpty.forall_iff, implies_true] at *
     by_contra h_ne
     rw [← zero_add 1, pullCount_eq_pullCount_of_action_ne h_ne] at h_spec
     simp only [pullCount_zero] at h_spec
@@ -592,7 +597,8 @@ lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
     · simp only [hn, pullCount_zero]
       exact measurable_const
     have h_meas := adapted_pullCount_add_one hA hR' a (n - 1)
-    grind
+    have : 1 ≤ n := by grind
+    simpa [Nat.sub_add_cancel this] using h_meas
 
 lemma measurable_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
@@ -938,13 +944,14 @@ lemma measurable_uncurry_empMean' [MeasurableEq 𝓐] (n : ℕ) :
 lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
     {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
-    IsPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+    IsStronglyPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
       (sumRewards A R' a) := by
-  rw [isPredictable_iff_measurable_add_one]
+  rw [IsStronglyPredictable.iff_measurable_add_one]
   constructor
   · simp only [sumRewards_zero]
     fun_prop
-  refine fun n ↦ measurable_fun_sum _ fun i hi ↦ Measurable.ite ?_ ?_ (by fun_prop)
+  refine fun n ↦ Measurable.stronglyMeasurable ?_
+  refine measurable_fun_sum _ fun i hi ↦ Measurable.ite ?_ ?_ (by fun_prop)
   · refine (measurableSet_singleton a).preimage ?_
     have h_meas_i := IsAlgEnvSeq.adapted_action h.measurable_action h.measurable_feedback i
     simp only [mem_range] at hi
@@ -955,15 +962,22 @@ lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace 𝓐] [Nonempty 
     exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback).mono
       (by lia)) le_rfl
 
-lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
-    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
+lemma IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐]
+    {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
-    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+    StronglyAdapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
       (fun n ↦ sumRewards A R' a (n + 1)) := by
   have h_predictable := h.isPredictable_sumRewards a
-  rw [isPredictable_iff_measurable_add_one] at h_predictable
+  rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable
   exact h_predictable.2
 
+lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
+    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
+    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
+    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+      (fun n ↦ sumRewards A R' a (n + 1)) :=
+  (h.stronglyAdapted_sumRewards_add_one a).adapted
+
 section CopiedFromPR
 
 open Set
@@ -990,23 +1004,30 @@ end CopiedFromPR
 lemma IsAlgEnvSeq.isPredictable_empMean [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
     {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
-    IsPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+    IsStronglyPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
       (empMean A R' a) := by
   unfold empMean
   refine StronglyMeasurable.div₀' ?_ ?_
   · exact h.isPredictable_sumRewards a
   · have h_meas := (isPredictable_pullCount h.measurable_action h.measurable_feedback a).measurable
     fun_prop
 
-lemma IsAlgEnvSeq.adapted_empMean_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
-    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
+lemma IsAlgEnvSeq.stronglyAdapted_empMean_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐]
+    {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
-    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+    StronglyAdapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
       (fun n ↦ empMean A R' a (n + 1)) := by
   have h_predictable := h.isPredictable_empMean a
-  rw [isPredictable_iff_measurable_add_one] at h_predictable
+  rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable
   exact h_predictable.2
 
+lemma IsAlgEnvSeq.adapted_empMean_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
+    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
+    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
+    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
+      (fun n ↦ empMean A R' a (n + 1)) :=
+  (h.stronglyAdapted_empMean_add_one a).adapted
+
 end SumRewards
 
 end Learning

LeanMachineLearning/Tutorial/BasicProbability.lean

@@ -9,6 +9,9 @@ public import Mathlib.Probability.Distributions.Gaussian.Real
 public import Mathlib.Probability.Independence.Basic
 public import Mathlib.Probability.Moments.Basic
 
+/-! # Tutorial source file for basic probability
+-/
+
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory

LeanMachineLearning/Tutorial/MarkovKernel.lean

@@ -8,6 +8,9 @@ module
 public import Mathlib.Probability.Kernel.Composition.Lemmas
 public import Mathlib.Tactic.Recall
 
+/-! # Tutorial source file for Markov kernels
+-/
+
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory

LeanMachineLearning/Tutorial/Martingales.lean

@@ -9,6 +9,8 @@ public import Mathlib.Probability.Martingale.Convergence
 public import Mathlib.Probability.Martingale.OptionalStopping
 public import Mathlib.Probability.Martingale.OptionalSampling
 
+/-! # Tutorial source file for martingales -/
+
 @[expose] public section
 
 open Filter