bump Lean to v4.30.0-rc2 + mathlib v4.30.0-rc2

Exchangeability/DeFinetti/ViaKoopman/ContractableFactorization.lean

@@ -749,7 +749,7 @@ theorem condexp_product_factorization_contractable
             ∏ i : Fin m, fs i (ω (i.val * (n + 1) + (j i).val)) ∂μ =
           (1 / ((n + 1) : ℝ)^m) * ∫ ω in s, ∑ j : Fin m → Fin (n + 1),
             ∏ i : Fin m, fs i (ω (i.val * (n + 1) + (j i).val)) ∂μ := by
-        rw [integral_mul_left]
+        rw [integral_const_mul]
 
       rw [h_rhs_eq]
 

Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean

@@ -317,7 +317,7 @@ lemma alphaIic_ae_eq_alphaIicCE
               have hm_pos' : 0 < (m : ℝ) := Nat.cast_pos.mpr hm_pos
               rw [abs_mul, abs_of_pos (one_div_pos.mpr hm_pos')]
         _ = (1/(m:ℝ)) * ∫ ω, |indIic t (X m ω) - indIic t (X 0 ω)| ∂μ := by
-              rw [integral_mul_left]
+              rw [integral_const_mul]
         _ ≤ (1/(m:ℝ)) * ∫ ω, |indIic t (X m ω)| + |indIic t (X 0 ω)| ∂μ := by
               gcongr
               -- gcongr creates 3 goals: integrability of LHS, RHS, and pointwise inequality

Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean

@@ -435,7 +435,7 @@ lemma alphaIicCE_right_continuous_at
     -- u is strictly anti, so m ≤ n implies u n ≤ u m
     have h_u_le : (u n : ℝ) ≤ (u m : ℝ) := by
       rcases hmn.lt_or_eq with h | h
-      · exact le_of_lt (Rat.cast_lt.mpr (u_anti.lt_iff_lt.mpr h))
+      · exact le_of_lt (Rat.cast_lt.mpr (u_anti.lt_iff_gt.mpr h))
       · simp [h]
     exact h_mono m n h_u_le
 

Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean

@@ -373,7 +373,7 @@ lemma kallenberg_L2_bound
       contradiction
 
     -- Case split on ordering
-    rcases hij'.lt_or_lt with h_lt | h_lt
+    rcases hij'.lt_or_gt with h_lt | h_lt
     · -- Case i' < j': Use contractable_map_pair directly
       have h_dist := Exchangeability.DeFinetti.L2Helpers.contractable_map_pair
         (X := Z) hZ_contract hZ_meas h_lt
@@ -1116,13 +1116,9 @@ private lemma cesaro_cauchy_rho_lt
     -- Should simplify to: n' * ∑_{i<n} Z_i - n * ∑_{j<n'} Z_j
     -- Expand RHS: n * n' * (∑ (if i<n then n⁻¹ else 0) * Z_i - ∑ (if j<n' then n'⁻¹ else 0) * Z_j)
     -- Using n * n' * n⁻¹ = n' and indicator sums
-    calc (↑n * m_mean + ∑ x ∈ Finset.range n, Z x ω) * ↑n' +
-          ↑n * (-(m_mean * ↑n') - ∑ x ∈ Finset.range n', Z x ω)
-        = ↑n * m_mean * ↑n' + (∑ x ∈ Finset.range n, Z x ω) * ↑n' +
-          ↑n * (-(m_mean * ↑n')) + ↑n * (- ∑ x ∈ Finset.range n', Z x ω) := by ring
-      _ = ↑n * m_mean * ↑n' + ↑n' * ∑ x ∈ Finset.range n, Z x ω +
-          (-(↑n * m_mean * ↑n')) + (-(↑n * ∑ x ∈ Finset.range n', Z x ω)) := by ring
-      _ = ↑n' * ∑ x ∈ Finset.range n, Z x ω - ↑n * ∑ x ∈ Finset.range n', Z x ω := by ring
+    calc ↑n' * (↑n * m_mean + ∑ x ∈ Finset.range n, Z x ω - ↑n * m_mean) -
+          ↑n * ∑ x ∈ Finset.range n', Z x ω
+        = ↑n' * ∑ x ∈ Finset.range n, Z x ω - ↑n * ∑ x ∈ Finset.range n', Z x ω := by ring
       _ = ↑n * ↑n' * (∑ x : Fin m, (if ↑x < n then (↑n)⁻¹ else 0) * Z (↑x) ω -
                       ∑ x : Fin m, (if ↑x < n' then (↑n')⁻¹ else 0) * Z (↑x) ω) := by
         -- RHS: distribute n * n' and simplify conditionals
@@ -1527,7 +1523,7 @@ private lemma blockAvg_cauchy_in_L2
         σSq hσ_pos rfl ρ hρ_bd rfl hρ_lt Cf rfl ε hε
 
     · -- Edge case: ρ = 1 (perfect correlation) → blockAvg values are ae-equal
-      have hρ_eq : ρ = 1 := le_antisymm hρ_bd.2 (le_of_not_lt hρ_lt)
+      have hρ_eq : ρ = 1 := le_antisymm hρ_bd.2 (not_lt.mp hρ_lt)
       -- When ρ = 1, Z_i = Z_0 a.e., so blockAvg values are equal a.e.
       -- Note: We only prove this for n, n' > 0, which suffices since we use N = 1 below.
       -- (The general case for all n, n' ∈ ℕ is also true, but not needed.)
@@ -1996,7 +1992,7 @@ lemma blockAvg_measurable_tailFamily
   -- tailFamily X m = iSup (fun j => comap (X (m + j)))
   -- X (m + k) ω = (fun j => X (m + j) ω) k, so it's the k-th coordinate
   -- of the shifted sequence, which is measurable by comap construction
-  simp only [TailSigma.tailFamily]
+  show Measurable[iSup (fun j : ℕ => MeasurableSpace.comap (fun ω => X (m + j) ω) inferInstance)] _
   apply Measurable.of_comap_le
   exact le_iSup (fun j => MeasurableSpace.comap (fun ω => X (m + j) ω) inferInstance) k
 

Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean

@@ -457,8 +457,8 @@ lemma integral_indicator_borel_tailAEStronglyMeasurable
             1 - t.indicator (fun _ => (1:ℝ)) x := by
           intro x
           by_cases hx : x ∈ t
-          · simp [Set.indicator_of_mem hx, Set.indicator_of_not_mem (Set.not_mem_compl_iff.mpr hx)]
-          · simp [Set.indicator_of_not_mem hx, Set.indicator_of_mem (Set.mem_compl hx)]
+          · simp [Set.indicator_of_mem hx, Set.indicator_of_notMem (Set.notMem_compl_iff.mpr hx)]
+          · simp [Set.indicator_of_notMem hx, Set.indicator_of_mem (Set.mem_compl hx)]
         simp_rw [h_ind_compl]
         rw [integral_sub (integrable_const 1), integral_const, measureReal_univ_eq_one, one_smul]
         exact (integrable_const 1).indicator ht_meas
@@ -492,10 +492,10 @@ lemma integral_indicator_borel_tailAEStronglyMeasurable
               exact (hdisj n m (Ne.symm hm)).ne_of_mem hn hxm rfl
             rw [tsum_eq_single n]
             · simp [Set.indicator_of_mem hn]
-            · intro m hm; simp [Set.indicator_of_not_mem (h_unique m hm)]
-          · simp only [Set.indicator_of_not_mem hx]
+            · intro m hm; simp [Set.indicator_of_notMem (h_unique m hm)]
+          · simp only [Set.indicator_of_notMem hx]
             have : ∀ n, x ∉ f n := fun n hn => hx (Set.mem_iUnion.mpr ⟨n, hn⟩)
-            simp [Set.indicator_of_not_mem (this _)]
+            simp [Set.indicator_of_notMem (this _)]
         simp_rw [h_ind_union]
         -- integral of tsum = tsum of integrals (for nonneg functions)
         rw [integral_tsum]
@@ -1000,8 +1000,8 @@ lemma setIntegral_directing_measure_indicator_eq
               1 - t.indicator (fun _ => (1:ℝ)) x := by
             intro x
             by_cases hx : x ∈ t
-            · simp [Set.indicator_of_mem hx, Set.indicator_of_not_mem (Set.not_mem_compl_iff.mpr hx)]
-            · simp [Set.indicator_of_not_mem hx, Set.indicator_of_mem (Set.mem_compl hx)]
+            · simp [Set.indicator_of_mem hx, Set.indicator_of_notMem (Set.notMem_compl_iff.mpr hx)]
+            · simp [Set.indicator_of_notMem hx, Set.indicator_of_mem (Set.mem_compl hx)]
           simp_rw [h_ind_compl]
           rw [integral_sub (integrable_const 1), integral_const, measureReal_univ_eq_one, one_smul]
           exact (integrable_const 1).indicator ht_meas
@@ -1034,8 +1034,8 @@ lemma setIntegral_directing_measure_indicator_eq
             1 - t.indicator (fun _ => (1:ℝ)) (X 0 ω) := by
           intro ω
           by_cases hx : X 0 ω ∈ t
-          · simp [Set.indicator_of_mem hx, Set.indicator_of_not_mem (Set.not_mem_compl_iff.mpr hx)]
-          · simp [Set.indicator_of_not_mem hx, Set.indicator_of_mem (Set.mem_compl hx)]
+          · simp [Set.indicator_of_mem hx, Set.indicator_of_notMem (Set.notMem_compl_iff.mpr hx)]
+          · simp [Set.indicator_of_notMem hx, Set.indicator_of_mem (Set.mem_compl hx)]
         simp_rw [h_ind_compl]
         rw [integral_sub, integral_const]
         · exact (integrable_const 1).integrableOn
@@ -1072,10 +1072,10 @@ lemma setIntegral_directing_measure_indicator_eq
                 intro m hm hxm; exact (hdisj n m (Ne.symm hm)).ne_of_mem hn hxm rfl
               rw [tsum_eq_single n]
               · simp [Set.indicator_of_mem hn]
-              · intro m hm; simp [Set.indicator_of_not_mem (h_unique m hm)]
-            · simp only [Set.indicator_of_not_mem hx]
+              · intro m hm; simp [Set.indicator_of_notMem (h_unique m hm)]
+            · simp only [Set.indicator_of_notMem hx]
               have : ∀ n, x ∉ f n := fun n hn => hx (Set.mem_iUnion.mpr ⟨n, hn⟩)
-              simp [Set.indicator_of_not_mem (this _)]
+              simp [Set.indicator_of_notMem (this _)]
           simp_rw [h_ind_union]
           rw [integral_tsum]
           · exact fun n => (measurable_const.indicator (hf n).1).aestronglyMeasurable
@@ -1159,10 +1159,10 @@ lemma setIntegral_directing_measure_indicator_eq
               intro m hm hxm; exact (hdisj n m (Ne.symm hm)).ne_of_mem hn hxm rfl
             rw [tsum_eq_single n]
             · simp [Set.indicator_of_mem hn]
-            · intro m hm; simp [Set.indicator_of_not_mem (h_unique m hm)]
-          · simp only [Set.indicator_of_not_mem hx]
+            · intro m hm; simp [Set.indicator_of_notMem (h_unique m hm)]
+          · simp only [Set.indicator_of_notMem hx]
             have : ∀ n, X 0 ω ∉ f n := fun n hn => hx (Set.mem_iUnion.mpr ⟨n, hn⟩)
-            simp [Set.indicator_of_not_mem (this _)]
+            simp [Set.indicator_of_notMem (this _)]
         simp_rw [h_ind_union]
         rw [integral_tsum]
         · intro n
@@ -1930,7 +1930,7 @@ lemma directing_measure_integral_via_chain
             _ = ∫ ω, |M| * |(1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω) - α_g ω| ∂μ := by
                   congr 1; ext ω; rw [← mul_sub, abs_mul]
             _ = |M| * ∫ ω, |(1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω) - α_g ω| ∂μ := by
-                  rw [integral_mul_left]
+                  rw [integral_const_mul]
             _ < |M| * (ε / (|M| + 1)) := by
                   gcongr; exact hM_idx m hm
             _ < (|M| + 1) * (ε / (|M| + 1)) := by

Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean

@@ -1304,7 +1304,7 @@ lemma integral_alphaIic_eq_marginal
     -- Use tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top with p = 1
     have h_A_int : ∀ m, Integrable (A m) μ := fun m => by
       refine ⟨(hA_meas m).aestronglyMeasurable, ?_⟩
-      apply hasFiniteIntegral_of_bounded (C := 1)
+      apply HasFiniteIntegral.of_bounded (C := 1)
       filter_upwards with ω
       rw [Real.norm_eq_abs]
       by_cases hm : m = 0
@@ -1383,7 +1383,7 @@ lemma integral_alphaIic_eq_marginal
     have h_int_sum : ∫ ω, A m ω ∂μ =
         (1/(m:ℝ)) * ∑ k : Fin m, ∫ ω, ind (X (0 + k.val + 1) ω) ∂μ := by
       simp only [A]
-      rw [integral_mul_left]
+      rw [integral_const_mul]
       congr 1
       rw [integral_finset_sum]
       intro k _

Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean

@@ -127,7 +127,7 @@ lemma preimage_measurable_in_futureFiltration {Ω α : Type*} [MeasurableSpace 
   -- futureFiltration X m = comap (shiftRV X (m+1))
   -- X (m + k) = X (m + 1 + (k-1)) = π_{k-1} ∘ shiftRV X (m+1)
   -- where π_n projects to the n-th coordinate
-  simp only [futureFiltration]
+  show MeasurableSet[MeasurableSpace.comap (shiftRV X (m + 1)) inferInstance] _
   have : X (m + k) = (fun f : ℕ → α => f (k - 1)) ∘ shiftRV X (m + 1) :=
     funext fun ω => by simp [shiftRV]; congr 1; omega
   rw [this, Set.preimage_comp]

Exchangeability/Probability/Martingale/Crossings.lean

@@ -591,7 +591,7 @@ lemma condExp_exists_ae_limit_antitone
           le' := fun _ => le_refl _
         }
         -- The process μ[f | 𝔽 n] is adapted to this constant filtration
-        have h_adapted : Adapted ℱ (fun n => μ[f | 𝔽 n]) := by
+        have h_adapted : StronglyAdapted ℱ (fun n => μ[f | 𝔽 n]) := by
           intro n
           exact stronglyMeasurable_condExp.mono (h_le n)
         -- Apply measurability for adapted processes
@@ -618,7 +618,7 @@ lemma condExp_exists_ae_limit_antitone
       mono' := fun _ _ _ => le_refl _
       le' := fun _ => le_refl _
     }
-    have h_adapted : Adapted ℱ (fun n => μ[f | 𝔽 n]) := by
+    have h_adapted : StronglyAdapted ℱ (fun n => μ[f | 𝔽 n]) := by
       intro n
       exact stronglyMeasurable_condExp.mono (h_le n)
     exact h_adapted.measurable_upcrossings hab'

Exchangeability/Tail/TailSigma.lean

@@ -241,9 +241,9 @@ lemma comap_shift_eq_iSup_comap_coords (n : ℕ) :
   -- Distribute comap over supremum
   rw [MeasurableSpace.comap_iSup]
   -- Compose: (eval k) ∘ (shift n) = eval (n+k)
-  congr 1
-  ext k
+  refine iSup_congr (fun k => ?_)
   rw [MeasurableSpace.comap_comp]
+  rfl
 
 omit [MeasurableSpace Ω] in
 /-- Helper: Each `tailFamily X n` equals the pullback along the sample-path map of the

lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/PatrickMassot/checkdecls.git",
@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "32d24245c7a12ded17325299fd41d412022cd3fe",
+   "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.30.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
+   "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
+   "rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,51 +55,52 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.84",
+   "inputRev": "v0.0.98",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb12f5535c80e40119286d9575c9393562252d21",
+   "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
+   "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
+   "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+   "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "exchangeability",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lakefile.toml

@@ -5,7 +5,7 @@ defaultTargets = ["Exchangeability", "ForMathlib"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.27.0-rc1"
+rev = "v4.30.0-rc2"
 
 [[require]]
 name = "checkdecls"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0-rc1
+leanprover/lean4:v4.30.0-rc2