feat: when the indicator is independent from a random variable (leanprover-community#39749)

If `A` is an event from a sigma-algebra `m` that is independent from a random variable `X`, then the indicator of  `A` is independent from `X`.

Author: EtienneC30

Mathlib/Probability/Independence/Basic.lean

@@ -1035,6 +1035,12 @@ theorem iIndepSet.iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β
     iIndepFun (fun n => (s n).indicator fun _ω => (1 : β)) μ :=
   Kernel.iIndepSet.iIndepFun_indicator hs
 
+lemma Indep.indicator_indepFun {m : MeasurableSpace Ω} {M 𝓧 : Type*}
+    [Zero M] [MeasurableSpace M] (c : M) [NeZero c] {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω}
+    {X : Ω → 𝓧} (hA : MeasurableSet[m] A) (h : Indep m (m𝓧.comap X) μ) :
+    (A.indicator (fun _ ↦ c)) ⟂ᵢ[μ] X :=
+  Kernel.Indep.indicator_const_indepFun c hA h
+
 end IndepFun
 
 variable {ι Ω α β : Type*} {mΩ : MeasurableSpace Ω} {mα : MeasurableSpace α}

Mathlib/Probability/Independence/Kernel/IndepFun.lean

@@ -694,6 +694,12 @@ theorem iIndepSet.iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β
   · exact @MeasurableSet.empty _ (generateFrom {s i})
   · exact @MeasurableSet.empty _ (generateFrom {s i})
 
+lemma Indep.indicator_const_indepFun {m : MeasurableSpace Ω} {M 𝓧 : Type*}
+    [Zero M] [MeasurableSpace M] (c : M) [NeZero c] {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω}
+    {X : Ω → 𝓧} (hA : MeasurableSet[m] A) (h : Indep m (m𝓧.comap X) κ μ) :
+    IndepFun (A.indicator (fun _ ↦ c)) X κ μ :=
+  indep_of_indep_of_le_left h (measurable_const.indicator hA).comap_le
+
 variable {mβ : MeasurableSpace β} {X : ι → Ω → α} {Y : ι → Ω → β}
   {f : _ → Set Ω} {t : ι → Set β} {s : Finset ι}