feat: independence of functions under conditioning (#17915)

From PFR

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -623,7 +623,7 @@ theorem tendsto_factorial_div_pow_self_atTop :
       refine (eventually_gt_atTop 0).mono fun n hn ↦ ?_
       rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩
       rw [← prod_range_add_one_eq_factorial, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
-        prod_natCast, Nat.cast_succ, ← prod_inv_distrib, ← prod_mul_distrib,
+        prod_natCast, Nat.cast_succ, ← Finset.prod_inv_distrib, ← prod_mul_distrib,
         Finset.prod_range_succ']
       simp only [prod_range_succ', one_mul, Nat.cast_add, zero_add, Nat.cast_one]
       refine

Mathlib/Data/ENNReal/Inv.lean

@@ -173,6 +173,16 @@ protected theorem inv_div {a b : ℝ≥0∞} (htop : b ≠ ∞ ∨ a ≠ ∞) (h
   rw [← ENNReal.inv_ne_top] at hzero
   rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]
 
+lemma prod_inv_distrib {ι : Type*} {f : ι → ℝ≥0∞} {s : Finset ι}
+    (hf : s.toSet.Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) : (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹ := by
+  induction' s using Finset.cons_induction with i s hi ih
+  · simp
+  simp [← ih (hf.mono <| by simp)]
+  refine ENNReal.mul_inv (not_or_of_imp fun hi₀ ↦ prod_ne_top fun j hj ↦ ?_)
+    (not_or_of_imp fun hi₀ ↦ Finset.prod_ne_zero_iff.2 fun j hj ↦ ?_)
+  · exact imp_iff_not_or.2 (hf (by simp) (by simp [hj]) <| .symm <| ne_of_mem_of_not_mem hj hi) hi₀
+  · exact imp_iff_not_or.2 (hf (by simp [hj]) (by simp) <| ne_of_mem_of_not_mem hj hi).symm hi₀
+
 protected theorem mul_div_mul_left (a b : ℝ≥0∞) (hc : c ≠ 0) (hc' : c ≠ ⊤) :
     c * a / (c * b) = a / b := by
   rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inl hc) (Or.inl hc'), mul_mul_mul_comm,

Mathlib/MeasureTheory/Function/LpSpace.lean

@@ -1192,7 +1192,7 @@ def compLpₗ (L : E →L[𝕜] F) : Lp E p μ →ₗ[𝕜] Lp F p μ where
     ext1
     filter_upwards [Lp.coeFn_smul c f, coeFn_compLp L (c • f), Lp.coeFn_smul c (L.compLp f),
       coeFn_compLp L f] with _ ha1 ha2 ha3 ha4
-    simp only [ha1, ha2, ha3, ha4, map_smul, Pi.smul_apply]
+    simp only [ha1, ha2, ha3, ha4, _root_.map_smul, Pi.smul_apply]
 
 /-- Composing `f : Lp E p μ` with `L : E →L[𝕜] F`, seen as a continuous `𝕜`-linear map on
 `Lp E p μ`. See also the similar

Mathlib/MeasureTheory/Integral/Bochner.lean

@@ -638,7 +638,7 @@ theorem integral_sub (f g : α →₁[μ] E) : integral (f - g) = integral f - i
 theorem integral_smul (c : 𝕜) (f : α →₁[μ] E) : integral (c • f) = c • integral f := by
   simp only [integral]
   show (integralCLM' (E := E) 𝕜) (c • f) = c • (integralCLM' (E := E) 𝕜) f
-  exact map_smul (integralCLM' (E := E) 𝕜) c f
+  exact _root_.map_smul (integralCLM' (E := E) 𝕜) c f
 
 local notation "Integral" => @integralCLM α E _ _ μ _ _
 

Mathlib/Probability/ConditionalProbability.lean

@@ -70,8 +70,8 @@ and scaled by the inverse of `μ s` (to make it a probability measure):
 def cond (s : Set Ω) : Measure Ω :=
   (μ s)⁻¹ • μ.restrict s
 
-@[inherit_doc] scoped notation:max μ "[" t " | " s "]" => ProbabilityTheory.cond μ s t
 @[inherit_doc] scoped notation:max μ "[|" s "]" => ProbabilityTheory.cond μ s
+@[inherit_doc cond] scoped notation3:max μ "[" t " | " s "]" => ProbabilityTheory.cond μ s t
 
 /-- The conditional probability measure of measure `μ` on `{ω | X ω ∈ s}`.
 
@@ -172,7 +172,7 @@ theorem inter_pos_of_cond_ne_zero (hms : MeasurableSet s) (hcst : μ[t|s] ≠ 0)
   simp [hms, Set.inter_comm, cond]
 
 lemma cond_pos_of_inter_ne_zero [IsFiniteMeasure μ] (hms : MeasurableSet s) (hci : μ (s ∩ t) ≠ 0) :
-    0 < μ[|s] t := by
+    0 < μ[t | s] := by
   rw [cond_apply hms]
   refine ENNReal.mul_pos ?_ hci
   exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)

Mathlib/Probability/Independence/Basic.lean

@@ -721,4 +721,61 @@ theorem iIndepSet.iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β
 
 end IndepFun
 
+variable {ι Ω α β : Type*} {mΩ : MeasurableSpace Ω} {mα : MeasurableSpace α}
+  {mβ : MeasurableSpace β} {μ : Measure Ω} {X : ι → Ω → α} {Y : ι → Ω → β} {f : _ → Set Ω}
+  {t : ι → Set β} {s : Finset ι}
+
+/-- The probability of an intersection of preimages conditioning on another intersection factors
+into a product. -/
+lemma cond_iInter [Finite ι] (hY : ∀ i, Measurable (Y i))
+    (hindep : iIndepFun (fun _ ↦ mα.prod mβ) (fun i ω ↦ (X i ω, Y i ω)) μ)
+    (hf : ∀ i ∈ s, MeasurableSet[mα.comap (X i)] (f i))
+    (hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0) (ht : ∀ i, MeasurableSet (t i)) :
+    μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | Y i in t i] := by
+  have : IsProbabilityMeasure (μ : Measure Ω) := hindep.isProbabilityMeasure
+  classical
+  cases nonempty_fintype ι
+  let g (i' : ι) := if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
+  calc
+    _ = (μ (⋂ i, Y i ⁻¹' t i))⁻¹ * μ ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) := by
+      rw [cond_apply]; exact .iInter fun i ↦ hY i (ht i)
+    _ = (μ (⋂ i, Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i) := by
+      congr
+      calc
+        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
+          congr
+          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
+        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
+        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, g]
+    _ = (∏ i, μ (Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i) := by
+      rw [hindep.meas_iInter]
+      exact fun i ↦ ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp [eq_comm]⟩
+    _ = (∏ i, μ (Y i ⁻¹' t i))⁻¹ * ∏ i, μ (g i) := by
+      rw [hindep.meas_iInter]
+      intro i
+      by_cases hi : i ∈ s <;> simp only [hi, ↓reduceIte, g]
+      · obtain ⟨A, hA, hA'⟩ := hf i hi
+        exact .inter ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp [eq_comm]⟩
+          ⟨A ×ˢ Set.univ, hA.prod .univ, by ext; simp [← hA']⟩
+      · exact ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp [eq_comm]⟩
+    _ = ∏ i, (μ (Y i ⁻¹' t i))⁻¹ * μ (g i) := by
+      rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
+      exact fun _ _ i _ _ ↦ .inr <| measure_ne_top _ _
+    _ = ∏ i, if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1 := by
+      refine Finset.prod_congr rfl fun i _ ↦ ?_
+      by_cases hi : i ∈ s
+      · simp only [hi, ↓reduceIte, g, cond_apply (hY i (ht i))]
+      · simp only [hi, ↓reduceIte, g, ENNReal.inv_mul_cancel (hy i hi) (measure_ne_top μ _)]
+    _ = _ := by simp
+
+lemma iIndepFun.cond [Finite ι] (hY : ∀ i, Measurable (Y i))
+    (hindep : iIndepFun (fun _ ↦ mα.prod mβ) (fun i ω ↦ (X i ω, Y i ω)) μ)
+    (hy : ∀ i, μ (Y i ⁻¹' t i) ≠ 0) (ht : ∀ i, MeasurableSet (t i)) :
+    iIndepFun (fun _ ↦ mα) X μ[|⋂ i, Y i ⁻¹' t i] := by
+  rw [iIndepFun_iff]
+  intro s f hf
+  convert cond_iInter hY hindep hf (fun i _ ↦ hy _) ht using 2 with i hi
+  simpa using cond_iInter hY hindep (fun j hj ↦ hf _ <| Finset.mem_singleton.1 hj ▸ hi)
+    (fun i _ ↦ hy _) ht
+
 end ProbabilityTheory

Mathlib/Probability/Independence/Kernel.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
 import Mathlib.MeasureTheory.Constructions.Pi
+import Mathlib.Probability.ConditionalProbability
 import Mathlib.Probability.Kernel.Basic
 import Mathlib.Tactic.Peel
 
@@ -1212,4 +1213,56 @@ theorem iIndepSet.iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β
 
 end IndepFun
 
+variable {ι Ω α β : Type*} {mΩ : MeasurableSpace Ω} {mα : MeasurableSpace α}
+  {mβ : MeasurableSpace β} {κ : Kernel α Ω} {μ : Measure α} {X : ι → Ω → α} {Y : ι → Ω → β}
+  {f : _ → Set Ω} {t : ι → Set β} {s : Finset ι}
+
+/-- The probability of an intersection of preimages conditioning on another intersection factors
+into a product. -/
+lemma iIndepFun.cond_iInter [Finite ι] (hY : ∀ i, Measurable (Y i))
+    (hindep : iIndepFun (fun _ ↦ mα.prod mβ) (fun i ω ↦ (X i ω, Y i ω)) κ μ)
+    (hf : ∀ i ∈ s, MeasurableSet[mα.comap (X i)] (f i))
+    (hy : ∀ᵐ a ∂μ, ∀ i ∉ s, κ a (Y i ⁻¹' t i) ≠ 0) (ht : ∀ i, MeasurableSet (t i)) :
+    ∀ᵐ a ∂μ, (κ a)[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, (κ a)[f i | Y i in t i] := by
+  classical
+  cases nonempty_fintype ι
+  let g (i' : ι) := if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
+  have hYt i : MeasurableSet[(mα.prod mβ).comap fun ω ↦ (X i ω, Y i ω)] (Y i ⁻¹' t i) :=
+    ⟨.univ ×ˢ t i, .prod .univ (ht _), by ext; simp [eq_comm]⟩
+  have hg i : MeasurableSet[(mα.prod mβ).comap fun ω ↦ (X i ω, Y i ω)] (g i) := by
+    by_cases hi : i ∈ s <;> simp only [hi, ↓reduceIte, g]
+    · obtain ⟨A, hA, hA'⟩ := hf i hi
+      exact (hYt _).inter ⟨A ×ˢ .univ, hA.prod .univ, by ext; simp [← hA']⟩
+    · exact hYt _
+  filter_upwards [hy, hindep.ae_isProbabilityMeasure, hindep.meas_iInter hYt, hindep.meas_iInter hg]
+    with a hy _ hYt hg
+  calc
+    _ = (κ a (⋂ i, Y i ⁻¹' t i))⁻¹ * κ a ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) := by
+      rw [cond_apply]; exact .iInter fun i ↦ hY i (ht i)
+    _ = (κ a (⋂ i, Y i ⁻¹' t i))⁻¹ * κ a (⋂ i, g i) := by
+      congr
+      calc
+        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
+          congr
+          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
+        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
+        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, g]
+    _ = (∏ i, κ a (Y i ⁻¹' t i))⁻¹ * κ a (⋂ i, g i) := by
+      rw [hYt]
+    _ = (∏ i, κ a (Y i ⁻¹' t i))⁻¹ * ∏ i, κ a (g i) := by
+      rw [hg]
+    _ = ∏ i, (κ a (Y i ⁻¹' t i))⁻¹ * κ a (g i) := by
+      rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
+      exact fun _ _ i _ _ ↦ .inr <| measure_ne_top _ _
+    _ = ∏ i, if i ∈ s then (κ a)[f i | Y i ⁻¹' t i] else 1 := by
+      refine Finset.prod_congr rfl fun i _ ↦ ?_
+      by_cases hi : i ∈ s
+      · simp only [hi, ↓reduceIte, g, cond_apply (hY i (ht i))]
+      · simp only [hi, ↓reduceIte, g, ENNReal.inv_mul_cancel (hy i hi) (measure_ne_top _ _)]
+    _ = _ := by simp
+
+-- TODO: We can't state `Kernel.iIndepFun.cond` (the `Kernel` analogue of
+-- `ProbabilityTheory.iIndepFun.cond`) because we don't have a version of `ProbabilityTheory.cond`
+-- for kernels
+
 end ProbabilityTheory.Kernel