feat: Independence of singletons (#7251)

Port a bit of leanprover-community/mathlib#18506, but it's mostly handmade.




Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

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,13 +215,25 @@ 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 Ω}
       (_H : ∀ i, i ∈ s → MeasurableSet[(m i).comap (f i)] (f' i)),
       μ (⋂ 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

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 α)