From 3aa2b3b733ef69a7d542952e2e61984849e0dc3b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 31 Oct 2023 11:24:44 +0000 Subject: [PATCH] feat: Independence of singletons (#7251) Port a bit of https://github.com/leanprover-community/mathlib/pull/18506, but it's mostly handmade. Co-authored-by: RemyDegenne --- Mathlib/Probability/Independence/Basic.lean | 89 ++++++++++++++++++-- Mathlib/Probability/Independence/Kernel.lean | 81 +++++++++++++++++- 2 files changed, 162 insertions(+), 8 deletions(-) diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean index 8dabbb42151f5..2367bbec20328 100644 --- a/Mathlib/Probability/Independence/Basic.lean +++ b/Mathlib/Probability/Independence/Basic.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne -/ import Mathlib.Probability.Independence.Kernel -#align_import probability.independence.basic from "leanprover-community/mathlib"@"2f8347015b12b0864dfaf366ec4909eb70c78740" +#align_import probability.independence.basic from "leanprover-community/mathlib"@"001ffdc42920050657fd45bd2b8bfbec8eaaeb29" /-! # Independence of sets of sets and measure spaces (σ-algebras) @@ -66,15 +66,13 @@ when defining `μ` in the example above, the measurable space used is the last o Part A, Chapter 4. -/ -set_option autoImplicit true - -open MeasureTheory MeasurableSpace +open MeasureTheory MeasurableSpace Set open scoped BigOperators MeasureTheory ENNReal namespace ProbabilityTheory -variable {Ω ι : Type*} +variable {Ω ι β γ : Type*} {κ : ι → Type*} section Definitions @@ -145,12 +143,23 @@ def IndepFun {β γ} [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace end Definitions section Definition_lemmas +variable {π : ι → Set (Set Ω)} {m : ι → MeasurableSpace Ω} {_ : MeasurableSpace Ω} {μ : Measure Ω} + {S : Finset ι} {s : ι → Set Ω} lemma iIndepSets_iff [MeasurableSpace Ω] (π : ι → Set (Set Ω)) (μ : Measure Ω) : iIndepSets π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → f i ∈ π i), μ (⋂ i ∈ s, f i) = ∏ i in s, μ (f i) := by simp only [iIndepSets, kernel.iIndepSets, ae_dirac_eq, Filter.eventually_pure, kernel.const_apply] +lemma iIndepSets.meas_biInter (h : iIndepSets π μ) (s : Finset ι) {f : ι → Set Ω} + (hf : ∀ i, i ∈ s → f i ∈ π i) : μ (⋂ i ∈ s, f i) = ∏ i in s, μ (f i) := + (iIndepSets_iff _ _).1 h s hf + +lemma iIndepSets.meas_iInter [Fintype ι] (h : iIndepSets π μ) (hs : ∀ i, s i ∈ π i) : + μ (⋂ i, s i) = ∏ i, μ (s i) := by simp [←h.meas_biInter _ fun _i _ ↦ hs _] +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_sets.meas_Inter ProbabilityTheory.iIndepSets.meas_iInter + lemma IndepSets_iff [MeasurableSpace Ω] (s1 s2 : Set (Set Ω)) (μ : Measure Ω) : IndepSets s1 s2 μ ↔ ∀ t1 t2 : Set Ω, t1 ∈ s1 → t2 ∈ s2 → (μ (t1 ∩ t2) = μ t1 * μ t2) := by simp only [IndepSets, kernel.IndepSets, ae_dirac_eq, Filter.eventually_pure, kernel.const_apply] @@ -159,11 +168,20 @@ lemma iIndep_iff_iIndepSets (m : ι → MeasurableSpace Ω) [MeasurableSpace Ω] iIndep m μ ↔ iIndepSets (fun x ↦ {s | MeasurableSet[m x] s}) μ := by simp only [iIndep, iIndepSets, kernel.iIndep] +lemma iIndep.iIndepSets' {m : ι → MeasurableSpace Ω} (hμ : iIndep m μ) : + iIndepSets (fun x ↦ {s | MeasurableSet[m x] s}) μ := (iIndep_iff_iIndepSets _ _).1 hμ + lemma iIndep_iff (m : ι → MeasurableSpace Ω) [MeasurableSpace Ω] (μ : Measure Ω) : iIndep m μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → MeasurableSet[m i] (f i)), μ (⋂ i ∈ s, f i) = ∏ i in s, μ (f i) := by simp only [iIndep_iff_iIndepSets, iIndepSets_iff]; rfl +lemma iIndep.meas_biInter (hμ : iIndep m μ) (hs : ∀ i, i ∈ S → MeasurableSet[m i] (s i)) : + μ (⋂ i ∈ S, s i) = ∏ i in S, μ (s i) := (iIndep_iff _ _).1 hμ _ hs + +lemma iIndep.meas_iInter [Fintype ι] (hμ : iIndep m μ) (hs : ∀ i, MeasurableSet[m i] (s i)) : + μ (⋂ i, s i) = ∏ i, μ (s i) := by simp [←hμ.meas_biInter fun _ _ ↦ hs _] + lemma Indep_iff_IndepSets (m₁ m₂ : MeasurableSpace Ω) [MeasurableSpace Ω] (μ : Measure Ω) : Indep m₁ m₂ μ ↔ IndepSets {s | MeasurableSet[m₁] s} {s | MeasurableSet[m₂] s} μ := by simp only [Indep, IndepSets, kernel.Indep] @@ -197,6 +215,10 @@ lemma iIndepFun_iff_iIndep [MeasurableSpace Ω] {β : ι → Type*} iIndepFun m f μ ↔ iIndep (fun x ↦ (m x).comap (f x)) μ := by simp only [iIndepFun, iIndep, kernel.iIndepFun] +protected lemma iIndepFun.iIndep {m : ∀ i, MeasurableSpace (κ i)} {f : ∀ x : ι, Ω → κ x} + (hf : iIndepFun m f μ) : + iIndep (fun x ↦ (m x).comap (f x)) μ := hf + lemma iIndepFun_iff [MeasurableSpace Ω] {β : ι → Type*} (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x) (μ : Measure Ω) : iIndepFun m f μ ↔ ∀ (s : Finset ι) {f' : ι → Set Ω} @@ -204,6 +226,14 @@ lemma iIndepFun_iff [MeasurableSpace Ω] {β : ι → Type*} μ (⋂ i ∈ s, f' i) = ∏ i in s, μ (f' i) := by simp only [iIndepFun_iff_iIndep, iIndep_iff] +lemma iIndepFun.meas_biInter {m : ∀ i, MeasurableSpace (κ i)} {f : ∀ x : ι, Ω → κ x} + (hf : iIndepFun m f μ) (hs : ∀ i, i ∈ S → MeasurableSet[(m i).comap (f i)] (s i)) : + μ (⋂ i ∈ S, s i) = ∏ i in S, μ (s i) := hf.iIndep.meas_biInter hs + +lemma iIndepFun.meas_iInter [Fintype ι] {m : ∀ i, MeasurableSpace (κ i)} {f : ∀ x : ι, Ω → κ x} + (hf : iIndepFun m f μ) (hs : ∀ i, MeasurableSet[(m i).comap (f i)] (s i)) : + μ (⋂ i, s i) = ∏ i, μ (s i) := hf.iIndep.meas_iInter hs + lemma IndepFun_iff_Indep [MeasurableSpace Ω] [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : Measure Ω) : IndepFun f g μ ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ := by @@ -215,6 +245,12 @@ lemma IndepFun_iff {β γ} [MeasurableSpace Ω] [mβ : MeasurableSpace β] [mγ → MeasurableSet[MeasurableSpace.comap g mγ] t2 → μ (t1 ∩ t2) = μ t1 * μ t2 := by rw [IndepFun_iff_Indep, Indep_iff] +lemma IndepFun.meas_inter [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] {f : Ω → β} {g : Ω → γ} + (hfg : IndepFun f g μ) {s t : Set Ω} (hs : MeasurableSet[mβ.comap f] s) + (ht : MeasurableSet[mγ.comap g] t) : + μ (s ∩ t) = μ s * μ t := + (IndepFun_iff _ _ _).1 hfg _ _ hs ht + end Definition_lemmas section Indep @@ -472,7 +508,7 @@ theorem iIndepSets.iIndep [IsProbabilityMeasure μ] (m : ι → MeasurableSpace iIndep m μ := kernel.iIndepSets.iIndep m h_le π h_pi h_generate h_ind set_option linter.uppercaseLean3 false in -#align probability_theory.Indep_sets.Indep ProbabilityTheory.IndepSets.indep +#align probability_theory.Indep_sets.Indep ProbabilityTheory.iIndepSets.iIndep end FromPiSystemsToMeasurableSpaces @@ -486,7 +522,7 @@ We prove the following equivalences on `IndepSet`, for measurable sets `s, t`. -/ -variable {s t : Set Ω} (S T : Set (Set Ω)) +variable {_ : MeasurableSpace Ω} {μ : Measure Ω} {s t : Set Ω} (S T : Set (Set Ω)) theorem indepSet_iff_indepSets_singleton {_m0 : MeasurableSpace Ω} (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (μ : Measure Ω := by volume_tac) @@ -521,6 +557,45 @@ theorem indep_iff_forall_indepSet (m₁ m₂ : MeasurableSpace Ω) {_m0 : Measur kernel.indep_iff_forall_indepSet m₁ m₂ _ _ #align probability_theory.indep_iff_forall_indep_set ProbabilityTheory.indep_iff_forall_indepSet +theorem iIndep_comap_mem_iff {f : ι → Set Ω} : + iIndep (fun i => MeasurableSpace.comap (· ∈ f i) ⊤) μ ↔ iIndepSet f μ := + kernel.iIndep_comap_mem_iff +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_comap_mem_iff ProbabilityTheory.iIndep_comap_mem_iff + +alias ⟨_, iIndepSet.iIndep_comap_mem⟩ := iIndep_comap_mem_iff +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_set.Indep_comap_mem ProbabilityTheory.iIndepSet.iIndep_comap_mem + +theorem iIndepSets_singleton_iff {s : ι → Set Ω} : + iIndepSets (fun i ↦ {s i}) μ ↔ ∀ t, μ (⋂ i ∈ t, s i) = ∏ i in t, μ (s i) := by + simp_rw [iIndepSets, kernel.iIndepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure, + kernel.const_apply] +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_sets_singleton_iff ProbabilityTheory.iIndepSets_singleton_iff + +variable [IsProbabilityMeasure μ] + +theorem iIndepSet_iff_iIndepSets_singleton {f : ι → Set Ω} (hf : ∀ i, MeasurableSet (f i)) : + iIndepSet f μ ↔ iIndepSets (fun i ↦ {f i}) μ := + kernel.iIndepSet_iff_iIndepSets_singleton hf +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_set_iff_Indep_sets_singleton ProbabilityTheory.iIndepSet_iff_iIndepSets_singleton + +theorem iIndepSet_iff_meas_biInter {f : ι → Set Ω} (hf : ∀ i, MeasurableSet (f i)) : + iIndepSet f μ ↔ ∀ s, μ (⋂ i ∈ s, f i) = ∏ i in s, μ (f i) := by + simp_rw [iIndepSet, kernel.iIndepSet_iff_meas_biInter hf, ae_dirac_eq, Filter.eventually_pure, + kernel.const_apply] +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_set_iff_measure_Inter_eq_prod ProbabilityTheory.iIndepSet_iff_meas_biInter + +theorem iIndepSets.iIndepSet_of_mem {π : ι → Set (Set Ω)} {f : ι → Set Ω} + (hfπ : ∀ i, f i ∈ π i) (hf : ∀ i, MeasurableSet (f i)) + (hπ : iIndepSets π μ) : iIndepSet f μ := + kernel.iIndepSets.iIndepSet_of_mem hfπ hf hπ +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_sets.Indep_set_of_mem ProbabilityTheory.iIndepSets.iIndepSet_of_mem + end IndepSet section IndepFun diff --git a/Mathlib/Probability/Independence/Kernel.lean b/Mathlib/Probability/Independence/Kernel.lean index d3131e24bd68a..9ce35e757abe2 100644 --- a/Mathlib/Probability/Independence/Kernel.lean +++ b/Mathlib/Probability/Independence/Kernel.lean @@ -114,6 +114,50 @@ def IndepFun {β γ} {_mΩ : MeasurableSpace Ω} [mβ : MeasurableSpace β] [mγ end Definitions +section ByDefinition + +variable {β : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)} + {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} + {κ : kernel α Ω} {μ : Measure α} + {π : ι → Set (Set Ω)} {s : ι → Set Ω} {S : Finset ι} {f : ∀ x : ι, Ω → β x} + +lemma iIndepSets.meas_biInter (h : iIndepSets π κ μ) (s : Finset ι) + {f : ι → Set Ω} (hf : ∀ i, i ∈ s → f i ∈ π i) : + ∀ᵐ a ∂μ, κ a (⋂ i ∈ s, f i) = ∏ i in s, κ a (f i) := h s hf + +lemma iIndepSets.meas_iInter [Fintype ι] (h : iIndepSets π κ μ) (hs : ∀ i, s i ∈ π i) : + ∀ᵐ a ∂μ, κ a (⋂ i, s i) = ∏ i, κ a (s i) := by + filter_upwards [h.meas_biInter Finset.univ (fun _i _ ↦ hs _)] with a ha using by simp [← ha] + +lemma iIndep.iIndepSets' (hμ : iIndep m κ μ) : + iIndepSets (fun x ↦ {s | MeasurableSet[m x] s}) κ μ := hμ + +lemma iIndep.meas_biInter (hμ : iIndep m κ μ) (hs : ∀ i, i ∈ S → MeasurableSet[m i] (s i)) : + ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, s i) = ∏ i in S, κ a (s i) := hμ _ hs + +lemma iIndep.meas_iInter [Fintype ι] (h : iIndep m κ μ) (hs : ∀ i, MeasurableSet[m i] (s i)) : + ∀ᵐ a ∂μ, κ a (⋂ i, s i) = ∏ i, κ a (s i) := by + filter_upwards [h.meas_biInter (fun i (_ : i ∈ Finset.univ) ↦ hs _)] with a ha + simp [← ha] + +protected lemma iIndepFun.iIndep (hf : iIndepFun mβ f κ μ) : + iIndep (fun x ↦ (mβ x).comap (f x)) κ μ := hf + +lemma iIndepFun.meas_biInter (hf : iIndepFun mβ f κ μ) + (hs : ∀ i, i ∈ S → MeasurableSet[(mβ i).comap (f i)] (s i)) : + ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, s i) = ∏ i in S, κ a (s i) := hf.iIndep.meas_biInter hs + +lemma iIndepFun.meas_iInter [Fintype ι] (hf : iIndepFun mβ f κ μ) + (hs : ∀ i, MeasurableSet[(mβ i).comap (f i)] (s i)) : + ∀ᵐ a ∂μ, κ a (⋂ i, s i) = ∏ i, κ a (s i) := hf.iIndep.meas_iInter hs + +lemma IndepFun.meas_inter {β γ : Type*} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] + {f : Ω → β} {g : Ω → γ} (hfg : IndepFun f g κ μ) + {s t : Set Ω} (hs : MeasurableSet[mβ.comap f] s) (ht : MeasurableSet[mγ.comap g] t) : + ∀ᵐ a ∂μ, κ a (s ∩ t) = κ a s * κ a t := hfg _ _ hs ht + +end ByDefinition + section Indep variable {_mα : MeasurableSpace α} @@ -228,6 +272,20 @@ theorem IndepSets.bInter {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : M rcases h with ⟨n, hn, h⟩ exact h t1 t2 (Set.biInter_subset_of_mem hn ht1) ht2 +theorem iIndep_comap_mem_iff {f : ι → Set Ω} {_mΩ : MeasurableSpace Ω} + {κ : kernel α Ω} {μ : Measure α} : + iIndep (fun i => MeasurableSpace.comap (· ∈ f i) ⊤) κ μ ↔ iIndepSet f κ μ := by + simp_rw [← generateFrom_singleton]; rfl + +theorem iIndepSets_singleton_iff {s : ι → Set Ω} {_mΩ : MeasurableSpace Ω} + {κ : kernel α Ω} {μ : Measure α} : + iIndepSets (fun i ↦ {s i}) κ μ ↔ + ∀ S : Finset ι, ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, s i) = ∏ i in S, κ a (s i) := by + refine ⟨fun h S ↦ h S (fun i _ ↦ rfl), fun h S f hf ↦ ?_⟩ + filter_upwards [h S] with a ha + have : ∀ i ∈ S, κ a (f i) = κ a (s i) := fun i hi ↦ by rw [hf i hi] + rwa [Finset.prod_congr rfl this, Set.iInter₂_congr hf] + theorem indepSets_singleton_iff {s t : Set Ω} {_mΩ : MeasurableSpace Ω} {κ : kernel α Ω} {μ : Measure α} : IndepSets {s} {t} κ μ ↔ ∀ᵐ a ∂μ, κ a (s ∩ t) = κ a s * κ a t := @@ -597,8 +655,29 @@ We prove the following equivalences on `IndepSet`, for measurable sets `s, t`. * `IndepSet s t κ μ ↔ IndepSets {s} {t} κ μ`. -/ +variable {_mα : MeasurableSpace α} -variable {s t : Set Ω} (S T : Set (Set Ω)) {_mα : MeasurableSpace α} +theorem iIndepSet_iff_iIndepSets_singleton {_mΩ : MeasurableSpace Ω} {κ : kernel α Ω} + [IsMarkovKernel κ] {μ : Measure α} {f : ι → Set Ω} + (hf : ∀ i, MeasurableSet (f i)) : + iIndepSet f κ μ ↔ iIndepSets (fun i ↦ {f i}) κ μ := + ⟨iIndep.iIndepSets fun _ ↦ rfl, + iIndepSets.iIndep _ (fun i ↦ generateFrom_le <| by rintro t (rfl : t = _); exact hf _) _ + (fun _ ↦ IsPiSystem.singleton _) fun _ ↦ rfl⟩ + +theorem iIndepSet_iff_meas_biInter {_mΩ : MeasurableSpace Ω} {κ : kernel α Ω} + [IsMarkovKernel κ] {μ : Measure α} {f : ι → Set Ω} (hf : ∀ i, MeasurableSet (f i)) : + iIndepSet f κ μ ↔ ∀ s, ∀ᵐ a ∂μ, κ a (⋂ i ∈ s, f i) = ∏ i in s, κ a (f i) := + (iIndepSet_iff_iIndepSets_singleton hf).trans iIndepSets_singleton_iff + +theorem iIndepSets.iIndepSet_of_mem {_mΩ : MeasurableSpace Ω} {κ : kernel α Ω} + [IsMarkovKernel κ] {μ : Measure α} {π : ι → Set (Set Ω)} {f : ι → Set Ω} + (hfπ : ∀ i, f i ∈ π i) (hf : ∀ i, MeasurableSet (f i)) + (hπ : iIndepSets π κ μ) : + iIndepSet f κ μ := + (iIndepSet_iff_meas_biInter hf).2 fun _t ↦ hπ.meas_biInter _ fun _i _ ↦ hfπ _ + +variable {s t : Set Ω} (S T : Set (Set Ω)) theorem indepSet_iff_indepSets_singleton {m0 : MeasurableSpace Ω} (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (κ : kernel α Ω) (μ : Measure α)