Documentation

Mathlib.Probability.Independence.Conditional

Conditional Independence #

We define conditional independence of sets/σ-algebras/functions with respect to a σ-algebra.

Two σ-algebras m₁ and m₂ are conditionally independent given a third σ-algebra m' if for all m₁-measurable sets t₁ and m₂-measurable sets t₂, μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧.

On standard Borel spaces, the conditional expectation with respect to m' defines a kernel ProbabilityTheory.condexpKernel, and the definition above is equivalent to ∀ᵐ ω ∂μ, condexpKernel μ m' ω (t₁ ∩ t₂) = condexpKernel μ m' ω t₁ * condexpKernel μ m' ω t₂. We use this property as the definition of conditional independence.

Main definitions #

We provide four definitions of conditional independence:

Additionally, we provide four corresponding statements for two measurable space structures (resp. sets of sets, sets, functions) instead of a family. These properties are denoted by the same names as for a family, but without the starting i, for example CondIndepFun is the version of iCondIndepFun for two functions.

Main statements #

Implementation notes #

The definitions of conditional independence in this file are a particular case of independence with respect to a kernel and a measure, as defined in the file Probability/Independence/Kernel.lean. The kernel used is ProbabilityTheory.condexpKernel.

def ProbabilityTheory.iCondIndepSets {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (π : ιSet (Set Ω)) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] :

A family of sets of sets π : ι → Set (Set Ω) is conditionally independent given m' with respect to a measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ π i_1, ..., f i_n ∈ π i_n, then μ⟦⋂ i in s, f i | m'⟧ =ᵐ[μ] ∏ i ∈ s, μ⟦f i | m'⟧. See ProbabilityTheory.iCondIndepSets_iff. It will be used for families of pi_systems.

Equations
Instances For
    def ProbabilityTheory.CondIndepSets {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (s1 : Set (Set Ω)) (s2 : Set (Set Ω)) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] :

    Two sets of sets s₁, s₂ are conditionally independent given m' with respect to a measure μ if for any sets t₁ ∈ s₁, t₂ ∈ s₂, then μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧. See ProbabilityTheory.condIndepSets_iff.

    Equations
    Instances For

      A family of measurable space structures (i.e. of σ-algebras) is conditionally independent given m' with respect to a measure μ (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. m : ι → MeasurableSpace Ω is conditionally independent given m' with respect to measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ m i_1, ..., f i_n ∈ m i_n, then μ⟦⋂ i in s, f i | m'⟧ =ᵐ[μ] ∏ i ∈ s, μ⟦f i | m'⟧ . See ProbabilityTheory.iCondIndep_iff.

      Equations
      Instances For

        Two measurable space structures (or σ-algebras) m₁, m₂ are conditionally independent given m' with respect to a measure μ (defined on a third σ-algebra) if for any sets t₁ ∈ m₁, t₂ ∈ m₂, μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧. See ProbabilityTheory.condIndep_iff.

        Equations
        Instances For
          def ProbabilityTheory.iCondIndepSet {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (s : ιSet Ω) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] :

          A family of sets is conditionally independent if the family of measurable space structures they generate is conditionally independent. For a set s, the generated measurable space has measurable sets ∅, s, sᶜ, univ. See ProbabilityTheory.iCondIndepSet_iff.

          Equations
          Instances For

            Two sets are conditionally independent if the two measurable space structures they generate are conditionally independent. For a set s, the generated measurable space structure has measurable sets ∅, s, sᶜ, univ. See ProbabilityTheory.condIndepSet_iff.

            Equations
            Instances For
              def ProbabilityTheory.iCondIndepFun {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) {β : ιType u_3} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] :

              A family of functions defined on the same space Ω and taking values in possibly different spaces, each with a measurable space structure, is conditionally independent if the family of measurable space structures they generate on Ω is conditionally independent. For a function g with codomain having measurable space structure m, the generated measurable space structure is m.comap g. See ProbabilityTheory.iCondIndepFun_iff.

              Equations
              Instances For
                def ProbabilityTheory.CondIndepFun {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) {β : Type u_3} {γ : Type u_4} [MeasurableSpace β] [MeasurableSpace γ] (f : Ωβ) (g : Ωγ) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] :

                Two functions are conditionally independent if the two measurable space structures they generate are conditionally independent. For a function f with codomain having measurable space structure m, the generated measurable space structure is m.comap f. See ProbabilityTheory.condIndepFun_iff.

                Equations
                Instances For
                  theorem ProbabilityTheory.iCondIndepSets_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (π : ιSet (Set Ω)) (hπ : ∀ (i : ι), sπ i, MeasurableSet s) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.iCondIndepSets m' hm' π μ ∀ (s : Finset ι) {f : ιSet Ω}, (is, f i π i)MeasureTheory.condexp m' μ ((is, f i).indicator fun (ω : Ω) => 1) =ᵐ[μ] is, MeasureTheory.condexp m' μ ((f i).indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.condIndepSets_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (s1 : Set (Set Ω)) (s2 : Set (Set Ω)) (hs1 : ss1, MeasurableSet s) (hs2 : ss2, MeasurableSet s) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.CondIndepSets m' hm' s1 s2 μ ∀ (t1 t2 : Set Ω), t1 s1t2 s2MeasureTheory.condexp m' μ ((t1 t2).indicator fun (ω : Ω) => 1) =ᵐ[μ] MeasureTheory.condexp m' μ (t1.indicator fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (t2.indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.iCondIndepSets_singleton_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (s : ιSet Ω) (hπ : ∀ (i : ι), MeasurableSet (s i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.iCondIndepSets m' hm' (fun (i : ι) => {s i}) μ ∀ (S : Finset ι), MeasureTheory.condexp m' μ ((iS, s i).indicator fun (ω : Ω) => 1) =ᵐ[μ] iS, MeasureTheory.condexp m' μ ((s i).indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.condIndepSets_singleton_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} {t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) :
                  ProbabilityTheory.CondIndepSets m' hm' {s} {t} μ MeasureTheory.condexp m' μ ((s t).indicator fun (ω : Ω) => 1) =ᵐ[μ] MeasureTheory.condexp m' μ (s.indicator fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (t.indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.iCondIndep_iff_iCondIndepSets {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (m : ιMeasurableSpace Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.iCondIndep m' hm' m μ ProbabilityTheory.iCondIndepSets m' hm' (fun (x : ι) => {s : Set Ω | MeasurableSet s}) μ
                  theorem ProbabilityTheory.iCondIndep_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (m : ιMeasurableSpace Ω) (hm : ∀ (i : ι), m i ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.iCondIndep m' hm' m μ ∀ (s : Finset ι) {f : ιSet Ω}, (is, MeasurableSet (f i))MeasureTheory.condexp m' μ ((is, f i).indicator fun (ω : Ω) => 1) =ᵐ[μ] is, MeasureTheory.condexp m' μ ((f i).indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.condIndep_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) (m₁ : MeasurableSpace Ω) (m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (hm₁ : m₁ ) (hm₂ : m₂ ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ ∀ (t1 t2 : Set Ω), MeasurableSet t1MeasurableSet t2MeasureTheory.condexp m' μ ((t1 t2).indicator fun (ω : Ω) => 1) =ᵐ[μ] MeasureTheory.condexp m' μ (t1.indicator fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (t2.indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.iCondIndepSet_iff_iCondIndepSets_singleton {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (s : ιSet Ω) (hs : ∀ (i : ι), MeasurableSet (s i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.iCondIndepSet m' hm' s μ ProbabilityTheory.iCondIndepSets m' hm' (fun (i : ι) => {s i}) μ
                  theorem ProbabilityTheory.iCondIndepSet_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (s : ιSet Ω) (hs : ∀ (i : ι), MeasurableSet (s i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.iCondIndepSet m' hm' s μ ∀ (S : Finset ι), MeasureTheory.condexp m' μ ((iS, s i).indicator fun (ω : Ω) => 1) =ᵐ[μ] iS, MeasureTheory.condexp m' μ ((s i).indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.condIndepSet_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) (s : Set Ω) (t : Set Ω) (hs : MeasurableSet s) (ht : MeasurableSet t) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.CondIndepSet m' hm' s t μ MeasureTheory.condexp m' μ ((s t).indicator fun (ω : Ω) => 1) =ᵐ[μ] MeasureTheory.condexp m' μ (s.indicator fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (t.indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.iCondIndepFun_iff_iCondIndep {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) {β : ιType u_3} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.iCondIndepFun m' hm' m f μ ProbabilityTheory.iCondIndep m' hm' (fun (x : ι) => MeasurableSpace.comap (f x) (m x)) μ
                  theorem ProbabilityTheory.iCondIndepFun_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) {β : ιType u_3} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (hf : ∀ (i : ι), Measurable (f i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.iCondIndepFun m' hm' m f μ ∀ (s : Finset ι) {g : ιSet Ω}, (is, MeasurableSet (g i))MeasureTheory.condexp m' μ ((is, g i).indicator fun (ω : Ω) => 1) =ᵐ[μ] is, MeasureTheory.condexp m' μ ((g i).indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.condIndepFun_iff_condIndep {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) {β : Type u_3} {γ : Type u_4} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ωβ) (g : Ωγ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  theorem ProbabilityTheory.condIndepFun_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ) {β : Type u_3} {γ : Type u_4} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ωβ) (g : Ωγ) (hf : Measurable f) (hg : Measurable g) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
                  ProbabilityTheory.CondIndepFun m' hm' f g μ ∀ (t1 t2 : Set Ω), MeasurableSet t1MeasurableSet t2MeasureTheory.condexp m' μ ((t1 t2).indicator fun (ω : Ω) => 1) =ᵐ[μ] MeasureTheory.condexp m' μ (t1.indicator fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (t2.indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.CondIndepSets.symm {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} (h : ProbabilityTheory.CondIndepSets m' hm' s₁ s₂ μ) :
                  theorem ProbabilityTheory.condIndepSets_of_condIndepSets_of_le_left {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} (h_indep : ProbabilityTheory.CondIndepSets m' hm' s₁ s₂ μ) (h31 : s₃ s₁) :
                  theorem ProbabilityTheory.condIndepSets_of_condIndepSets_of_le_right {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} (h_indep : ProbabilityTheory.CondIndepSets m' hm' s₁ s₂ μ) (h32 : s₃ s₂) :
                  theorem ProbabilityTheory.CondIndepSets.union {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} (h₁ : ProbabilityTheory.CondIndepSets m' hm' s₁ s' μ) (h₂ : ProbabilityTheory.CondIndepSets m' hm' s₂ s' μ) :
                  ProbabilityTheory.CondIndepSets m' hm' (s₁ s₂) s' μ
                  @[simp]
                  theorem ProbabilityTheory.CondIndepSets.union_iff {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} :
                  theorem ProbabilityTheory.CondIndepSets.iUnion {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ιSet (Set Ω)} {s' : Set (Set Ω)} (hyp : ∀ (n : ι), ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ) :
                  ProbabilityTheory.CondIndepSets m' hm' (⋃ (n : ι), s n) s' μ
                  theorem ProbabilityTheory.CondIndepSets.bUnion {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (hyp : nu, ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ) :
                  ProbabilityTheory.CondIndepSets m' hm' (nu, s n) s' μ
                  theorem ProbabilityTheory.CondIndepSets.inter {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s' : Set (Set Ω)} (s₂ : Set (Set Ω)) (h₁ : ProbabilityTheory.CondIndepSets m' hm' s₁ s' μ) :
                  ProbabilityTheory.CondIndepSets m' hm' (s₁ s₂) s' μ
                  theorem ProbabilityTheory.CondIndepSets.iInter {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ιSet (Set Ω)} {s' : Set (Set Ω)} (h : ∃ (n : ι), ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ) :
                  ProbabilityTheory.CondIndepSets m' hm' (⋂ (n : ι), s n) s' μ
                  theorem ProbabilityTheory.CondIndepSets.bInter {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (h : nu, ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ) :
                  ProbabilityTheory.CondIndepSets m' hm' (nu, s n) s' μ
                  theorem ProbabilityTheory.CondIndep.symm {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h : ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ) :
                  ProbabilityTheory.CondIndep m' m₂ m₁ hm' μ
                  theorem ProbabilityTheory.condIndep_of_condIndep_of_le_left {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m₃ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ) (h31 : m₃ m₁) :
                  ProbabilityTheory.CondIndep m' m₃ m₂ hm' μ
                  theorem ProbabilityTheory.condIndep_of_condIndep_of_le_right {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m₃ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ) (h32 : m₃ m₂) :
                  ProbabilityTheory.CondIndep m' m₁ m₃ hm' μ

                  Deducing CondIndep from iCondIndep #

                  theorem ProbabilityTheory.iCondIndepSets.condIndepSets {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ιSet (Set Ω)} (h_indep : ProbabilityTheory.iCondIndepSets m' hm' s μ) {i : ι} {j : ι} (hij : i j) :
                  ProbabilityTheory.CondIndepSets m' hm' (s i) (s j) μ
                  theorem ProbabilityTheory.iCondIndep.condIndep {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : ιMeasurableSpace Ω} (h_indep : ProbabilityTheory.iCondIndep m' hm' m μ) {i : ι} {j : ι} (hij : i j) :
                  ProbabilityTheory.CondIndep m' (m i) (m j) hm' μ
                  theorem ProbabilityTheory.iCondIndepFun.condIndepFun {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ιType u_3} {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ωβ i} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' m f μ) {i : ι} {j : ι} (hij : i j) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i) (f j) μ

                  π-system lemma #

                  Conditional independence of measurable spaces is equivalent to conditional independence of generating π-systems.

                  Conditional independence of σ-algebras implies conditional independence of #

                  generating π-systems

                  theorem ProbabilityTheory.iCondIndep.iCondIndepSets {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : ιMeasurableSpace Ω} {s : ιSet (Set Ω)} (hms : ∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)) (h_indep : ProbabilityTheory.iCondIndep m' hm' m μ) :

                  Conditional independence of generating π-systems implies conditional independence of #

                  σ-algebras

                  theorem ProbabilityTheory.CondIndepSets.condIndep {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (h1 : m₁ ) (h2 : m₂ ) (hp1 : IsPiSystem p1) (hp2 : IsPiSystem p2) (hpm1 : m₁ = MeasurableSpace.generateFrom p1) (hpm2 : m₂ = MeasurableSpace.generateFrom p2) (hyp : ProbabilityTheory.CondIndepSets m' hm' p1 p2 μ) :
                  ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ
                  theorem ProbabilityTheory.CondIndepSets.condIndep' {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (hp1m : sp1, MeasurableSet s) (hp2m : sp2, MeasurableSet s) (hp1 : IsPiSystem p1) (hp2 : IsPiSystem p2) (hyp : ProbabilityTheory.CondIndepSets m' hm' p1 p2 μ) :
                  theorem ProbabilityTheory.condIndepSets_piiUnionInter_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ιSet (Set Ω)} {S : Set ι} {T : Set ι} (h_indep : ProbabilityTheory.iCondIndepSets m' hm' s μ) (hST : Disjoint S T) :
                  theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iCondIndepSet m' hm' s μ) (S : Set ι) (T : Set ι) (hST : Disjoint S T) :
                  ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {t : Set Ω | nS, s n = t}) (MeasurableSpace.generateFrom {t : Set Ω | kT, s k = t}) hm' μ
                  theorem ProbabilityTheory.condIndep_iSup_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : ιMeasurableSpace Ω} (h_le : ∀ (i : ι), m i ) (h_indep : ProbabilityTheory.iCondIndep m' hm' m μ) {S : Set ι} {T : Set ι} (hST : Disjoint S T) :
                  ProbabilityTheory.CondIndep m' (iS, m i) (iT, m i) hm' μ
                  theorem ProbabilityTheory.condIndep_iSup_of_directed_le {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : ιMeasurableSpace Ω} (h_indep : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm' μ) (h_le : ∀ (i : ι), m i ) (h_le' : m₁ ) (hm : Directed (fun (x x_1 : MeasurableSpace Ω) => x x_1) m) :
                  ProbabilityTheory.CondIndep m' (⨆ (i : ι), m i) m₁ hm' μ
                  theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_lt {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [Preorder ι] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iCondIndepSet m' hm' s μ) (i : ι) :
                  theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [LinearOrder ι] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iCondIndepSet m' hm' s μ) (i : ι) {k : ι} (hk : i < k) :
                  theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le_nat {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hsm : ∀ (n : ), MeasurableSet (s n)) (hs : ProbabilityTheory.iCondIndepSet m' hm' s μ) (n : ) :
                  ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s (n + 1)}) (MeasurableSpace.generateFrom {t : Set Ω | kn, s k = t}) hm' μ
                  theorem ProbabilityTheory.condIndep_iSup_of_monotone {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [SemilatticeSup ι] {m : ιMeasurableSpace Ω} (h_indep : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm' μ) (h_le : ∀ (i : ι), m i ) (h_le' : m₁ ) (hm : Monotone m) :
                  ProbabilityTheory.CondIndep m' (⨆ (i : ι), m i) m₁ hm' μ
                  theorem ProbabilityTheory.condIndep_iSup_of_antitone {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [SemilatticeInf ι] {m : ιMeasurableSpace Ω} (h_indep : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm' μ) (h_le : ∀ (i : ι), m i ) (h_le' : m₁ ) (hm : Antitone m) :
                  ProbabilityTheory.CondIndep m' (⨆ (i : ι), m i) m₁ hm' μ
                  theorem ProbabilityTheory.iCondIndepSets.piiUnionInter_of_not_mem {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {π : ιSet (Set Ω)} {a : ι} {S : Finset ι} (hp_ind : ProbabilityTheory.iCondIndepSets m' hm' π μ) (haS : aS) :
                  theorem ProbabilityTheory.iCondIndepSets.iCondIndep {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (m : ιMeasurableSpace Ω) (h_le : ∀ (i : ι), m i ) (π : ιSet (Set Ω)) (h_pi : ∀ (n : ι), IsPiSystem (π n)) (h_generate : ∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)) (h_ind : ProbabilityTheory.iCondIndepSets m' hm' π μ) :

                  The σ-algebras generated by conditionally independent pi-systems are conditionally independent.

                  Conditional independence of measurable sets #

                  theorem ProbabilityTheory.CondIndepSets.condIndepSet_of_mem {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {s : Set Ω} {t : Set Ω} (S : Set (Set Ω)) (T : Set (Set Ω)) (hs : s S) (ht : t T) (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (h_indep : ProbabilityTheory.CondIndepSets m' hm' S T μ) :
                  theorem ProbabilityTheory.CondIndep.condIndepSet_of_measurableSet {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ) {s : Set Ω} {t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) :

                  Conditional independence of random variables #

                  theorem ProbabilityTheory.condIndepFun_iff_condexp_inter_preimage_eq_mul {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (hf : Measurable f) (hg : Measurable g) :
                  ProbabilityTheory.CondIndepFun m' hm' f g μ ∀ (s : Set β) (t : Set β'), MeasurableSet sMeasurableSet tMeasureTheory.condexp m' μ ((f ⁻¹' s g ⁻¹' t).indicator fun (ω : Ω) => 1) =ᵐ[μ] fun (ω : Ω) => MeasureTheory.condexp m' μ ((f ⁻¹' s).indicator fun (ω : Ω) => 1) ω * MeasureTheory.condexp m' μ ((g ⁻¹' t).indicator fun (ω : Ω) => 1) ω
                  theorem ProbabilityTheory.iCondIndepFun_iff_condexp_inter_preimage_eq_mul {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ιType u_5} (m : (x : ι) → MeasurableSpace (β x)) (f : (i : ι) → Ωβ i) (hf : ∀ (i : ι), Measurable (f i)) :
                  ProbabilityTheory.iCondIndepFun m' hm' m f μ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (iS, MeasurableSet (sets i))MeasureTheory.condexp m' μ ((iS, f i ⁻¹' sets i).indicator fun (ω : Ω) => 1) =ᵐ[μ] iS, MeasureTheory.condexp m' μ ((f i ⁻¹' sets i).indicator fun (ω : Ω) => 1)
                  theorem ProbabilityTheory.condIndepFun_iff_condIndepSet_preimage {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (hf : Measurable f) (hg : Measurable g) :
                  ProbabilityTheory.CondIndepFun m' hm' f g μ ∀ (s : Set β) (t : Set β'), MeasurableSet sMeasurableSet tProbabilityTheory.CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ
                  theorem ProbabilityTheory.CondIndepFun.symm {Ω : Type u_1} {β : Type u_3} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] :
                  ∀ {x : MeasurableSpace β} {f g : Ωβ}, ProbabilityTheory.CondIndepFun m' hm' f g μProbabilityTheory.CondIndepFun m' hm' g f μ
                  theorem ProbabilityTheory.CondIndepFun.comp {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ωβ} {g : Ωβ'} {γ : Type u_5} {γ' : Type u_6} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} {_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'} {φ : βγ} {ψ : β'γ'} (hfg : ProbabilityTheory.CondIndepFun m' hm' f g μ) (hφ : Measurable φ) (hψ : Measurable ψ) :
                  ProbabilityTheory.CondIndepFun m' hm' (φ f) (ψ g) μ
                  theorem ProbabilityTheory.CondIndepFun.neg_right {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ωβ} {g : Ωβ'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β'] [MeasurableNeg β'] (hfg : ProbabilityTheory.CondIndepFun m' hm' f g μ) :
                  theorem ProbabilityTheory.CondIndepFun.neg_left {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ωβ} {g : Ωβ'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β] [MeasurableNeg β] (hfg : ProbabilityTheory.CondIndepFun m' hm' f g μ) :
                  theorem ProbabilityTheory.iCondIndepFun.of_subsingleton {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ιType u_5} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} [Subsingleton ι] :
                  theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ιType u_6} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (S : Finset ι) (T : Finset ι) (hST : Disjoint S T) (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' m f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) :
                  ProbabilityTheory.CondIndepFun m' hm' (fun (a : Ω) (i : { x : ι // x S }) => f (i) a) (fun (a : Ω) (i : { x : ι // x T }) => f (i) a) μ

                  If f is a family of mutually conditionally independent random variables (iCondIndepFun m' hm' m f μ) and S, T are two disjoint finite index sets, then the tuple formed by f i for i ∈ S is conditionally independent of the tuple (f i)_i for i ∈ T.

                  theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_mk {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ιType u_6} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' m f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.CondIndepFun m' hm' (fun (a : Ω) => (f i a, f j a)) (f k) μ
                  theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_mk_prod_mk {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ιType u_5} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (h_indep : ProbabilityTheory.iCondIndepFun m' hm' m f μ) (hf : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i k) (hil : i l) (hjk : j k) (hjl : j l) :
                  ProbabilityTheory.CondIndepFun m' hm' (fun (a : Ω) => (f i a, f j a)) (fun (a : Ω) => (f k a, f l a)) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_add_left {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i + f j) (f k) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_mul_left {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i * f j) (f k) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_add_right {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i) (f j + f k) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_mul_right {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i) (f j * f k) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_add_add {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i k) (hil : i l) (hjk : j k) (hjl : j l) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i + f j) (f k + f l) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_mul_mul {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i k) (hil : i l) (hjk : j k) (hjl : j l) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i * f j) (f k * f l) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_sub_left {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i - f j) (f k) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_div_left {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i / f j) (f k) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_sub_right {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i) (f j - f k) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_div_right {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i) (f j / f k) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_sub_sub {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i k) (hil : i l) (hjk : j k) (hjl : j l) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i - f j) (f k - f l) μ
                  theorem ProbabilityTheory.iCondIndepFun.indepFun_div_div {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i k) (hil : i l) (hjk : j k) (hjl : j l) :
                  ProbabilityTheory.CondIndepFun m' hm' (f i / f j) (f k / f l) μ
                  theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_sum_of_not_mem {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : is) :
                  ProbabilityTheory.CondIndepFun m' hm' (js, f j) (f i) μ
                  theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_not_mem {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : ιΩβ} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : is) :
                  ProbabilityTheory.CondIndepFun m' hm' (js, f j) (f i) μ
                  theorem ProbabilityTheory.iCondIndepFun.condIndepFun_sum_range_succ {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : Ωβ} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ) => m) f μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
                  ProbabilityTheory.CondIndepFun m' hm' (jFinset.range n, f j) (f n) μ
                  theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_range_succ {Ω : Type u_1} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : Ωβ} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ) => m) f μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
                  ProbabilityTheory.CondIndepFun m' hm' (jFinset.range n, f j) (f n) μ
                  theorem ProbabilityTheory.iCondIndepSet.iCondIndepFun_indicator {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' : MeasurableSpace Ω} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' } {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [Zero β] [One β] {m : MeasurableSpace β} {s : ιSet Ω} (hs : ProbabilityTheory.iCondIndepSet m' hm' s μ) :
                  ProbabilityTheory.iCondIndepFun m' hm' (fun (_n : ι) => m) (fun (n : ι) => (s n).indicator fun ( : Ω) => 1) μ