From 6cc6776678a52b28ebf7557ba83342275ced9362 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sun, 17 May 2026 17:54:38 +0000 Subject: [PATCH 1/4] chore(bump): Lean v4.30.0-rc2 + mathlib v4.30.0-rc2 Bumps the toolchain from v4.27.0-rc1 to v4.30.0-rc2 and the mathlib pin to the matching tag. No source changes in this commit; build fixups for breakage introduced by the bump follow in subsequent tier commits. - lean-toolchain: leanprover/lean4:v4.27.0-rc1 -> v4.30.0-rc2 - lakefile.toml: mathlib rev v4.27.0-rc1 -> v4.30.0-rc2 - lake-manifest.json: regenerated via `lake update mathlib` --- lake-manifest.json | 35 ++++++++++++++++++----------------- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 20 insertions(+), 19 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 1ecf92b2..eb185bd1 100644 --- a/lake-manifest.json +++ b/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} diff --git a/lakefile.toml b/lakefile.toml index 4babc0af..eb7fb756 100644 --- a/lakefile.toml +++ b/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" diff --git a/lean-toolchain b/lean-toolchain index bd19bde0..6c7e31ff 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0-rc1 +leanprover/lean4:v4.30.0-rc2 From 0b29ddb6805b411365f95a23e0c55ce6210de699 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sun, 17 May 2026 17:59:11 +0000 Subject: [PATCH 2/4] =?UTF-8?q?fix(bump):=20tier=200-1=20=E2=80=94=20TailS?= =?UTF-8?q?igma=20comap=5FiSup=20proof?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `comap_shift_eq_iSup_comap_coords` no longer closes via `congr 1; ext k; rw [MeasurableSpace.comap_comp]` at v4.30.0-rc2: after the rewrite a residual `comap ((eval k) ∘ shift n) inst = comap (eval (n+k)) inst` is left, which is definitionally true but not closed by `congr` alone. Use `iSup_congr (fun k => ?_)` for the supremum, then `rw [MeasurableSpace.comap_comp]; rfl`. - Exchangeability/Tail/TailSigma.lean: replace `congr 1; ext k` step --- Exchangeability/Tail/TailSigma.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Exchangeability/Tail/TailSigma.lean b/Exchangeability/Tail/TailSigma.lean index c6280cf5..9a3721da 100644 --- a/Exchangeability/Tail/TailSigma.lean +++ b/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 From 683fe6cbedd7b5c7db7f59cb378e7eb936f743db Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sun, 17 May 2026 18:02:54 +0000 Subject: [PATCH 3/4] =?UTF-8?q?fix(bump):=20tier=202=20=E2=80=94=20Crossin?= =?UTF-8?q?gs=20StronglyAdapted=20rename?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit mathlib renamed `Adapted` -> `StronglyAdapted` on 2026-01-13 (see Mathlib/Probability/Process/Adapted.lean header note); the new `Adapted` requires plain `Measurable`, while the pre-rename `Adapted` (which the local proofs target) is now `StronglyAdapted`. The body `stronglyMeasurable_condExp.mono (h_le n)` already produces `StronglyMeasurable`, so only the annotation needs the rename. - Exchangeability/Probability/Martingale/Crossings.lean: rename two `have h_adapted : Adapted ℱ ...` annotations to `StronglyAdapted ℱ ...` (lines 594 and 621). --- Exchangeability/Probability/Martingale/Crossings.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Exchangeability/Probability/Martingale/Crossings.lean b/Exchangeability/Probability/Martingale/Crossings.lean index 7c4a9b68..cd855726 100644 --- a/Exchangeability/Probability/Martingale/Crossings.lean +++ b/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' From b6b2751ea05e33016e94c7b11b0ae7ab89dab178 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sun, 17 May 2026 18:12:54 +0000 Subject: [PATCH 4/4] =?UTF-8?q?fix(bump):=20tier=204=20=E2=80=94=20proof?= =?UTF-8?q?=20branches=20(ViaL2,=20ViaMartingale,=20ViaKoopman)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mathlib API renames between v4.27.0-rc1 and v4.30.0-rc2: - `integral_mul_left` -> `integral_const_mul` (ViaKoopman/ContractableFactorization.lean:752, ViaL2/AlphaConvergence.lean:320, ViaL2/MoreL2Helpers.lean:1386, ViaL2/DirectingMeasureIntegral.lean:1933) - `Set.indicator_of_not_mem` -> `Set.indicator_of_notMem` `Set.not_mem_compl_iff` -> `Set.notMem_compl_iff` (15 occurrences in ViaL2/DirectingMeasureIntegral.lean) - `hasFiniteIntegral_of_bounded` -> `HasFiniteIntegral.of_bounded` (ViaL2/MoreL2Helpers.lean:1307) - `Ne.lt_or_lt` -> `Ne.lt_or_gt` (signature renamed) (ViaL2/CesaroConvergence.lean:376) - `StrictAnti.lt_iff_lt` -> `StrictAnti.lt_iff_gt` (ViaL2/AlphaIicCE.lean:438) - `le_of_not_lt` -> `not_lt.mp` (generic lemma removed; use `not_lt` iff) (ViaL2/CesaroConvergence.lean:1526) Two `simp only` calls on `def`s no longer make progress at v4.30 (simp no longer auto-unfolds opaque `def`s). Replace with `show` of the unfolded form: - `simp only [futureFiltration]` -> `show … comap (shiftRV …) _` (ViaMartingale/FutureFiltration.lean:130) - `simp only [TailSigma.tailFamily]` -> `show … iSup (fun j => …)` (ViaL2/CesaroConvergence.lean:1995) One `calc` step LHS no longer matches the goal LHS after `simp only [ξ, p, q]` (different normal form in v4.30); collapse the three pure-`ring` calc steps into one bridging step from the new goal LHS form: - ViaL2/CesaroConvergence.lean:1119 --- .../ViaKoopman/ContractableFactorization.lean | 2 +- .../DeFinetti/ViaL2/AlphaConvergence.lean | 2 +- .../DeFinetti/ViaL2/AlphaIicCE.lean | 2 +- .../DeFinetti/ViaL2/CesaroConvergence.lean | 16 ++++------ .../ViaL2/DirectingMeasureIntegral.lean | 32 +++++++++---------- .../DeFinetti/ViaL2/MoreL2Helpers.lean | 4 +-- .../ViaMartingale/FutureFiltration.lean | 2 +- 7 files changed, 28 insertions(+), 32 deletions(-) diff --git a/Exchangeability/DeFinetti/ViaKoopman/ContractableFactorization.lean b/Exchangeability/DeFinetti/ViaKoopman/ContractableFactorization.lean index b1ccce32..b46509d6 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/ContractableFactorization.lean +++ b/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] diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean b/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean index 35a4ae02..c4d41dc0 100644 --- a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean b/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean index 0d35ba35..bd42a164 100644 --- a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean b/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean index 48f1414d..3d5d21b8 100644 --- a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean +++ b/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 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 diff --git a/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean b/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean index 15d18d33..21a72249 100644 --- a/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean b/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean index 7b2ee3b6..40ca0b6e 100644 --- a/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean +++ b/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 _ diff --git a/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean b/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean index 1c8aa0ea..4882e44f 100644 --- a/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean +++ b/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]