Documentation

Mathlib.Probability.Independence.Kernel

Independence with respect to a kernel and a measure #

A family of sets of sets π : ι → Set (Set Ω) is independent with respect to a kernel κ : Kernel α Ω and a measure μ on α 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 for μ-almost every a : α, κ a (⋂ i in s, f i) = ∏ i ∈ s, κ a (f i).

This notion of independence is a generalization of both independence and conditional independence. For conditional independence, κ is the conditional kernel ProbabilityTheory.condexpKernel and μ is the ambiant measure. For (non-conditional) independence, κ = Kernel.const Unit μ and the measure is the Dirac measure on Unit.

The main purpose of this file is to prove only once the properties that hold for both conditional and non-conditional independence.

Main definitions #

See the file Mathlib/Probability/Kernel/Basic.lean for a more detailed discussion of these definitions in the particular case of the usual independence notion.

Main statements #

def ProbabilityTheory.Kernel.iIndepSets {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (π : ιSet (Set Ω)) (κ : ProbabilityTheory.Kernel α Ω) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

A family of sets of sets π : ι → Set (Set Ω) is independent with respect to a kernel κ and 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 ∀ᵐ a ∂μ, κ a (⋂ i in s, f i) = ∏ i ∈ s, κ a (f i). It will be used for families of pi_systems.

Equations
Instances For
    def ProbabilityTheory.Kernel.IndepSets {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (s1 : Set (Set Ω)) (s2 : Set (Set Ω)) (κ : ProbabilityTheory.Kernel α Ω) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

    Two sets of sets s₁, s₂ are independent with respect to a kernel κ and a measure μ if for any sets t₁ ∈ s₁, t₂ ∈ s₂, then ∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a (t₁) * κ a (t₂)

    Equations
    Instances For
      def ProbabilityTheory.Kernel.iIndep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} (m : ιMeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (κ : ProbabilityTheory.Kernel α Ω) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

      A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a kernel κ and a measure μ if the family of sets of measurable sets they define is independent.

      Equations
      Instances For
        def ProbabilityTheory.Kernel.Indep {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} (m₁ : MeasurableSpace Ω) (m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (κ : ProbabilityTheory.Kernel α Ω) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

        Two measurable space structures (or σ-algebras) m₁, m₂ are independent with respect to a kernel κ and a measure μ if for any sets t₁ ∈ m₁, t₂ ∈ m₂, ∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a (t₁) * κ a (t₂)

        Equations
        Instances For
          def ProbabilityTheory.Kernel.iIndepSet {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (s : ιSet Ω) (κ : ProbabilityTheory.Kernel α Ω) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

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

          Equations
          Instances For
            def ProbabilityTheory.Kernel.IndepSet {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (s : Set Ω) (t : Set Ω) (κ : ProbabilityTheory.Kernel α Ω) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

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

            Equations
            Instances For
              def ProbabilityTheory.Kernel.iIndepFun {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {β : ιType u_4} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (κ : ProbabilityTheory.Kernel α Ω) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

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

              Equations
              Instances For
                def ProbabilityTheory.Kernel.IndepFun {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {β : Type u_4} {γ : Type u_5} {_mΩ : MeasurableSpace Ω} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ωβ) (g : Ωγ) (κ : ProbabilityTheory.Kernel α Ω) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

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

                Equations
                Instances For
                  @[simp]
                  theorem ProbabilityTheory.Kernel.iIndepSets_zero_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {π : ιSet (Set Ω)} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.indepSets_zero_right {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {s1 : Set (Set Ω)} {s2 : Set (Set Ω)} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.indepSets_zero_left {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure α} {s1 : Set (Set Ω)} {s2 : Set (Set Ω)} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.iIndep_zero_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.indep_zero_right {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.indep_zero_left {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.iIndepSet_zero_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {s : ιSet Ω} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.indepSet_zero_right {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {s : Set Ω} {t : Set Ω} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.indepSet_zero_left {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure α} {s : Set Ω} {t : Set Ω} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.iIndepFun_zero_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {β : ιType u_5} {m : (x : ι) → MeasurableSpace (β x)} {f : (x : ι) → Ωβ x} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.indepFun_zero_right {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {β : Type u_5} {γ : Type u_6} [MeasurableSpace β] [MeasurableSpace γ] {f : Ωβ} {g : Ωγ} :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.indepFun_zero_left {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure α} {β : Type u_5} {γ : Type u_6} [MeasurableSpace β] [MeasurableSpace γ] {f : Ωβ} {g : Ωγ} :
                  theorem ProbabilityTheory.Kernel.iIndepSets_congr {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ιSet (Set Ω)} (h : κ =ᵐ[μ] η) :
                  theorem ProbabilityTheory.Kernel.iIndepSets.congr {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ιSet (Set Ω)} (h : κ =ᵐ[μ] η) :

                  Alias of the forward direction of ProbabilityTheory.Kernel.iIndepSets_congr.

                  theorem ProbabilityTheory.Kernel.indepSets_congr {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s1 : Set (Set Ω)} {s2 : Set (Set Ω)} (h : κ =ᵐ[μ] η) :
                  theorem ProbabilityTheory.Kernel.IndepSets.congr {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s1 : Set (Set Ω)} {s2 : Set (Set Ω)} (h : κ =ᵐ[μ] η) :

                  Alias of the forward direction of ProbabilityTheory.Kernel.indepSets_congr.

                  theorem ProbabilityTheory.Kernel.iIndep_congr {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h : κ =ᵐ[μ] η) :
                  theorem ProbabilityTheory.Kernel.iIndep.congr {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h : κ =ᵐ[μ] η) :

                  Alias of the forward direction of ProbabilityTheory.Kernel.iIndep_congr.

                  theorem ProbabilityTheory.Kernel.indep_congr {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} (h : κ =ᵐ[μ] η) :
                  theorem ProbabilityTheory.Kernel.Indep.congr {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} (h : κ =ᵐ[μ] η) :

                  Alias of the forward direction of ProbabilityTheory.Kernel.indep_congr.

                  theorem ProbabilityTheory.Kernel.iIndepSet_congr {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ιSet Ω} (h : κ =ᵐ[μ] η) :
                  theorem ProbabilityTheory.Kernel.iIndepSet.congr {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ιSet Ω} (h : κ =ᵐ[μ] η) :

                  Alias of the forward direction of ProbabilityTheory.Kernel.iIndepSet_congr.

                  theorem ProbabilityTheory.Kernel.indepSet_congr {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : Set Ω} {t : Set Ω} (h : κ =ᵐ[μ] η) :
                  theorem ProbabilityTheory.Kernel.indepSet.congr {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : Set Ω} {t : Set Ω} (h : κ =ᵐ[μ] η) :

                  Alias of the forward direction of ProbabilityTheory.Kernel.indepSet_congr.

                  theorem ProbabilityTheory.Kernel.iIndepFun_congr {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ιType u_5} {m : (x : ι) → MeasurableSpace (β x)} {f : (x : ι) → Ωβ x} (h : κ =ᵐ[μ] η) :
                  theorem ProbabilityTheory.Kernel.iIndepFun.congr {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ιType u_5} {m : (x : ι) → MeasurableSpace (β x)} {f : (x : ι) → Ωβ x} (h : κ =ᵐ[μ] η) :

                  Alias of the forward direction of ProbabilityTheory.Kernel.iIndepFun_congr.

                  theorem ProbabilityTheory.Kernel.indepFun_congr {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_5} {γ : Type u_6} [MeasurableSpace β] [MeasurableSpace γ] {f : Ωβ} {g : Ωγ} (h : κ =ᵐ[μ] η) :
                  theorem ProbabilityTheory.Kernel.IndepFun.congr {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_5} {γ : Type u_6} [MeasurableSpace β] [MeasurableSpace γ] {f : Ωβ} {g : Ωγ} (h : κ =ᵐ[μ] η) :

                  Alias of the forward direction of ProbabilityTheory.Kernel.indepFun_congr.

                  theorem ProbabilityTheory.Kernel.iIndepSets.meas_biInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ιSet (Set Ω)} (h : ProbabilityTheory.Kernel.iIndepSets π κ μ) (s : Finset ι) {f : ιSet Ω} (hf : is, f i π i) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ is, f i) = is, (κ a) (f i)
                  theorem ProbabilityTheory.Kernel.iIndepSets.ae_isProbabilityMeasure {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ιSet (Set Ω)} (h : ProbabilityTheory.Kernel.iIndepSets π κ μ) :
                  ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
                  theorem ProbabilityTheory.Kernel.iIndepSets.meas_iInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ιSet (Set Ω)} {s : ιSet Ω} [Fintype ι] (h : ProbabilityTheory.Kernel.iIndepSets π κ μ) (hs : ∀ (i : ι), s i π i) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ (i : ι), s i) = i : ι, (κ a) (s i)
                  theorem ProbabilityTheory.Kernel.iIndep.iIndepSets' {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (hμ : ProbabilityTheory.Kernel.iIndep m κ μ) :
                  ProbabilityTheory.Kernel.iIndepSets (fun (x : ι) => {s : Set Ω | MeasurableSet s}) κ μ
                  theorem ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h : ProbabilityTheory.Kernel.iIndep m κ μ) :
                  ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
                  theorem ProbabilityTheory.Kernel.iIndep.meas_biInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ιSet Ω} {S : Finset ι} (hμ : ProbabilityTheory.Kernel.iIndep m κ μ) (hs : iS, MeasurableSet (s i)) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ iS, s i) = iS, (κ a) (s i)
                  theorem ProbabilityTheory.Kernel.iIndep.meas_iInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ιSet Ω} [Fintype ι] (h : ProbabilityTheory.Kernel.iIndep m κ μ) (hs : ∀ (i : ι), MeasurableSet (s i)) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ (i : ι), s i) = i : ι, (κ a) (s i)
                  theorem ProbabilityTheory.Kernel.iIndepFun.iIndep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ιType u_4} {mβ : (i : ι) → MeasurableSpace (β i)} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : (x : ι) → Ωβ x} (hf : ProbabilityTheory.Kernel.iIndepFun f κ μ) :
                  ProbabilityTheory.Kernel.iIndep (fun (x : ι) => MeasurableSpace.comap (f x) ( x)) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ιType u_4} {mβ : (i : ι) → MeasurableSpace (β i)} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : (x : ι) → Ωβ x} (h : ProbabilityTheory.Kernel.iIndepFun f κ μ) :
                  ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
                  theorem ProbabilityTheory.Kernel.iIndepFun.meas_biInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ιType u_4} {mβ : (i : ι) → MeasurableSpace (β i)} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ιSet Ω} {S : Finset ι} {f : (x : ι) → Ωβ x} (hf : ProbabilityTheory.Kernel.iIndepFun f κ μ) (hs : iS, MeasurableSet (s i)) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ iS, s i) = iS, (κ a) (s i)
                  theorem ProbabilityTheory.Kernel.iIndepFun.meas_iInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ιType u_4} {mβ : (i : ι) → MeasurableSpace (β i)} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ιSet Ω} {f : (x : ι) → Ωβ x} [Fintype ι] (hf : ProbabilityTheory.Kernel.iIndepFun f κ μ) (hs : ∀ (i : ι), MeasurableSet (s i)) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ (i : ι), s i) = i : ι, (κ a) (s i)
                  theorem ProbabilityTheory.Kernel.IndepFun.meas_inter {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_5} {γ : Type u_6} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] {f : Ωβ} {g : Ωγ} (hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ) {s : Set Ω} {t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (s t) = (κ a) s * (κ a) t
                  theorem ProbabilityTheory.Kernel.IndepSets.symm {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} (h : ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ) :
                  theorem ProbabilityTheory.Kernel.Indep.symm {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h : ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ) :
                  theorem ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_left {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h_indep : ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ) (h31 : s₃ s₁) :
                  theorem ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_right {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h_indep : ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ) (h32 : s₃ s₂) :
                  theorem ProbabilityTheory.Kernel.indep_of_indep_of_le_left {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m₃ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h_indep : ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ) (h31 : m₃ m₁) :
                  theorem ProbabilityTheory.Kernel.indep_of_indep_of_le_right {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m₃ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h_indep : ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ) (h32 : m₃ m₂) :
                  theorem ProbabilityTheory.Kernel.IndepSets.union {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h₁ : ProbabilityTheory.Kernel.IndepSets s₁ s' κ μ) (h₂ : ProbabilityTheory.Kernel.IndepSets s₂ s' κ μ) :
                  @[simp]
                  theorem ProbabilityTheory.Kernel.IndepSets.union_iff {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} :
                  theorem ProbabilityTheory.Kernel.IndepSets.iUnion {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (hyp : ∀ (n : ι), ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ) :
                  ProbabilityTheory.Kernel.IndepSets (⋃ (n : ι), s n) s' κ μ
                  theorem ProbabilityTheory.Kernel.IndepSets.bUnion {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {u : Set ι} (hyp : nu, ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ) :
                  ProbabilityTheory.Kernel.IndepSets (⋃ nu, s n) s' κ μ
                  theorem ProbabilityTheory.Kernel.IndepSets.inter {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ : Set (Set Ω)} {s' : Set (Set Ω)} (s₂ : Set (Set Ω)) {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h₁ : ProbabilityTheory.Kernel.IndepSets s₁ s' κ μ) :
                  theorem ProbabilityTheory.Kernel.IndepSets.iInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h : ∃ (n : ι), ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ) :
                  ProbabilityTheory.Kernel.IndepSets (⋂ (n : ι), s n) s' κ μ
                  theorem ProbabilityTheory.Kernel.IndepSets.bInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {u : Set ι} (h : nu, ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ) :
                  ProbabilityTheory.Kernel.IndepSets (⋂ nu, s n) s' κ μ
                  theorem ProbabilityTheory.Kernel.iIndep_comap_mem_iff {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {f : ιSet Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} :
                  theorem ProbabilityTheory.Kernel.iIndepSets_singleton_iff {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ιSet Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} :
                  ProbabilityTheory.Kernel.iIndepSets (fun (i : ι) => {s i}) κ μ ∀ (S : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ iS, s i) = iS, (κ a) (s i)
                  theorem ProbabilityTheory.Kernel.indepSets_singleton_iff {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s : Set Ω} {t : Set Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} :
                  ProbabilityTheory.Kernel.IndepSets {s} {t} κ μ ∀ᵐ (a : α) ∂μ, (κ a) (s t) = (κ a) s * (κ a) t

                  Deducing Indep from iIndep #

                  theorem ProbabilityTheory.Kernel.iIndepSets.indepSets {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ιSet (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h_indep : ProbabilityTheory.Kernel.iIndepSets s κ μ) {i : ι} {j : ι} (hij : i j) :
                  theorem ProbabilityTheory.Kernel.iIndep.indep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h_indep : ProbabilityTheory.Kernel.iIndep m κ μ) {i : ι} {j : ι} (hij : i j) :
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ιType u_4} {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ωβ i} (hf_Indep : ProbabilityTheory.Kernel.iIndepFun m f κ μ) {i : ι} {j : ι} (hij : i j) :

                  π-system lemma #

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

                  Independence of measurable space structures implies independence of generating π-systems #

                  theorem ProbabilityTheory.Kernel.iIndep.iIndepSets {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {m : ιMeasurableSpace Ω} {s : ιSet (Set Ω)} (hms : ∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)) (h_indep : ProbabilityTheory.Kernel.iIndep m κ μ) :

                  Independence of generating π-systems implies independence of measurable space structures #

                  theorem ProbabilityTheory.Kernel.IndepSets.indep_aux {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₂ : MeasurableSpace Ω} {m : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (h2 : m₂ m) (hp2 : IsPiSystem p2) (hpm2 : m₂ = MeasurableSpace.generateFrom p2) (hyp : ProbabilityTheory.Kernel.IndepSets p1 p2 κ μ) {t1 : Set Ω} {t2 : Set Ω} (ht1 : t1 p1) (ht1m : MeasurableSet t1) (ht2m : MeasurableSet t2) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (t1 t2) = (κ a) t1 * (κ a) t2
                  theorem ProbabilityTheory.Kernel.IndepSets.indep {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m1 : MeasurableSpace Ω} {m2 : MeasurableSpace Ω} {m : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (h1 : m1 m) (h2 : m2 m) (hp1 : IsPiSystem p1) (hp2 : IsPiSystem p2) (hpm1 : m1 = MeasurableSpace.generateFrom p1) (hpm2 : m2 = MeasurableSpace.generateFrom p2) (hyp : ProbabilityTheory.Kernel.IndepSets p1 p2 κ μ) :

                  The measurable space structures generated by independent pi-systems are independent.

                  theorem ProbabilityTheory.Kernel.IndepSets.indep' {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (hp1m : sp1, MeasurableSet s) (hp2m : sp2, MeasurableSet s) (hp1 : IsPiSystem p1) (hp2 : IsPiSystem p2) (hyp : ProbabilityTheory.Kernel.IndepSets p1 p2 κ μ) :
                  theorem ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ιSet (Set Ω)} {S : Set ι} {T : Set ι} (h_indep : ProbabilityTheory.Kernel.iIndepSets s κ μ) (hST : Disjoint S T) :
                  theorem ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.Kernel.iIndepSet s κ μ) (S : Set ι) (T : Set ι) (hST : Disjoint S T) :
                  ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {t : Set Ω | nS, s n = t}) (MeasurableSpace.generateFrom {t : Set Ω | kT, s k = t}) κ μ
                  theorem ProbabilityTheory.Kernel.indep_iSup_of_disjoint {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {m : ιMeasurableSpace Ω} (h_le : ∀ (i : ι), m i _mΩ) (h_indep : ProbabilityTheory.Kernel.iIndep m κ μ) {S : Set ι} {T : Set ι} (hST : Disjoint S T) :
                  ProbabilityTheory.Kernel.Indep (⨆ iS, m i) (⨆ iT, m i) κ μ
                  theorem ProbabilityTheory.Kernel.indep_iSup_of_directed_le {α : Type u_1} {ι : Type u_3} {_mα : MeasurableSpace α} {Ω : Type u_4} {m : ιMeasurableSpace Ω} {m' : MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] (h_indep : ∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ) (h_le : ∀ (i : ι), m i m0) (h_le' : m' m0) (hm : Directed (fun (x1 x2 : MeasurableSpace Ω) => x1 x2) m) :
                  ProbabilityTheory.Kernel.Indep (⨆ (i : ι), m i) m' κ μ
                  theorem ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_lt {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [Preorder ι] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.Kernel.iIndepSet s κ μ) (i : ι) :
                  theorem ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [LinearOrder ι] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.Kernel.iIndepSet s κ μ) (i : ι) {k : ι} (hk : i < k) :
                  theorem ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le_nat {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : Set Ω} (hsm : ∀ (n : ), MeasurableSet (s n)) (hs : ProbabilityTheory.Kernel.iIndepSet s κ μ) (n : ) :
                  theorem ProbabilityTheory.Kernel.indep_iSup_of_monotone {α : Type u_1} {ι : Type u_3} {_mα : MeasurableSpace α} [SemilatticeSup ι] {Ω : Type u_4} {m : ιMeasurableSpace Ω} {m' : MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] (h_indep : ∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ) (h_le : ∀ (i : ι), m i m0) (h_le' : m' m0) (hm : Monotone m) :
                  ProbabilityTheory.Kernel.Indep (⨆ (i : ι), m i) m' κ μ
                  theorem ProbabilityTheory.Kernel.indep_iSup_of_antitone {α : Type u_1} {ι : Type u_3} {_mα : MeasurableSpace α} [SemilatticeInf ι] {Ω : Type u_4} {m : ιMeasurableSpace Ω} {m' : MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] (h_indep : ∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ) (h_le : ∀ (i : ι), m i m0) (h_le' : m' m0) (hm : Antitone m) :
                  ProbabilityTheory.Kernel.Indep (⨆ (i : ι), m i) m' κ μ
                  theorem ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_not_mem {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ιSet (Set Ω)} {a : ι} {S : Finset ι} (hp_ind : ProbabilityTheory.Kernel.iIndepSets π κ μ) (haS : aS) :
                  theorem ProbabilityTheory.Kernel.iIndepSets.iIndep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (m : ιMeasurableSpace Ω) (h_le : ∀ (i : ι), m i _mΩ) (π : ιSet (Set Ω)) (h_pi : ∀ (n : ι), IsPiSystem (π n)) (h_generate : ∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)) (h_ind : ProbabilityTheory.Kernel.iIndepSets π κ μ) :

                  The measurable space structures generated by independent pi-systems are independent.

                  Independence of measurable sets #

                  We prove the following equivalences on IndepSet, for measurable sets s, t.

                  theorem ProbabilityTheory.Kernel.iIndepSet_iff_iIndepSets_singleton {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : ιSet Ω} (hf : ∀ (i : ι), MeasurableSet (f i)) :
                  theorem ProbabilityTheory.Kernel.iIndepSet.meas_biInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : ιSet Ω} (h : ProbabilityTheory.Kernel.iIndepSet f κ μ) (s : Finset ι) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ is, f i) = is, (κ a) (f i)
                  theorem ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : ιSet Ω} (hf : ∀ (i : ι), MeasurableSet (f i)) :
                  ProbabilityTheory.Kernel.iIndepSet f κ μ ∀ (s : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ is, f i) = is, (κ a) (f i)
                  theorem ProbabilityTheory.Kernel.iIndepSets.iIndepSet_of_mem {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ιSet (Set Ω)} {f : ιSet Ω} (hfπ : ∀ (i : ι), f i π i) (hf : ∀ (i : ι), MeasurableSet (f i)) (hπ : ProbabilityTheory.Kernel.iIndepSets π κ μ) :
                  theorem ProbabilityTheory.Kernel.indepSet_iff_measure_inter_eq_mul {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s : Set Ω} {t : Set Ω} {_m0 : MeasurableSpace Ω} (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α) [ProbabilityTheory.IsZeroOrMarkovKernel κ] :
                  ProbabilityTheory.Kernel.IndepSet s t κ μ ∀ᵐ (a : α) ∂μ, (κ a) (s t) = (κ a) s * (κ a) t
                  theorem ProbabilityTheory.Kernel.IndepSet.measure_inter_eq_mul {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s : Set Ω} {t : Set Ω} {_m0 : MeasurableSpace Ω} (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α) (h : ProbabilityTheory.Kernel.IndepSet s t κ μ) :
                  ∀ᵐ (a : α) ∂μ, (κ a) (s t) = (κ a) s * (κ a) t
                  theorem ProbabilityTheory.Kernel.IndepSets.indepSet_of_mem {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s : Set Ω} {t : Set Ω} (S : Set (Set Ω)) (T : Set (Set Ω)) {_m0 : MeasurableSpace Ω} (hs : s S) (ht : t T) (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (h_indep : ProbabilityTheory.Kernel.IndepSets S T κ μ) :
                  theorem ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (h_indep : ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ) {s : Set Ω} {t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) :

                  Independence of random variables #

                  theorem ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} :
                  ProbabilityTheory.Kernel.IndepFun f g κ μ ∀ (s : Set β) (t : Set β'), MeasurableSet sMeasurableSet t∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
                  theorem ProbabilityTheory.Kernel.IndepFun.measure_inter_preimage_eq_mul {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} :
                  ProbabilityTheory.Kernel.IndepFun f g κ μ∀ (s : Set β) (t : Set β'), MeasurableSet sMeasurableSet t∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)

                  Alias of the forward direction of ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul.

                  theorem ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {ι : Type u_8} {β : ιType u_9} (m : (x : ι) → MeasurableSpace (β x)) (f : (i : ι) → Ωβ i) :
                  ProbabilityTheory.Kernel.iIndepFun m f κ μ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ iS, MeasurableSet (sets i))∀ᵐ (a : α) ∂μ, (κ a) (⋂ iS, f i ⁻¹' sets i) = iS, (κ a) (f i ⁻¹' sets i)
                  theorem ProbabilityTheory.Kernel.iIndepFun.measure_inter_preimage_eq_mul {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {ι : Type u_8} {β : ιType u_9} (m : (x : ι) → MeasurableSpace (β x)) (f : (i : ι) → Ωβ i) :
                  ProbabilityTheory.Kernel.iIndepFun m f κ μ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ iS, MeasurableSet (sets i))∀ᵐ (a : α) ∂μ, (κ a) (⋂ iS, f i ⁻¹' sets i) = iS, (κ a) (f i ⁻¹' sets i)

                  Alias of the forward direction of ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul.

                  theorem ProbabilityTheory.Kernel.indepFun_iff_indepSet_preimage {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [ProbabilityTheory.IsZeroOrMarkovKernel κ] (hf : Measurable f) (hg : Measurable g) :
                  theorem ProbabilityTheory.Kernel.IndepFun.symm {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ωβ} {g : Ωβ'} :
                  theorem ProbabilityTheory.Kernel.IndepFun.ae_eq {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {f' : Ωβ} {g' : Ωβ'} (hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ) (hf : ∀ᵐ (a : α) ∂μ, f =ᵐ[κ a] f') (hg : ∀ᵐ (a : α) ∂μ, g =ᵐ[κ a] g') :
                  theorem ProbabilityTheory.Kernel.IndepFun.comp {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {γ : Type u_6} {γ' : Type u_7} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {mγ : MeasurableSpace γ} {mγ' : MeasurableSpace γ'} {φ : βγ} {ψ : β'γ'} (hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ) (hφ : Measurable φ) (hψ : Measurable ψ) :
                  theorem ProbabilityTheory.Kernel.IndepFun.neg_right {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ωβ} {g : Ωβ'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β'] [MeasurableNeg β'] (hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ) :
                  theorem ProbabilityTheory.Kernel.IndepFun.neg_left {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ωβ} {g : Ωβ'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β] [MeasurableNeg β] (hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ) :
                  theorem ProbabilityTheory.Kernel.iIndepFun.of_subsingleton {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ιType u_8} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} [ProbabilityTheory.IsMarkovKernel κ] [Subsingleton ι] :
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ιType u_8} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (S : Finset ι) (T : Finset ι) (hST : Disjoint S T) (hf_Indep : ProbabilityTheory.Kernel.iIndepFun m f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) :
                  ProbabilityTheory.Kernel.IndepFun (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 independent random variables (iIndepFun m f μ) and S, T are two disjoint finite index sets, then the tuple formed by f i for i ∈ S is independent of the tuple (f i)_i for i ∈ T.

                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ιType u_8} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (hf_Indep : ProbabilityTheory.Kernel.iIndepFun m f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.Kernel.IndepFun (fun (a : Ω) => (f i a, f j a)) (f k) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk_prod_mk {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ιType u_8} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (hf_indep : ProbabilityTheory.Kernel.iIndepFun 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.Kernel.IndepFun (fun (a : Ω) => (f i a, f j a)) (fun (a : Ω) => (f k a, f l a)) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.Kernel.IndepFun (f i + f j) (f k) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.Kernel.IndepFun (f i * f j) (f k) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_add_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.Kernel.IndepFun (f i) (f j + f k) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.Kernel.IndepFun (f i) (f j * f k) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_add_add {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (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.Kernel.IndepFun (f i + f j) (f k + f l) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (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.Kernel.IndepFun (f i * f j) (f k * f l) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_left {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.Kernel.IndepFun (f i - f j) (f k) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.Kernel.IndepFun (f i / f j) (f k) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.Kernel.IndepFun (f i) (f j - f k) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.Kernel.IndepFun (f i) (f j / f k) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_sub {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (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.Kernel.IndepFun (f i - f j) (f k - f l) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.Kernel.iIndepFun (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.Kernel.IndepFun (f i / f j) (f k / f l) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_not_mem {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : is) :
                  ProbabilityTheory.Kernel.IndepFun (∑ js, f j) (f i) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_not_mem {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : ιΩβ} (hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : is) :
                  ProbabilityTheory.Kernel.IndepFun (∏ js, f j) (f i) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_sum_range_succ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : Ωβ} (hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ) => m) f κ μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
                  ProbabilityTheory.Kernel.IndepFun (∑ jFinset.range n, f j) (f n) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : Ωβ} (hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ) => m) f κ μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
                  ProbabilityTheory.Kernel.IndepFun (∏ jFinset.range n, f j) (f n) κ μ
                  theorem ProbabilityTheory.Kernel.iIndepSet.iIndepFun_indicator {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : Type u_4} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [Zero β] [One β] {m : MeasurableSpace β} {s : ιSet Ω} (hs : ProbabilityTheory.Kernel.iIndepSet s κ μ) :
                  ProbabilityTheory.Kernel.iIndepFun (fun (_n : ι) => m) (fun (n : ι) => (s n).indicator fun ( : Ω) => 1) κ μ