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 in 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 Ω)) (κ : { x // x 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 in s, κ a (f i). It will be used for families of pi_systems.

Instances For
    def ProbabilityTheory.kernel.IndepSets {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (s1 : Set (Set Ω)) (s2 : Set (Set Ω)) (κ : { x // x 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₂)

    Instances For
      def ProbabilityTheory.kernel.iIndep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} (m : ιMeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (κ : { x // x 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.

      Instances For
        def ProbabilityTheory.kernel.Indep {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} (m₁ : MeasurableSpace Ω) (m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (κ : { x // x 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₂)

        Instances For
          def ProbabilityTheory.kernel.iIndepSet {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (s : ιSet Ω) (κ : { x // x 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.

          Instances For
            def ProbabilityTheory.kernel.IndepSet {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (s : Set Ω) (t : Set Ω) (κ : { x // x 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.

            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) (κ : { 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.

              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 : Ωγ) (κ : { x // x 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.

                Instances For
                  theorem ProbabilityTheory.kernel.IndepSets.symm {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} {u : Set ι} (hyp : ∀ (n : ι), n uProbabilityTheory.kernel.IndepSets (s n) s' κ) :
                  ProbabilityTheory.kernel.IndepSets (⋃ (n : ι) (_ : n u), 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} {u : Set ι} (h : n, n u ProbabilityTheory.kernel.IndepSets (s n) s' κ) :
                  ProbabilityTheory.kernel.IndepSets (⋂ (n : ι) (_ : n u), s n) s' κ
                  theorem ProbabilityTheory.kernel.indepSets_singleton_iff {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s : Set Ω} {t : Set Ω} {_mΩ : MeasurableSpace Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (hp1m : ∀ (s : Set Ω), s p1MeasurableSet s) (hp2m : ∀ (s : Set Ω), s p2MeasurableSet 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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.kernel.iIndepSet s κ) (S : Set ι) (T : Set ι) (hST : Disjoint S T) :
                  theorem ProbabilityTheory.kernel.indep_iSup_of_disjoint {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {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 (⨆ (i : ι) (_ : i S), m i) (⨆ (i : ι) (_ : i T), 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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] (h_indep : ∀ (i : ι), ProbabilityTheory.kernel.Indep (m i) m' κ) (h_le : ∀ (i : ι), m i m0) (h_le' : m' m0) (hm : Directed (fun x x_1 => x x_1) 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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [Preorder ι] [ProbabilityTheory.IsMarkovKernel κ] {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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [LinearOrder ι] [ProbabilityTheory.IsMarkovKernel κ] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.kernel.iIndepSet s κ) (i : ι) {k : ι} (hk : i < k) :
                  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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] (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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] (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 Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} {π : ιSet (Set Ω)} {a : ι} {S : Finset ι} (hp_ind : ProbabilityTheory.kernel.iIndepSets π κ) (haS : ¬a S) :
                  theorem ProbabilityTheory.kernel.iIndepSets.iIndep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] (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.indepSet_iff_measure_inter_eq_mul {α : Type u_1} {Ω : Type u_2} {s : Set Ω} {t : Set Ω} {_mα : MeasurableSpace α} {_m0 : MeasurableSpace Ω} (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (κ : { x // x ProbabilityTheory.kernel α Ω }) (μ : MeasureTheory.Measure α) [ProbabilityTheory.IsMarkovKernel κ] :
                  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} {s : Set Ω} {t : Set Ω} (S : Set (Set Ω)) (T : Set (Set Ω)) {_mα : MeasurableSpace α} {_m0 : MeasurableSpace Ω} (hs : s S) (ht : t T) (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (κ : { x // x ProbabilityTheory.kernel α Ω }) (μ : MeasureTheory.Measure α) [ProbabilityTheory.IsMarkovKernel κ] (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 Ω} {κ : { x // x 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 Ω} {κ : { x // x 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.iIndepFun_iff_measure_inter_preimage_eq_mul {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x 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)}, (∀ (i : ι), i SMeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, ↑(κ a) (⋂ (i : ι) (_ : i S), f i ⁻¹' sets i) = Finset.prod S fun i => ↑(κ a) (f i ⁻¹' sets i)
                  theorem ProbabilityTheory.kernel.indepFun_iff_indepSet_preimage {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [ProbabilityTheory.IsMarkovKernel κ] (hf : Measurable f) (hg : Measurable g) :
                  theorem ProbabilityTheory.kernel.IndepFun.symm {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} :
                  theorem ProbabilityTheory.kernel.IndepFun.ae_eq {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {f : Ωβ} {g : Ωβ} {f' : Ωβ} {g' : Ωβ} (hfg : ProbabilityTheory.kernel.IndepFun f g κ) (hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[MeasureTheory.Measure.ae (κ a)] f') (hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[MeasureTheory.Measure.ae (κ 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 Ω} {κ : { x // x 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.iIndepFun.indepFun_finset {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {ι : Type u_8} {β : ιType u_9} {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 => f (i) a) (fun a i => 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 {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {ι : Type u_8} {β : ιType u_9} {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.add {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {ι : Type u_8} {β : Type u_9} {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) :
                  theorem ProbabilityTheory.kernel.iIndepFun.mul {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {ι : Type u_8} {β : Type u_9} {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) :
                  theorem ProbabilityTheory.kernel.iIndepFun.indepFun_finset_sum_of_not_mem {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {ι : Type u_8} {β : Type u_9} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : ¬i s) :
                  theorem ProbabilityTheory.kernel.iIndepFun.indepFun_finset_prod_of_not_mem {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {ι : Type u_8} {β : Type u_9} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : ιΩβ} (hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : ¬i s) :
                  theorem ProbabilityTheory.kernel.iIndepFun.indepFun_sum_range_succ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {β : Type u_8} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : Ωβ} (hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
                  theorem ProbabilityTheory.kernel.iIndepFun.indepFun_prod_range_succ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsMarkovKernel κ] {β : Type u_8} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : Ωβ} (hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
                  theorem ProbabilityTheory.kernel.iIndepSet.iIndepFun_indicator {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : Type u_4} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : { x // x ProbabilityTheory.kernel α Ω }} {μ : MeasureTheory.Measure α} [Zero β] [One β] {m : MeasurableSpace β} {s : ιSet Ω} (hs : ProbabilityTheory.kernel.iIndepSet s κ) :
                  ProbabilityTheory.kernel.iIndepFun (fun _n => m) (fun n => Set.indicator (s n) fun => 1) κ