Update to 4.30.0 (#114)

Author: RemyDegenne

.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