relaxing independence

StatsMLlib/Probability/Independence/Grouping.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Kei Tsukamoto. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kei Tsukamoto
+-/
+import Mathlib.Probability.Independence.Basic
+
+/-!
+# Grouping an independent family into blocks
+
+A family of random variables indexed by a product `ι × κ` can be curried into an `ι`-indexed family
+of `κ`-indexed blocks, each block taking values in `κ → β` with the product σ-algebra. This file
+shows that independence is preserved by this regrouping.
+
+The proof goes through π-systems: the σ-algebra generated by the `i`-th block is generated by the
+finite intersections of preimages `f (i, j) ⁻¹' B`, and independence of those finite intersections
+follows from the independence of the original family.
+
+## Main results
+
+* `ProbabilityTheory.iIndepFun_curry`: if `f : ι × κ → Ω → β` is an independent family, then so is
+  the curried family `fun i ω j => f (i, j) ω` of blocks.
+-/
+
+open MeasureTheory MeasurableSpace Set
+
+namespace ProbabilityTheory
+
+variable {Ω ι κ β : Type*} [MeasurableSpace Ω] [MeasurableSpace β]
+  {f : ι × κ → Ω → β} {μ : Measure Ω}
+
+/-- Independence of a family indexed by a product implies independence of the curried family of
+blocks, each block taking values in `κ → β` with the product σ-algebra. -/
+theorem iIndepFun_curry [IsProbabilityMeasure μ] (hf : ∀ p, Measurable (f p))
+    (h : iIndepFun f μ) :
+    iIndepFun (fun (i : ι) (ω : Ω) (j : κ) => f (i, j) ω) μ := by
+  classical
+  rw [iIndepFun_iff_iIndep]
+  refine iIndepSets.iIndep ?_
+    (fun i => piiUnionInter
+      (fun p => {s | MeasurableSet[MeasurableSpace.comap (f p) inferInstance] s})
+      (Set.range fun j : κ => (i, j))) ?_ ?_ ?_
+  · exact fun i => (Measurable.of_eval fun j => hf (i, j)).comap_le
+  · exact fun _ => isPiSystem_piiUnionInter _
+      (fun p => @isPiSystem_measurableSet Ω (MeasurableSpace.comap (f p) inferInstance)) _
+  · intro i
+    rw [generateFrom_piiUnionInter_measurableSet
+      (fun p : ι × κ => MeasurableSpace.comap (f p) inferInstance)
+      (Set.range fun j : κ => (i, j)), iSup_range]
+    exact MeasurableSpace.comap_process_pi fun (j : κ) (ω : Ω) => f (i, j) ω
+  · rw [iIndepSets_iff]
+    intro s F hF
+    have hF' : ∀ i : ι, ∃ (t : Finset (ι × κ)) (_ : ↑t ⊆ Set.range fun j : κ => (i, j))
+        (G : ι × κ → Set Ω)
+        (_ : ∀ p ∈ t, MeasurableSet[MeasurableSpace.comap (f p) inferInstance] (G p)),
+        i ∈ s → F i = ⋂ p ∈ t, G p := by
+      intro i
+      by_cases hi : i ∈ s
+      · obtain ⟨t, hts, G, hG, hEq⟩ := hF i hi
+        exact ⟨t, hts, G, hG, fun _ => hEq⟩
+      · exact ⟨∅, by simp, fun _ => Set.univ, by simp, fun hi' => absurd hi' hi⟩
+    choose t hts G hG hFeq using hF'
+    have hfst : ∀ (i : ι) (p : ι × κ), p ∈ t i → p.1 = i := by
+      intro i p hp
+      obtain ⟨j, hj⟩ := hts i (Finset.mem_coe.mpr hp)
+      rw [← hj]
+    have hFi : ∀ i ∈ s, F i = ⋂ p ∈ t i, G p.1 p := by
+      intro i hi
+      rw [hFeq i hi]
+      exact Set.iInter₂_congr fun p hp => by rw [hfst i p hp]
+    have hblock : ∀ i ∈ s, μ (⋂ p ∈ t i, G p.1 p) = ∏ p ∈ t i, μ (G p.1 p) :=
+      fun i _ => h.meas_biInter fun p hp => by rw [hfst i p hp]; exact hG i p hp
+    have hdisj : (↑s : Set ι).PairwiseDisjoint t := by
+      intro a _ b _ hab
+      simp only [Function.onFun, Finset.disjoint_left]
+      intro p hpa hpb
+      exact hab ((hfst a p hpa).symm.trans (hfst b p hpb))
+    have hGmem : ∀ p ∈ s.biUnion t,
+        MeasurableSet[MeasurableSpace.comap (f p) inferInstance] (G p.1 p) := by
+      intro p hp
+      rw [Finset.mem_biUnion] at hp
+      obtain ⟨i, _, hpi⟩ := hp
+      rw [hfst i p hpi]
+      exact hG i p hpi
+    calc μ (⋂ i ∈ s, F i)
+        = μ (⋂ p ∈ s.biUnion t, G p.1 p) := by
+          rw [Finset.set_biInter_biUnion]
+          exact congrArg μ (Set.iInter₂_congr hFi)
+      _ = ∏ p ∈ s.biUnion t, μ (G p.1 p) := h.meas_biInter hGmem
+      _ = ∏ i ∈ s, ∏ p ∈ t i, μ (G p.1 p) := Finset.prod_biUnion hdisj
+      _ = ∏ i ∈ s, μ (F i) := by
+          refine Finset.prod_congr rfl fun i hi => ?_
+          rw [hFi i hi, hblock i hi]
+
+end ProbabilityTheory