[Merged by Bors] - chore: notation for (conditional) independence

Mathlib/Probability/HasLaw.lean

@@ -80,7 +80,7 @@ lemma HasLaw.fun_comp {𝒴 : Type*} {m𝒴 : MeasurableSpace 𝒴} {ν : Measur
 @[to_additive]
 lemma IndepFun.hasLaw_mul {M : Type*} [Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M]
     {μ ν : Measure M} [SigmaFinite μ] [SigmaFinite ν] {X Y : Ω → M}
-    (hX : HasLaw X μ P) (hY : HasLaw Y ν P) (hXY : IndepFun X Y P) :
+    (hX : HasLaw X μ P) (hY : HasLaw Y ν P) (hXY : X ⟂ᵢ[P] Y) :
     HasLaw (X * Y) (μ ∗ₘ ν) P where
   map_eq := by
     rw [hXY.map_mul_eq_map_mconv_map₀' hX.aemeasurable hY.aemeasurable, hX.map_eq, hY.map_eq]
@@ -90,7 +90,7 @@ lemma IndepFun.hasLaw_mul {M : Type*} [Monoid M] {mM : MeasurableSpace M} [Measu
 @[to_additive]
 lemma IndepFun.hasLaw_fun_mul {M : Type*} [Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M]
     {μ ν : Measure M} [SigmaFinite μ] [SigmaFinite ν] {X Y : Ω → M}
-    (hX : HasLaw X μ P) (hY : HasLaw Y ν P) (hXY : IndepFun X Y P) :
+    (hX : HasLaw X μ P) (hY : HasLaw Y ν P) (hXY : X ⟂ᵢ[P] Y) :
     HasLaw (fun ω ↦ X ω * Y ω) (μ ∗ₘ ν) P := hXY.hasLaw_mul hX hY
 
 lemma HasLaw.integral_comp {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

Mathlib/Probability/IdentDistrib.lean

@@ -332,9 +332,9 @@ end UniformIntegrable
 then `X'` and `Y'` are independent. -/
 lemma indepFun_of_identDistrib_pair
     {μ : Measure γ} {μ' : Measure δ} [IsFiniteMeasure μ] [IsFiniteMeasure μ']
-    {X : γ → α} {X' : δ → α} {Y : γ → β} {Y' : δ → β} (h_indep : IndepFun X Y μ)
+    {X : γ → α} {X' : δ → α} {Y : γ → β} {Y' : δ → β} (h_indep : X ⟂ᵢ[μ] Y)
     (h_ident : IdentDistrib (fun ω ↦ (X ω, Y ω)) (fun ω ↦ (X' ω, Y' ω)) μ μ') :
-    IndepFun X' Y' μ' := by
+    X' ⟂ᵢ[μ'] Y' := by
   rw [indepFun_iff_map_prod_eq_prod_map_map _ _, ← h_ident.map_eq,
     (indepFun_iff_map_prod_eq_prod_map_map _ _).1 h_indep]
   · exact congr (congrArg Measure.prod <| (h_ident.comp measurable_fst).map_eq)

Mathlib/Probability/Independence/Basic.lean

@@ -31,6 +31,13 @@ import Mathlib.MeasureTheory.Group.Convolution
   measurable space structures they generate are independent.
 * `IndepSets.indep`: variant with two π-systems.
 
+These notations are scoped in the `ProbabilityTheory` namespace.
+
+## Notation
+
+* `X ⟂ᵢ[μ] Y` for `IndepFun X Y μ`, independence of two random variables.
+* `X ⟂ᵢ Y` for `IndepFun X Y volume`.
+
 ## Implementation notes
 
 The definitions of independence in this file are a particular case of independence with respect to a
@@ -135,6 +142,12 @@ def IndepFun {β γ} {_mΩ : MeasurableSpace Ω} [MeasurableSpace β] [Measurabl
 
 end Definitions
 
+@[inherit_doc ProbabilityTheory.IndepFun]
+scoped[ProbabilityTheory] notation3 X:50 " ⟂ᵢ[" μ "] " Y:50 => ProbabilityTheory.IndepFun X Y μ
+
+@[inherit_doc ProbabilityTheory.IndepFun]
+scoped[ProbabilityTheory] notation3 X:50 " ⟂ᵢ " Y:50 => ProbabilityTheory.IndepFun X Y volume
+
 section Definition_lemmas
 variable {π : ι → Set (Set Ω)} {m : ι → MeasurableSpace Ω} {_ : MeasurableSpace Ω} {μ : Measure Ω}
   {S : Finset ι} {s : ι → Set Ω}
@@ -250,17 +263,17 @@ lemma iIndepFun.meas_iInter [Fintype ι] {m : ∀ i, MeasurableSpace (κ i)} {f
 
 lemma IndepFun_iff_Indep [mβ : MeasurableSpace β]
     [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : Measure Ω) :
-    IndepFun f g μ ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ := by
+    f ⟂ᵢ[μ] g ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ := by
   simp only [IndepFun, Indep, Kernel.IndepFun]
 
 lemma IndepFun_iff {β γ} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ]
     (f : Ω → β) (g : Ω → γ) (μ : Measure Ω) :
-    IndepFun f g μ ↔ ∀ t1 t2, MeasurableSet[MeasurableSpace.comap f mβ] t1
+    f ⟂ᵢ[μ] g ↔ ∀ t1 t2, MeasurableSet[MeasurableSpace.comap f mβ] t1
       → 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)
+    (hfg : 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
@@ -366,7 +379,7 @@ theorem iIndep.indep
 theorem iIndepFun.indepFun {β : ι → Type*}
     {m : ∀ x, MeasurableSpace (β x)} {f : ∀ i, Ω → β i} (hf_Indep : iIndepFun f μ) {i j : ι}
     (hij : i ≠ j) :
-    IndepFun (f i) (f j) μ :=
+    f i ⟂ᵢ[μ] f j :=
   Kernel.iIndepFun.indepFun hf_Indep hij
 
 end FromIndepToIndep
@@ -563,7 +576,7 @@ variable {β β' γ γ' : Type*} {_mΩ : MeasurableSpace Ω} {μ : Measure Ω} {
 
 theorem indepFun_iff_measure_inter_preimage_eq_mul {mβ : MeasurableSpace β}
     {mβ' : MeasurableSpace β'} :
-    IndepFun f g μ ↔
+    f ⟂ᵢ[μ] g ↔
       ∀ s t, MeasurableSet s → MeasurableSet t
         → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t) := by
   simp only [IndepFun, Kernel.indepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq,
@@ -600,14 +613,14 @@ nonrec lemma iIndepFun.comp₀ {β γ : ι → Type*} {mβ : ∀ i, MeasurableSp
 
 theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     [IsZeroOrProbabilityMeasure μ] (hf : Measurable f) (hg : Measurable g) :
-    IndepFun f g μ ↔
+    f ⟂ᵢ[μ] g ↔
       ∀ s t, MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) μ := by
   simp only [IndepFun, IndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]
 
 theorem indepFun_iff_map_prod_eq_prod_map_map' {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
     (σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) :
-    IndepFun f g μ ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
+    f ⟂ᵢ[μ] g ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
   rw [indepFun_iff_measure_inter_preimage_eq_mul]
   have h₀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) :
       μ (f ⁻¹' s) * μ (g ⁻¹' t) = μ.map f s * μ.map g t ∧
@@ -622,7 +635,7 @@ theorem indepFun_iff_map_prod_eq_prod_map_map' {mβ : MeasurableSpace β} {mβ'
 
 theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     [IsFiniteMeasure μ] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
-    IndepFun f g μ ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
+    f ⟂ᵢ[μ] g ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
   apply indepFun_iff_map_prod_eq_prod_map_map' hf hg <;> apply IsFiniteMeasure.toSigmaFinite
 
 theorem iIndepFun_iff_map_fun_eq_pi_map [Fintype ι] {β : ι → Type*}
@@ -655,11 +668,11 @@ theorem iIndepFun_iff_map_fun_eq_pi_map [Fintype ι] {β : ι → Type*}
 
 @[symm]
 nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {_ : MeasurableSpace β'}
-    (hfg : IndepFun f g μ) : IndepFun g f μ := hfg.symm
+    (hfg : f ⟂ᵢ[μ] g) : g ⟂ᵢ[μ] f := hfg.symm
 
 theorem IndepFun.congr {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
-    {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g μ)
-    (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') : IndepFun f' g' μ := by
+    {f' : Ω → β} {g' : Ω → β'} (hfg : f ⟂ᵢ[μ] g) (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') :
+    f' ⟂ᵢ[μ] g' := by
   refine Kernel.IndepFun.congr' hfg ?_ ?_ <;> simpa
 
 @[deprecated (since := "2025-03-18")] alias IndepFun.ae_eq := IndepFun.congr
@@ -673,7 +686,7 @@ variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'
 /-- Given random variables `X : Ω → 𝓧` and `Y : Ω' → 𝓨`, they are independent when viewed as random
 variables defined on the product space `Ω × Ω'`. -/
 lemma indepFun_prod (mX : Measurable X) (mY : Measurable Y) :
-    IndepFun (fun ω ↦ X ω.1) (fun ω ↦ Y ω.2) (μ.prod ν) := by
+    (fun ω ↦ X ω.1) ⟂ᵢ[μ.prod ν] (fun ω ↦ Y ω.2) := by
   refine indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop) |>.2 ?_
   convert Measure.map_prod_map μ ν mX mY |>.symm
   · rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod,
@@ -684,8 +697,8 @@ lemma indepFun_prod (mX : Measurable X) (mY : Measurable Y) :
 /-- Given random variables `X : Ω → 𝓧` and `Y : Ω' → 𝓨`, they are independent when viewed as random
 variables defined on the product space `Ω × Ω'`. -/
 lemma indepFun_prod₀ (mX : AEMeasurable X μ) (mY : AEMeasurable Y ν) :
-    IndepFun (fun ω ↦ X ω.1) (fun ω ↦ Y ω.2) (μ.prod ν) := by
-  have : IndepFun (fun ω ↦ mX.mk X ω.1) (fun ω ↦ mY.mk Y ω.2) (μ.prod ν) :=
+    (fun ω ↦ X ω.1) ⟂ᵢ[μ.prod ν] (fun ω ↦ Y ω.2) := by
+  have : (fun ω ↦ mX.mk X ω.1) ⟂ᵢ[μ.prod ν] (fun ω ↦ mY.mk Y ω.2) :=
     indepFun_prod mX.measurable_mk mY.measurable_mk
   refine this.congr ?_ ?_
   · rw [← Function.comp_def, ← Function.comp_def]
@@ -722,34 +735,34 @@ end Prod
 
 theorem IndepFun.comp {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'}
     {_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'}
-    (hfg : IndepFun f g μ) (hφ : Measurable φ) (hψ : Measurable ψ) :
-    IndepFun (φ ∘ f) (ψ ∘ g) μ :=
+    (hfg : f ⟂ᵢ[μ] g) (hφ : Measurable φ) (hψ : Measurable ψ) :
+    (φ ∘ f) ⟂ᵢ[μ] ψ ∘ g :=
   Kernel.IndepFun.comp hfg hφ hψ
 
 theorem IndepFun.comp₀ {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'}
     {_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'}
-    (hfg : IndepFun f g μ) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    (hfg : f ⟂ᵢ[μ] g) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
     (hφ : AEMeasurable φ (μ.map f)) (hψ : AEMeasurable ψ (μ.map g)) :
-    IndepFun (φ ∘ f) (ψ ∘ g) μ :=
+    (φ ∘ f) ⟂ᵢ[μ] (ψ ∘ g) :=
   Kernel.IndepFun.comp₀ hfg (by simp [hf]) (by simp [hg]) (by simp [hφ]) (by simp [hψ])
 
 lemma indepFun_const_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     [IsZeroOrProbabilityMeasure μ] (c : β) (X : Ω → β') :
-    IndepFun (fun _ ↦ c) X μ :=
+    (fun _ ↦ c) ⟂ᵢ[μ] X :=
   Kernel.indepFun_const_left c X
 
 lemma indepFun_const_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     [IsZeroOrProbabilityMeasure μ] (X : Ω → β) (c : β') :
-    IndepFun X (fun _ ↦ c) μ :=
+    X ⟂ᵢ[μ] (fun _ ↦ c) :=
   Kernel.indepFun_const_right X c
 
 theorem IndepFun.neg_right {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β']
-    [MeasurableNeg β'] (hfg : IndepFun f g μ) :
-    IndepFun f (-g) μ := hfg.comp measurable_id measurable_neg
+    [MeasurableNeg β'] (hfg : f ⟂ᵢ[μ] g) :
+    f ⟂ᵢ[μ] (-g) := hfg.comp measurable_id measurable_neg
 
 theorem IndepFun.neg_left {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β]
-    [MeasurableNeg β] (hfg : IndepFun f g μ) :
-    IndepFun (-f) g μ := hfg.comp measurable_neg measurable_id
+    [MeasurableNeg β] (hfg : f ⟂ᵢ[μ] g) :
+    (-f) ⟂ᵢ[μ] g := hfg.comp measurable_neg measurable_id
 
 section iIndepFun
 variable {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i}
@@ -1042,7 +1055,7 @@ variable {M : Type*} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M]
 @[to_additive]
 theorem IndepFun.map_mul_eq_map_mconv_map₀'
     {f g : Ω → M} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
-    (σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) (hfg : IndepFun f g μ) :
+    (σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) (hfg : f ⟂ᵢ[μ] g) :
     μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) := by
   conv in f * g => change (fun x ↦ x.1 * x.2) ∘ (fun ω ↦ (f ω, g ω))
   rw [← measurable_mul.aemeasurable.map_map_of_aemeasurable (hf.prodMk hg),
@@ -1051,22 +1064,22 @@ theorem IndepFun.map_mul_eq_map_mconv_map₀'
 @[to_additive]
 theorem IndepFun.map_mul_eq_map_mconv_map'
     {f g : Ω → M} (hf : Measurable f) (hg : Measurable g)
-    (σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) (hfg : IndepFun f g μ) :
+    (σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) (hfg : f ⟂ᵢ[μ] g) :
     μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) :=
   hfg.map_mul_eq_map_mconv_map₀' hf.aemeasurable hg.aemeasurable σf σg
 
 @[to_additive]
 theorem IndepFun.map_mul_eq_map_mconv_map₀
     [IsFiniteMeasure μ] {f g : Ω → M} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
-    (hfg : IndepFun f g μ) :
+    (hfg : f ⟂ᵢ[μ] g) :
     μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) := by
   apply hfg.map_mul_eq_map_mconv_map₀' hf hg
     <;> apply IsFiniteMeasure.toSigmaFinite
 
 @[to_additive]
 theorem IndepFun.map_mul_eq_map_mconv_map
     [IsFiniteMeasure μ] {f g : Ω → M} (hf : Measurable f) (hg : Measurable g)
-    (hfg : IndepFun f g μ) :
+    (hfg : f ⟂ᵢ[μ] g) :
     μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) :=
   hfg.map_mul_eq_map_mconv_map₀ hf.aemeasurable hg.aemeasurable
 

Mathlib/Probability/Independence/CharacteristicFunction.lean

@@ -40,7 +40,7 @@ variable [InnerProductSpace ℝ E] [InnerProductSpace ℝ F]
 to the product of the characteristic functions. This is the version for Hilbert spaces, see
 `indepFun_iff_charFunDual_prod` for the Banach space version. -/
 lemma indepFun_iff_charFun_prod (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
-    IndepFun X Y P ↔ ∀ t, charFun (P.map (fun ω ↦ toLp 2 (X ω, Y ω))) t =
+    X ⟂ᵢ[P] Y ↔ ∀ t, charFun (P.map (fun ω ↦ toLp 2 (X ω, Y ω))) t =
       charFun (P.map X) t.ofLp.1 * charFun (P.map Y) t.ofLp.2 := by
   rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFun_eq_prod_iff,
     AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]
@@ -55,7 +55,7 @@ variable [NormedSpace ℝ E] [NormedSpace ℝ F]
 to the product of the characteristic functions. This is the version for Banach spaces, see
 `indepFun_iff_charFun_prod` for the Hilbert space version. -/
 lemma indepFun_iff_charFunDual_prod (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
-    IndepFun X Y P ↔ ∀ L, charFunDual (P.map (fun ω ↦ (X ω, Y ω))) L =
+    X ⟂ᵢ[P] Y ↔ ∀ L, charFunDual (P.map (fun ω ↦ (X ω, Y ω))) L =
       charFunDual (P.map X) (L.comp (.inl ℝ E F)) *
       charFunDual (P.map Y) (L.comp (.inr ℝ E F)) := by
   rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFunDual_eq_prod_iff]
@@ -64,7 +64,7 @@ lemma indepFun_iff_charFunDual_prod (hX : AEMeasurable X P) (hY : AEMeasurable Y
 to the product of the characteristic functions. This is `indepFun_iff_charFunDual_prod` for
 `WithLp`. See `indepFun_iff_charFun_prod` for the Hilbert space version. -/
 lemma indepFun_iff_charFunDual_prod' (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
-    IndepFun X Y P ↔ ∀ L, charFunDual (P.map (fun ω ↦ toLp p (X ω, Y ω))) L =
+    X ⟂ᵢ[P] Y ↔ ∀ L, charFunDual (P.map (fun ω ↦ toLp p (X ω, Y ω))) L =
       charFunDual (P.map X) (L.comp
         ((prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp
           (.inl ℝ E F))) *

Mathlib/Probability/Independence/Conditional.lean

@@ -44,6 +44,14 @@ as for a family, but without the starting `i`, for example `CondIndepFun` is the
   of sets, then the measurable space structures they generate are conditionally independent.
 * `ProbabilityTheory.condIndepSets.condIndep`: variant with two π-systems.
 
+## Notation
+
+* `X ⟂ᵢ[Z, hZ; μ] Y` for `CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le X Y μ`,
+  independence of `X` and `Y` given `Z`.
+* `X ⟂ᵢ[Z, hZ] Y` for the cases of `μ = volume`.
+
+These notations are scoped in the `ProbabilityTheory` namespace.
+
 ## Implementation notes
 
 The definitions of conditional independence in this file are a particular case of independence with
@@ -145,6 +153,16 @@ end
 
 end Definitions
 
+@[inherit_doc ProbabilityTheory.CondIndepFun]
+scoped[ProbabilityTheory] notation3 X:50 " ⟂ᵢ[" Z ", " hZ "; " μ "] " Y:50 =>
+  ProbabilityTheory.CondIndepFun (MeasurableSpace.comap Z inferInstance) (Measurable.comap_le hZ)
+  X Y μ
+
+@[inherit_doc ProbabilityTheory.CondIndepFun]
+scoped[ProbabilityTheory] notation3 X:50 " ⟂ᵢ[" Z ", " hZ "] " Y:50 =>
+  ProbabilityTheory.CondIndepFun (MeasurableSpace.comap Z inferInstance) (Measurable.comap_le hZ)
+  X Y volume
+
 section DefinitionLemmas
 
 section
@@ -731,12 +749,12 @@ lemma condIndepFun_of_measurable_right {mβ : MeasurableSpace β} {mβ' : Measur
 
 lemma condIndepFun_self_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     {X : Ω → β} {Z : Ω → β'} (hX : Measurable X) (hZ : Measurable Z) :
-    CondIndepFun (mβ'.comap Z) hZ.comap_le Z X μ :=
+    Z ⟂ᵢ[Z, hZ; μ] X :=
   condIndepFun_of_measurable_left (comap_measurable Z) hX
 
 lemma condIndepFun_self_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     {X : Ω → β} {Z : Ω → β'} (hX : Measurable X) (hZ : Measurable Z) :
-    CondIndepFun (mβ'.comap Z) hZ.comap_le X Z μ :=
+    X ⟂ᵢ[Z, hZ; μ] Z :=
   condIndepFun_of_measurable_right hX (comap_measurable Z)
 
 /-- Two random variables are conditionally independent iff they satisfy the almost sure equality
@@ -797,7 +815,7 @@ theorem condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib
     {γ : Type*} {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β'] [Nonempty β']
     (hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) :
-    CondIndepFun _ hk.comap_le f g μ ↔
+    f ⟂ᵢ[k, hk; μ] g ↔
       μ.map (fun ω ↦ (k ω, f ω, g ω)) =
         (Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ μ.map k := by
   rw [condIndepFun_iff_map_prod_eq_prod_comp_trim hf hg]
@@ -847,7 +865,7 @@ theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft
     {γ : Type*} {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β'] [Nonempty β']
     (hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) :
-    CondIndepFun (mγ.comap k) hk.comap_le g f μ ↔
+    g ⟂ᵢ[k, hk; μ] f ↔
       condDistrib f (fun ω ↦ (k ω, g ω)) μ =ᵐ[μ.map (fun ω ↦ (k ω, g ω))]
         (condDistrib f k μ).prodMkRight _ := by
   rw [condDistrib_ae_eq_iff_measure_eq_compProd (μ := μ) _ hf.aemeasurable,

Mathlib/Probability/Independence/Integrable.lean

@@ -28,7 +28,7 @@ variable {Ω E F : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
 the space is a probability space. -/
 lemma MemLp.isProbabilityMeasure_of_indepFun
     (f : Ω → E) (g : Ω → F) {p : ℝ≥0∞} (hp : p ≠ 0) (hp' : p ≠ ∞)
-    (hℒp : MemLp f p μ) (h'f : ¬ (∀ᵐ ω ∂μ, f ω = 0)) (hindep : IndepFun f g μ) :
+    (hℒp : MemLp f p μ) (h'f : ¬ (∀ᵐ ω ∂μ, f ω = 0)) (hindep : f ⟂ᵢ[μ] g) :
     IsProbabilityMeasure μ := by
   obtain ⟨c, c_pos, hc⟩ : ∃ (c : ℝ≥0), 0 < c ∧ 0 < μ {ω | c ≤ ‖f ω‖₊} := by
     contrapose! h'f
@@ -47,7 +47,7 @@ lemma MemLp.isProbabilityMeasure_of_indepFun
 /-- If a nonzero function is integrable and is independent of another function, then
 the space is a probability space. -/
 lemma Integrable.isProbabilityMeasure_of_indepFun (f : Ω → E) (g : Ω → F)
-    (hf : Integrable f μ) (h'f : ¬ (∀ᵐ ω ∂μ, f ω = 0)) (hindep : IndepFun f g μ) :
+    (hf : Integrable f μ) (h'f : ¬ (∀ᵐ ω ∂μ, f ω = 0)) (hindep : f ⟂ᵢ[μ] g) :
     IsProbabilityMeasure μ :=
   MemLp.isProbabilityMeasure_of_indepFun f g one_ne_zero ENNReal.one_ne_top
     (memLp_one_iff_integrable.mpr hf) h'f hindep