From 667401f1f41737578820f3ac78fd7633f705e172 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 21 Dec 2023 18:46:33 +0000 Subject: [PATCH] Bump mathlib --- LeanCamCombi.lean | 1 - LeanCamCombi/BernoulliSeq.lean | 4 +- .../SimpleGraph/Containment.lean | 4 +- .../MeasureTheory/Measure/MeasureSpace.lean | 70 ------------------- .../MeasureTheory/Measure/Typeclasses.lean | 6 +- .../Probability/Independence/Basic.lean | 1 - .../Constructions.lean | 1 - lake-manifest.json | 4 +- 8 files changed, 8 insertions(+), 83 deletions(-) delete mode 100644 LeanCamCombi/Mathlib/MeasureTheory/Measure/MeasureSpace.lean diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean index 455bd467f8..f231075d0b 100644 --- a/LeanCamCombi.lean +++ b/LeanCamCombi.lean @@ -47,7 +47,6 @@ import LeanCamCombi.Mathlib.Data.Set.Image import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup import LeanCamCombi.Mathlib.GroupTheory.Subgroup.Stabilizer -import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace import LeanCamCombi.Mathlib.MeasureTheory.Measure.Typeclasses import LeanCamCombi.Mathlib.Order.Category.BoolAlg import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic diff --git a/LeanCamCombi/BernoulliSeq.lean b/LeanCamCombi/BernoulliSeq.lean index 37f65c82ff..57296246ac 100644 --- a/LeanCamCombi/BernoulliSeq.lean +++ b/LeanCamCombi/BernoulliSeq.lean @@ -82,8 +82,8 @@ protected lemma meas [Fintype α] (s : Finset α) : Finset.prod_eq_pow_card, Finset.card_compl] · rintro a hi rw [Finset.mem_compl] at hi - simp only [hi, ←compl_setOf, NullMeasurableSet.prob_compl_eq_one_sub, mem_setOf_eq, - Finset.mem_coe, iff_false_iff, hX.nullMeasurableSet, hX.meas_apply] + simp only [hi, ←compl_setOf, prob_compl_eq_one_sub₀, mem_setOf_eq, Finset.mem_coe, + iff_false_iff, hX.nullMeasurableSet, hX.meas_apply] · rintro a hi simp only [hi, mem_setOf_eq, Finset.mem_coe, iff_true_iff, hX.meas_apply] rintro a diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean index 03bd0a7c95..f19d4c168e 100644 --- a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean +++ b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean @@ -184,8 +184,8 @@ noncomputable def copyCount (G : SimpleGraph α) (H : SimpleGraph β) : ℕ := haveI : IsEmpty (⊥ : H.Subgraph).verts := by simp refine' ⟨⟨⟨⟨isEmptyElim, isEmptyElim, isEmptyElim, isEmptyElim⟩, fun {a} ↦ isEmptyElim a⟩⟩, fun H' e ↦ Subgraph.ext _ _ _ $ funext₂ fun a b ↦ _⟩ - · simpa [Set.eq_empty_iff_forall_not_mem, filter_eq_empty_iff] using - Fintype.card_congr e.toEquiv.symm + · simpa [Set.eq_empty_iff_forall_not_mem, filter_eq_empty_iff, ‹IsEmpty α›] using + e.toEquiv.symm.isEmpty_congr · simp only [Subgraph.not_bot_adj, eq_iff_iff, iff_false_iff] exact fun hab ↦ e.symm.map_rel_iff.2 hab.coe diff --git a/LeanCamCombi/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/LeanCamCombi/Mathlib/MeasureTheory/Measure/MeasureSpace.lean deleted file mode 100644 index dbdbcbb0d1..0000000000 --- a/LeanCamCombi/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ /dev/null @@ -1,70 +0,0 @@ -import Mathlib.Logic.Lemmas -import Mathlib.MeasureTheory.Measure.MeasureSpace - -open Function MeasureTheory Set -open scoped ENNReal MeasureTheory - -variable {α β : Type*} [MeasurableSpace β] {f g : α → β} {s : Set β} - -namespace MeasureTheory -variable [MeasurableSpace α] {μ : Measure α} - -namespace Measure - -@[simp] lemma map_eq_zero_iff (hf : AEMeasurable f μ) : μ.map f = 0 ↔ μ = 0 := by - refine' ⟨fun h ↦ _, _⟩ - · replace h := congr_fun (congr_arg (↑) h) Set.univ - rwa [map_apply_of_aemeasurable hf MeasurableSet.univ, Set.preimage_univ, coe_zero, - Pi.zero_apply, measure_univ_eq_zero] at h - · rintro rfl - exact Measure.map_zero _ - -@[simp] lemma mapₗ_eq_zero_iff (hf : Measurable f) : Measure.mapₗ f μ = 0 ↔ μ = 0 := by - classical - rw [←map_eq_zero_iff hf.aemeasurable, map, dif_pos hf.aemeasurable, - mapₗ_congr hf hf.aemeasurable.measurable_mk] - exact hf.aemeasurable.ae_eq_mk - -lemma map_ne_zero_iff (hf : AEMeasurable f μ) : μ.map f ≠ 0 ↔ μ ≠ 0 := (map_eq_zero_iff hf).not -lemma mapₗ_ne_zero_iff (hf : Measurable f) : Measure.mapₗ f μ ≠ 0 ↔ μ ≠ 0 := - (mapₗ_eq_zero_iff hf).not - -end Measure - -end MeasureTheory - -namespace MeasurableSpace -variable [BooleanAlgebra β] (p : α → Prop) - -lemma comap_of_involutive {g : β → β} (hg : Involutive g) (hg' : Measurable g) (f : α → β) : - MeasurableSpace.comap (fun a ↦ g (f a)) inferInstance = - MeasurableSpace.comap f inferInstance := by - ext - set e : Set β ≃ Set β := - { toFun := preimage g - invFun := preimage g - left_inv := hg.preimage - right_inv := hg.preimage } - refine' e.exists_congr_left.trans (exists_congr fun t ↦ _) - simp only [preimage_preimage, compl_compl, Equiv.coe_fn_symm_mk, and_congr_left_iff, hg _] - rintro rfl - refine' ⟨fun ht ↦ _, fun ht ↦ hg' ht⟩ - convert hg' ht - simp_rw [preimage_preimage, hg _, preimage_id'] - -end MeasurableSpace - -lemma AEMeasurable.nullMeasurableSet_preimage [MeasurableSpace α] {μ : Measure α} - (hf : AEMeasurable f μ) (hs : MeasurableSet s) : NullMeasurableSet (f ⁻¹' s) μ := - ⟨hf.mk _ ⁻¹' s, hf.measurable_mk hs, hf.ae_eq_mk.preimage _⟩ - -namespace MeasureTheory -variable [MeasurableSpace α] {μ : Measure α} {s : Set α} - -nonrec lemma NullMeasurableSet.measure_compl (h : NullMeasurableSet s μ) (hs : μ s ≠ ∞) : - μ sᶜ = μ Set.univ - μ s := by - rw [←measure_congr h.toMeasurable_ae_eq, ←measure_compl (measurableSet_toMeasurable _ _)] - · exact measure_congr h.toMeasurable_ae_eq.symm.compl - · rwa [measure_congr h.toMeasurable_ae_eq] - -end MeasureTheory diff --git a/LeanCamCombi/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/LeanCamCombi/Mathlib/MeasureTheory/Measure/Typeclasses.lean index 8b1036f049..478db06d1e 100644 --- a/LeanCamCombi/Mathlib/MeasureTheory/Measure/Typeclasses.lean +++ b/LeanCamCombi/Mathlib/MeasureTheory/Measure/Typeclasses.lean @@ -1,13 +1,11 @@ import Mathlib.MeasureTheory.Measure.Typeclasses -import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace variable {α β : Type*} [MeasurableSpace β] {f g : α → β} {s : Set β} namespace MeasureTheory variable [MeasurableSpace α] {μ : Measure α} {s : Set α} -lemma NullMeasurableSet.prob_compl_eq_one_sub [IsProbabilityMeasure μ] {s : Set α} - (h : NullMeasurableSet s μ) : μ (sᶜ) = 1 - μ s := by - rw [h.measure_compl (measure_ne_top _ _), measure_univ] +lemma prob_compl_eq_one_sub₀ [IsProbabilityMeasure μ] {s : Set α} (h : NullMeasurableSet s μ) : + μ sᶜ = 1 - μ s := by rw [measure_compl₀ h (measure_ne_top _ _), measure_univ] end MeasureTheory diff --git a/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean b/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean index a6d384d6ea..bcdad1abbb 100644 --- a/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean +++ b/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean @@ -1,5 +1,4 @@ import Mathlib.Probability.Independence.Basic -import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace open MeasureTheory MeasurableSpace Set open scoped BigOperators diff --git a/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean b/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean index b8d93c7118..cb7b35bea4 100644 --- a/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean +++ b/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean @@ -1,5 +1,4 @@ import Mathlib.Probability.ProbabilityMassFunction.Constructions -import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace -- TODO: On a countable space, define one-to-one correspondance between `PMF` and probability -- measures diff --git a/lake-manifest.json b/lake-manifest.json index 079c654093..6b8261e982 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "6b4cf96c89e53cfcd73350bbcd90333a051ff4f0", + "rev": "5bf9172331fb4de21647a919c64d3569839b63c6", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "4160b2aa344c39b1238e7c5da7227f763ac72b58", + "rev": "da34c254e89b2cde09d066068c17cf30ebe603f8", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,