feat(Probability/Independence): reindexing lemmas for iIndep* (#31309)

Author: gasparattila

Mathlib/Probability/Independence/Basic.lean

@@ -155,7 +155,7 @@ scoped[ProbabilityTheory] notation3 X:50 " ⟂ᵢ " Y:50 => ProbabilityTheory.In
 
 section Definition_lemmas
 variable {π : ι → Set (Set Ω)} {m : ι → MeasurableSpace Ω} {_ : MeasurableSpace Ω} {μ : Measure Ω}
-  {S : Finset ι} {s : ι → Set Ω}
+  {S : Finset ι} {s : ι → Set Ω} {ι' : Type*} {g : ι' → ι}
 
 lemma iIndepSets_iff (π : ι → Set (Set Ω)) (μ : Measure Ω) :
     iIndepSets π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → f i ∈ π i),
@@ -283,6 +283,56 @@ lemma IndepFun.meas_inter [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ]
     μ (s ∩ t) = μ s * μ t :=
   (IndepFun_iff _ _ _).1 hfg _ _ hs ht
 
+lemma iIndepSets.precomp (hg : Function.Injective g) (h : iIndepSets π μ) :
+    iIndepSets (π ∘ g) μ :=
+  Kernel.iIndepSets.precomp hg h
+
+lemma iIndepSets.of_precomp (hg : Function.Surjective g) (h : iIndepSets (π ∘ g) μ) :
+    iIndepSets π μ :=
+  Kernel.iIndepSets.of_precomp hg h
+
+lemma iIndepSets_precomp_of_bijective (hg : Function.Bijective g) :
+    iIndepSets (π ∘ g) μ ↔ iIndepSets π μ :=
+  Kernel.iIndepSets_precomp_of_bijective hg
+
+lemma iIndep.precomp (hg : Function.Injective g) (h : iIndep m μ) :
+    iIndep (m ∘ g) μ :=
+  Kernel.iIndep.precomp hg h
+
+lemma iIndep.of_precomp (hg : Function.Surjective g) (h : iIndep (m ∘ g) μ) :
+    iIndep m μ :=
+  Kernel.iIndep.of_precomp hg h
+
+lemma iIndep_precomp_of_bijective (hg : Function.Bijective g) :
+    iIndep (m ∘ g) μ ↔ iIndep m μ :=
+  Kernel.iIndep_precomp_of_bijective hg
+
+lemma iIndepSet.precomp (hg : Function.Injective g) (h : iIndepSet s μ) :
+    iIndepSet (s ∘ g) μ :=
+  Kernel.iIndepSet.precomp hg h
+
+lemma iIndepSet.of_precomp (hg : Function.Surjective g) (h : iIndepSet (s ∘ g) μ) :
+    iIndepSet s μ :=
+  Kernel.iIndepSet.of_precomp hg h
+
+lemma iIndepSet_precomp_of_bijective (hg : Function.Bijective g) :
+    iIndepSet (s ∘ g) μ ↔ iIndepSet s μ :=
+  Kernel.iIndepSet_precomp_of_bijective hg
+
+variable {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i}
+
+lemma iIndepFun.precomp (hg : g.Injective) (h : iIndepFun f μ) :
+    iIndepFun (m := fun i ↦ m (g i)) (fun i ↦ f (g i)) μ :=
+  Kernel.iIndepFun.precomp hg h
+
+lemma iIndepFun.of_precomp (hg : g.Surjective)
+    (h : iIndepFun (m := fun i ↦ m (g i)) (fun i ↦ f (g i)) μ) : iIndepFun f μ :=
+  Kernel.iIndepFun.of_precomp hg h
+
+lemma iIndepFun_precomp_of_bijective (hg : g.Bijective) :
+    iIndepFun (m := fun i ↦ m (g i)) (fun i ↦ f (g i)) μ ↔ iIndepFun f μ :=
+  Kernel.iIndepFun_precomp_of_bijective hg
+
 end Definition_lemmas
 
 section Indep
@@ -818,18 +868,6 @@ lemma iIndepFun.indepFun_prodMk_prodMk₀ (h_indep : iIndepFun f μ) (hf : ∀ i
     IndepFun (fun a ↦ (f i a, f j a)) (fun a ↦ (f k a, f l a)) μ :=
   Kernel.iIndepFun.indepFun_prodMk_prodMk₀ h_indep (by simp [hf]) i j k l hik hil hjk hjl
 
-variable {ι' : Type*} {α : ι → Type*} [∀ i, MeasurableSpace (α i)]
-
-open Function in
-lemma iIndepFun.precomp {g : ι' → ι} (hg : g.Injective) (h : iIndepFun f μ) :
-    iIndepFun (m := fun i ↦ m (g i)) (fun i ↦ f (g i)) μ := by
-  have : IsProbabilityMeasure μ := h.isProbabilityMeasure
-  nontriviality ι'
-  have A (x) : Function.invFun g (g x) = x := Function.leftInverse_invFun hg x
-  rw [iIndepFun_iff] at h ⊢
-  intro t s' hs'
-  simpa [A] using h (t.map ⟨g, hg⟩) (f' := fun i ↦ s' (invFun g i)) (by simpa [A] using hs')
-
 lemma iIndepFun_iff_finset : iIndepFun f μ ↔ ∀ s : Finset ι, iIndepFun (s.restrict f) μ where
   mp h s := h.precomp (g := ((↑) : s → ι)) Subtype.val_injective
   mpr h := by
@@ -839,30 +877,6 @@ lemma iIndepFun_iff_finset : iIndepFun f μ ↔ ∀ s : Finset ι, iIndepFun (s.
     rw [← Finset.prod_coe_sort, this]
     exact (h s).meas_iInter fun i ↦ hs i i.2
 
-lemma iIndepFun.of_precomp {g : ι' → ι} (hg : g.Surjective)
-    (h : iIndepFun (m := fun i ↦ m (g i)) (fun i ↦ f (g i)) μ) : iIndepFun f μ := by
-  have : IsProbabilityMeasure μ := h.isProbabilityMeasure
-  nontriviality ι
-  have := hg.nontrivial
-  classical
-  rw [iIndepFun_iff] at h ⊢
-  intro t s hs
-  have A (x) : g (Function.invFun g x) = x := Function.rightInverse_invFun hg x
-  have : ∀ i ∈ Finset.image (Function.invFun g) t,
-    @MeasurableSet _ (MeasurableSpace.comap (f <| g i) (m <| g i)) (s <| g i) := by
-    intro i hi
-    obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hi
-    simpa [A] using (A j).symm ▸ hs j hj
-  have eq : ∏ i ∈ Finset.image (Function.invFun g) t, μ (s (g i)) = ∏ i ∈ t, μ (s i) := by
-    rw [Finset.prod_image (fun x hx y hy h => ?_), Finset.prod_congr rfl (fun x _ => by rw [A])]
-    rw [← A x, ← A y, h]
-  simpa [A, eq] using h (t.image (Function.invFun g)) (f' := fun i ↦ s (g i)) this
-
-lemma iIndepFun_precomp_of_bijective {g : ι' → ι} (hg : g.Bijective) :
-    iIndepFun (m := fun i ↦ m (g i)) (fun i ↦ f (g i)) μ ↔ iIndepFun f μ where
-  mp := .of_precomp hg.surjective
-  mpr := .precomp hg.injective
-
 end iIndepFun
 
 section Mul

Mathlib/Probability/Independence/Kernel.lean

@@ -127,7 +127,7 @@ variable {β : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)}
   {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω}
   {κ η : Kernel α Ω} {μ : Measure α}
   {π : ι → Set (Set Ω)} {s : ι → Set Ω} {S : Finset ι} {f : ∀ x : ι, Ω → β x}
-  {s1 s2 : Set (Set Ω)}
+  {s1 s2 : Set (Set Ω)} {ι' : Type*} {g : ι' → ι}
 
 @[simp] lemma iIndepSets_zero_right : iIndepSets π κ 0 := by simp [iIndepSets]
 
@@ -273,6 +273,64 @@ lemma IndepFun.meas_inter {β γ : Type*} [mβ : MeasurableSpace β] [mγ : Meas
     {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
 
+lemma iIndepSets.precomp (hg : Function.Injective g) (h : iIndepSets π κ μ) :
+    iIndepSets (π ∘ g) κ μ := by
+  intro s f hf
+  let f' := Function.extend g f fun _ => ∅
+  have f'_apply x : f' (g x) = f x := hg.extend_apply ..
+  classical
+  have hf' : ∀ i ∈ s.image g, f' i ∈ π i := by
+    simp_rw [Finset.forall_mem_image, f'_apply]
+    exact hf
+  filter_upwards [@h (s.image g) f' hf'] with a ha
+  simpa [Finset.set_biInter_finset_image, Finset.prod_image hg.injOn, f'_apply] using ha
+
+lemma iIndepSets.of_precomp (hg : Function.Surjective g) (h : iIndepSets (π ∘ g) κ μ) :
+    iIndepSets π κ μ := by
+  obtain ⟨g', hg'⟩ := hg.hasRightInverse
+  convert h.precomp hg'.injective
+  rw [Function.comp_assoc, hg'.comp_eq_id, Function.comp_id]
+
+lemma iIndepSets_precomp_of_bijective (hg : Function.Bijective g) :
+    iIndepSets (π ∘ g) κ μ ↔ iIndepSets π κ μ :=
+  ⟨.of_precomp hg.surjective, .precomp hg.injective⟩
+
+lemma iIndep.precomp (hg : Function.Injective g) (h : iIndep m κ μ) :
+    iIndep (m ∘ g) κ μ :=
+  (iIndepSets.precomp hg h :)
+
+lemma iIndep.of_precomp (hg : Function.Surjective g) (h : iIndep (m ∘ g) κ μ) :
+    iIndep m κ μ :=
+  iIndepSets.of_precomp hg h
+
+lemma iIndep_precomp_of_bijective (hg : Function.Bijective g) :
+    iIndep (m ∘ g) κ μ ↔ iIndep m κ μ :=
+  ⟨.of_precomp hg.surjective, .precomp hg.injective⟩
+
+lemma iIndepSet.precomp (hg : Function.Injective g) (h : iIndepSet s κ μ) :
+    iIndepSet (s ∘ g) κ μ :=
+  iIndep.precomp hg h
+
+lemma iIndepSet.of_precomp (hg : Function.Surjective g) (h : iIndepSet (s ∘ g) κ μ) :
+    iIndepSet s κ μ :=
+  iIndep.of_precomp hg h
+
+lemma iIndepSet_precomp_of_bijective (hg : Function.Bijective g) :
+    iIndepSet (s ∘ g) κ μ ↔ iIndepSet s κ μ :=
+  ⟨.of_precomp hg.surjective, .precomp hg.injective⟩
+
+lemma iIndepFun.precomp (hg : Function.Injective g) (h : iIndepFun f κ μ) :
+    iIndepFun (fun i ↦ f (g i)) κ μ :=
+  iIndep.precomp hg h
+
+lemma iIndepFun.of_precomp (hg : Function.Surjective g) (h : iIndepFun (fun i ↦ f (g i)) κ μ) :
+    iIndepFun f κ μ :=
+  iIndep.of_precomp hg h
+
+lemma iIndepFun_precomp_of_bijective (hg : Function.Bijective g) :
+    iIndepFun (fun i ↦ f (g i)) κ μ ↔ iIndepFun f κ μ :=
+  ⟨.of_precomp hg.surjective, .precomp hg.injective⟩
+
 end ByDefinition
 
 section Indep
@@ -1482,3 +1540,5 @@ lemma iIndepFun.cond_iInter [Finite ι] (hY : ∀ i, Measurable (Y i))
 -- for kernels
 
 end ProbabilityTheory.Kernel
+
+set_option linter.style.longFile 1700