Mathlib.Probability.Independence

theorem condIndepFun_pi_cond_residual_of_disjoint {ι : Type*} [Finite ι] {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] [∀ i, StandardBorelSpace (Ω i)] (μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] {S0 T0 U : Finset ι} (hS0T0 : Disjoint S0 T0) (hS0U : Disjoint S0 U) : letI : Fintype ι := Fintype.ofFinite ι CondIndepFun (comap (finsetCoordProj (Ω := Ω) U) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) U)) (fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) S0 x)) (fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) T0 x)) (Measure.pi μ) := by classical letI : Fintype ι := Fintype.ofFinite ι have hS0T0U : Disjoint S0 (T0 ∪ U) := by rw [Finset.disjoint_left] intro i hiS0 hiT0U rcases Finset.mem_union.mp hiT0U with hiT0 | hiU · exact (Finset.disjoint_left.mp hS0T0) hiS0 hiT0 · exact (Finset.disjoint_left.mp hS0U) hiS0 hiU have hindep : IndepFun (finsetCoordProj (Ω := Ω) S0) (finsetCoordProj (Ω := Ω) (T0 ∪ U)) (Measure.pi μ) := indepFun_pi_of_disjoint (Ω := Ω) μ hS0T0U have hindep_pair : IndepFun (finsetCoordProj (Ω := Ω) S0) (fun x => (finsetCoordProj (Ω := Ω) T0 x, finsetCoordProj (Ω := Ω) U x)) (Measure.pi μ) := by simpa [finsetCoordProjPairFromUnion_comp] using hindep.comp measurable_id (measurable_finsetCoordProjPairFromUnion (Ω := Ω) T0 U) have hbot : CondIndepFun ⊥ bot_le (finsetCoordProj (Ω := Ω) S0) (fun x => (finsetCoordProj (Ω := Ω) T0 x, finsetCoordProj (Ω := Ω) U x)) (Measure.pi μ) := condIndepFun_bot_of_indepFun (measurable_finsetCoordProj (Ω := Ω) S0) ((measurable_finsetCoordProj (Ω := Ω) T0).prod (measurable_finsetCoordProj (Ω := Ω) U)) hindep_pair have hbase : CondIndepFun (comap (finsetCoordProj (Ω := Ω) U) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) U)) (finsetCoordProj (Ω := Ω) S0) (finsetCoordProj (Ω := Ω) T0) (Measure.pi μ) := by simpa [sup_bot_eq] using (condIndepFun_weak_union_of_prodMk (Ω := (i : ι) → Ω i) (m := ⊥) (mΩ := inferInstance) (μ := Measure.pi μ) bot_le (W := finsetCoordProj (Ω := Ω) S0) (V := finsetCoordProj (Ω := Ω) T0) (A := finsetCoordProj (Ω := Ω) U) (measurable_finsetCoordProj (Ω := Ω) S0) (measurable_finsetCoordProj (Ω := Ω) T0) (measurable_finsetCoordProj (Ω := Ω) U) hbot) have hleft : CondIndepFun (comap (finsetCoordProj (Ω := Ω) U) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) U)) (fun x => (finsetCoordProj (Ω := Ω) S0 x, finsetCoordProj (Ω := Ω) U x)) (finsetCoordProj (Ω := Ω) T0) (Measure.pi μ) := condIndepFun_prodMk_of_measurable_left (m := comap (finsetCoordProj (Ω := Ω) U) inferInstance) (mΩ := inferInstance) (μ := Measure.pi μ) (comap_le (measurable_finsetCoordProj (Ω := Ω) U)) (measurable_finsetCoordProj (Ω := Ω) S0) (measurable_finsetCoordProj (Ω := Ω) T0) (comap_measurable (finsetCoordProj (Ω := Ω) U)) hbase have hright : CondIndepFun (comap (finsetCoordProj (Ω := Ω) U) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) U)) (fun x => (finsetCoordProj (Ω := Ω) T0 x, finsetCoordProj (Ω := Ω) U x)) (fun x => (finsetCoordProj (Ω := Ω) S0 x, finsetCoordProj (Ω := Ω) U x)) (Measure.pi μ) := condIndepFun_prodMk_of_measurable_left (m := comap (finsetCoordProj (Ω := Ω) U) inferInstance) (mΩ := inferInstance) (μ := Measure.pi μ) (comap_le (measurable_finsetCoordProj (Ω := Ω) U)) (measurable_finsetCoordProj (Ω := Ω) T0) ((measurable_finsetCoordProj (Ω := Ω) S0).prod (measurable_finsetCoordProj (Ω := Ω) U)) (comap_measurable (finsetCoordProj (Ω := Ω) U)) hleft.symm have hswapS : Measurable (fun p : (((i : {i // i ∈ S0}) → Ω i.val) × ((i : {i // i ∈ U}) → Ω i.val)) => (p.2, p.1)) := measurable_snd.prod measurable_fst have hswapT : Measurable (fun p : (((i : {i // i ∈ T0}) → Ω i.val) × ((i : {i // i ∈ U}) → Ω i.val)) => (p.2, p.1)) := measurable_snd.prod measurable_fst exact hright.symm.comp hswapS hswapT

theorem condIndepFun_pi_of_inter_subset {ι : Type*} [DecidableEq ι] [Finite ι] {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] [∀ i, StandardBorelSpace (Ω i)] (μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] {S T U : Finset ι} (hSTU : S ∩ T ⊆ U) : letI : Fintype ι := Fintype.ofFinite ι CondIndepFun (comap (finsetCoordProj (Ω := Ω) U) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) U)) (finsetCoordProj (Ω := Ω) S) (finsetCoordProj (Ω := Ω) T) (Measure.pi μ) := by classical letI : Fintype ι := Fintype.ofFinite ι let S0 : Finset ι := S \ U let T0 : Finset ι := T \ U have hS0T0 : Disjoint S0 T0 := by rw [Finset.disjoint_left] intro i hiS0 hiT0 change i ∈ S \ U at hiS0 change i ∈ T \ U at hiT0 rw [mem_sdiff] at hiS0 rw [mem_sdiff] at hiT0 exact hiT0.2 (hSTU (Finset.mem_inter.mpr ⟨hiS0.1, hiT0.1⟩)) have hS0U : Disjoint S0 U := by rw [Finset.disjoint_left] intro i hiS0 hiU change i ∈ S \ U at hiS0 rw [mem_sdiff] at hiS0 exact hiS0.2 hiU have hT0U : Disjoint T0 U := by rw [Finset.disjoint_left] intro i hiT0 hiU change i ∈ T \ U at hiT0 rw [mem_sdiff] at hiT0 exact hiT0.2 hiU have hbase : CondIndepFun (comap (finsetCoordProj (Ω := Ω) U) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) U)) (fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) S0 x)) (fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) T0 x)) (Measure.pi μ) := condIndepFun_pi_cond_residual_of_disjoint (Ω := Ω) μ hS0T0 hS0U have h := hbase.comp (measurable_finsetCoordProjFromCondResidual (Ω := Ω) S U) (measurable_finsetCoordProjFromCondResidual (Ω := Ω) T U) simpa [S0, T0, finsetCoordProjFromCondResidual_comp] using h

theorem IndepFun.integral_restrict_preimage_eq_mul {Ω α β : Type*} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : Measure Ω} {f : Ω → α} {g : Ω → β} (hfg : IndepFun f g μ) (hf_ae : AEMeasurable f μ) (hg : AEMeasurable g μ) {E : Set α} (hE : MeasurableSet E) (hpre : MeasurableSet (f ⁻¹' E)) {h : β → ℝ} (hh : AEStronglyMeasurable h (μ.map g)) : ∫ ω in f ⁻¹' E, h (g ω) ∂μ = (μ (f ⁻¹' E)).toReal * ∫ ω, h (g ω) ∂μ := by classical -- `φ : α → ℝ` is the indicator of `E` as a plain function. set φ : α → ℝ := fun a => if a ∈ E then (1 : ℝ) else 0 with hφ_def have hφ_meas : Measurable φ := Measurable.ite hE measurable_const measurable_const -- Pointwise: `φ (f ω) = (f ⁻¹' E).indicator 1 ω`. have hφ_indicator : ∀ ω, φ (f ω) = (f ⁻¹' E).indicator (fun _ => (1 : ℝ)) ω := by intro ω by_cases hω : ω ∈ f ⁻¹' E · have hfE : f ω ∈ E := hω simp [hφ_def, hfE] · have hfE : f ω ∉ E := hω simp [hφ_def, hfE] -- Rewrite `∫ in f ⁻¹' E, ...` as `∫ φ(f) * h(g) dμ`. have heq_int : ∫ ω in f ⁻¹' E, h (g ω) ∂μ = ∫ ω, φ (f ω) * h (g ω) ∂μ := by rw [← MeasureTheory.integral_indicator hpre] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω by_cases hω : ω ∈ f ⁻¹' E · have hfE : f ω ∈ E := hω simp [hφ_def, hfE] · have hfE : f ω ∉ E := hω simp [hφ_def, hfE] -- Apply independence to factor the product integral. have hfAE : AEMeasurable f μ := hf_ae have hgAE : AEMeasurable g μ := hg have hφAEStr : AEStronglyMeasurable φ (μ.map f) := hφ_meas.aestronglyMeasurable have hmul : ∫ ω, φ (f ω) * h (g ω) ∂μ = (∫ ω, φ (f ω) ∂μ) * ∫ ω, h (g ω) ∂μ := hfg.integral_fun_comp_mul_comp hfAE hgAE hφAEStr hh -- `∫ φ(f) dμ = μ(f ⁻¹' E).toReal`. have hφint : ∫ ω, φ (f ω) ∂μ = (μ (f ⁻¹' E)).toReal := by rw [MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall hφ_indicator)] rw [MeasureTheory.integral_indicator_const (1 : ℝ) hpre] simp [MeasureTheory.measureReal_def] rw [heq_int, hmul, hφint]

theorem iIndepFun_pair_prod (mX : ∀ j, Measurable (X j)) (mY : ∀ j, Measurable (Y j)) (hX : iIndepFun X μ) (hY : iIndepFun Y ν) : iIndepFun (fun j p => (X j p.1, Y j p.2)) (μ.prod ν) := by let FX : Ω → J → A := fun ω j => X j ω let FY : Ω' → J → B := fun ω j => Y j ω have mFX : Measurable FX := measurable_pi_iff.mpr mX have mFY : Measurable FY := measurable_pi_iff.mpr mY have mPair : ∀ j, Measurable (fun p : Ω × Ω' => (X j p.1, Y j p.2)) := by intro j exact (mX j).comp measurable_fst |>.prodMk ((mY j).comp measurable_snd) have hXm : μ.map FX = infinitePi (fun j => μ.map (X j)) := (iIndepFun_iff_map_fun_eq_infinitePi_map mX).mp hX have hYm : ν.map FY = infinitePi (fun j => ν.map (Y j)) := (iIndepFun_iff_map_fun_eq_infinitePi_map mY).mp hY have hcoord (j : J) : (μ.prod ν).map (fun p : Ω × Ω' => (X j p.1, Y j p.2)) = (μ.map (X j)).prod (ν.map (Y j)) := by calc _ = (μ.prod ν).map (map (X j) (Y j)) := by congr 1 _ = _ := (Measure.map_prod_map μ ν (mX j) (mY j)).symm letI : ∀ j, IsProbabilityMeasure (μ.map (X j)) := fun j => Measure.isProbabilityMeasure_map (mX j).aemeasurable letI : ∀ j, IsProbabilityMeasure (ν.map (Y j)) := fun j => Measure.isProbabilityMeasure_map (mY j).aemeasurable apply (iIndepFun_iff_map_fun_eq_infinitePi_map mPair).mpr calc (μ.prod ν).map (fun p : Ω × Ω' => fun j => (X j p.1, Y j p.2)) = Measure.map (fun q : (J → A) × (J → B) => fun j => (q.1 j, q.2 j)) ((μ.map FX).prod (ν.map FY)) := by rw [Measure.map_prod_map μ ν mFX mFY, Measure.map_map (by fun_prop) (by fun_prop)] rfl _ = Measure.map (fun q : (J → A) × (J → B) => fun j => (q.1 j, q.2 j)) ((infinitePi (fun j => μ.map (X j))).prod (infinitePi (fun j => ν.map (Y j)))) := by rw [hXm, hYm] _ = infinitePi (fun j => (μ.map (X j)).prod (ν.map (Y j))) := map_pair_infinitePi_prod _ _ _ = infinitePi (fun j => (μ.prod ν).map (fun p : Ω × Ω' => (X j p.1, Y j p.2))) := by simp_rw [hcoord]