Documentation

Mathlib.Probability.Independence.Basic

Independence of sets of sets and measure spaces (σ-algebras) #

Main statements #

Implementation notes #

The definitions of independence in this file are a particular case of independence with respect to a kernel and a measure, as defined in the file Kernel.lean.

We provide four definitions of 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 IndepFun is the version of iIndepFun for two functions.

The definition of independence for iIndepSets uses finite sets (Finset). See ProbabilityTheory.Kernel.iIndepSets. An alternative and equivalent way of defining independence would have been to use countable sets.

Most of the definitions and lemmas in this file list all variables instead of using the variable keyword at the beginning of a section, for example lemma Indep.symm {Ω} {m₁ m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : measure Ω} ... . This is intentional, to be able to control the order of the MeasurableSpace variables. Indeed when defining μ in the example above, the measurable space used is the last one defined, here {_mΩ : MeasurableSpace Ω}, and not m₁ or m₂.

References #

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

A family of sets of sets π : ι → Set (Set Ω) is independent 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) = ∏ i ∈ s, μ (f i) . It will be used for families of pi_systems.

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

    Two sets of sets s₁, s₂ are independent with respect to a measure μ if for any sets t₁ ∈ p₁, t₂ ∈ s₂, then μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)

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

      A family of measurable space structures (i.e. of σ-algebras) is independent 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 independent 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) = ∏ i ∈ s, μ (f i).

      Equations
      Instances For

        Two measurable space structures (or σ-algebras) m₁, m₂ are independent with respect to a measure μ (defined on a third σ-algebra) if for any sets t₁ ∈ m₁, t₂ ∈ m₂, μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)

        Equations
        Instances For
          def ProbabilityTheory.iIndepSet {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} (s : ιSet Ω) (μ : 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.IndepSet {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} (s : Set Ω) (t : Set Ω) (μ : 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.iIndepFun {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {β : ιType u_6} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (μ : 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.IndepFun {Ω : Type u_1} {β : Type u_6} {γ : Type u_7} {_mΩ : MeasurableSpace Ω} [MeasurableSpace β] [MeasurableSpace γ] (f : Ωβ) (g : Ωγ) (μ : 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
                  theorem ProbabilityTheory.iIndepSets_iff {Ω : Type u_1} {ι : Type u_2} :
                  ∀ {x : MeasurableSpace Ω} (π : ιSet (Set Ω)) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.iIndepSets π μ ∀ (s : Finset ι) {f : ιSet Ω}, (∀ is, f i π i)μ (⋂ is, f i) = is, μ (f i)
                  theorem ProbabilityTheory.iIndepSets.meas_biInter {Ω : Type u_1} {ι : Type u_2} {π : ιSet (Set Ω)} :
                  ∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}, ProbabilityTheory.iIndepSets π μ∀ (s : Finset ι) {f : ιSet Ω}, (∀ is, f i π i)μ (⋂ is, f i) = is, μ (f i)
                  theorem ProbabilityTheory.iIndepSets.meas_iInter {Ω : Type u_1} {ι : Type u_2} {π : ιSet (Set Ω)} :
                  ∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet Ω} [inst : Fintype ι], ProbabilityTheory.iIndepSets π μ(∀ (i : ι), s i π i)μ (⋂ (i : ι), s i) = i : ι, μ (s i)
                  theorem ProbabilityTheory.IndepSets_iff {Ω : Type u_1} :
                  ∀ {x : MeasurableSpace Ω} (s1 s2 : Set (Set Ω)) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.IndepSets s1 s2 μ ∀ (t1 t2 : Set Ω), t1 s1t2 s2μ (t1 t2) = μ t1 * μ t2
                  theorem ProbabilityTheory.iIndep_iff_iIndepSets {Ω : Type u_1} {ι : Type u_2} (m : ιMeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) :
                  theorem ProbabilityTheory.iIndep.iIndepSets' {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} :
                  ∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}, ProbabilityTheory.iIndep m μProbabilityTheory.iIndepSets (fun (x : ι) => {s : Set Ω | MeasurableSet s}) μ
                  theorem ProbabilityTheory.iIndep_iff {Ω : Type u_1} {ι : Type u_2} (m : ιMeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) :
                  ProbabilityTheory.iIndep m μ ∀ (s : Finset ι) {f : ιSet Ω}, (∀ is, MeasurableSet (f i))μ (⋂ is, f i) = is, μ (f i)
                  theorem ProbabilityTheory.iIndep.meas_biInter {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} :
                  ∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Finset ι} {s : ιSet Ω}, ProbabilityTheory.iIndep m μ(∀ iS, MeasurableSet (s i))μ (⋂ iS, s i) = iS, μ (s i)
                  theorem ProbabilityTheory.iIndep.meas_iInter {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} :
                  ∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet Ω} [inst : Fintype ι], ProbabilityTheory.iIndep m μ(∀ (i : ι), MeasurableSet (s i))μ (⋂ (i : ι), s i) = i : ι, μ (s i)
                  theorem ProbabilityTheory.Indep_iff {Ω : Type u_1} (m₁ : MeasurableSpace Ω) (m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) :
                  ProbabilityTheory.Indep m₁ m₂ μ ∀ (t1 t2 : Set Ω), MeasurableSet t1MeasurableSet t2μ (t1 t2) = μ t1 * μ t2
                  theorem ProbabilityTheory.iIndepSet_iff {Ω : Type u_1} {ι : Type u_2} :
                  ∀ {x : MeasurableSpace Ω} (s : ιSet Ω) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.iIndepSet s μ ∀ (s' : Finset ι) {f : ιSet Ω}, (∀ is', MeasurableSet (f i))μ (⋂ is', f i) = is', μ (f i)
                  theorem ProbabilityTheory.IndepSet_iff {Ω : Type u_1} :
                  ∀ {x : MeasurableSpace Ω} (s t : Set Ω) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.IndepSet s t μ ∀ (t1 t2 : Set Ω), MeasurableSet t1MeasurableSet t2μ (t1 t2) = μ t1 * μ t2
                  theorem ProbabilityTheory.iIndepFun_iff_iIndep {Ω : Type u_1} {ι : Type u_2} :
                  ∀ {x : MeasurableSpace Ω} {β : ιType u_6} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.iIndepFun m f μ ProbabilityTheory.iIndep (fun (x : ι) => MeasurableSpace.comap (f x) (m x)) μ
                  theorem ProbabilityTheory.iIndepFun.iIndep {Ω : Type u_1} {ι : Type u_2} {κ : ιType u_5} :
                  ∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ωκ x}, ProbabilityTheory.iIndepFun m f μProbabilityTheory.iIndep (fun (x : ι) => MeasurableSpace.comap (f x) (m x)) μ
                  theorem ProbabilityTheory.iIndepFun_iff {Ω : Type u_1} {ι : Type u_2} :
                  ∀ {x : MeasurableSpace Ω} {β : ιType u_6} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.iIndepFun m f μ ∀ (s : Finset ι) {f' : ιSet Ω}, (∀ is, MeasurableSet (f' i))μ (⋂ is, f' i) = is, μ (f' i)
                  theorem ProbabilityTheory.iIndepFun.meas_biInter {Ω : Type u_1} {ι : Type u_2} {κ : ιType u_5} :
                  ∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Finset ι} {s : ιSet Ω} {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ωκ x}, ProbabilityTheory.iIndepFun m f μ(∀ iS, MeasurableSet (s i))μ (⋂ iS, s i) = iS, μ (s i)
                  theorem ProbabilityTheory.iIndepFun.meas_iInter {Ω : Type u_1} {ι : Type u_2} {κ : ιType u_5} :
                  ∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet Ω} [inst : Fintype ι] {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ωκ x}, ProbabilityTheory.iIndepFun m f μ(∀ (i : ι), MeasurableSet (s i))μ (⋂ (i : ι), s i) = i : ι, μ (s i)
                  theorem ProbabilityTheory.IndepFun_iff_Indep {Ω : Type u_1} {β : Type u_3} {γ : Type u_4} :
                  ∀ {x : MeasurableSpace Ω} [ : MeasurableSpace β] [ : MeasurableSpace γ] (f : Ωβ) (g : Ωγ) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.IndepFun f g μ ProbabilityTheory.Indep (MeasurableSpace.comap f ) (MeasurableSpace.comap g ) μ
                  theorem ProbabilityTheory.IndepFun_iff {Ω : Type u_1} :
                  ∀ {x : MeasurableSpace Ω} {β : Type u_6} {γ : Type u_7} [ : MeasurableSpace β] [ : MeasurableSpace γ] (f : Ωβ) (g : Ωγ) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.IndepFun f g μ ∀ (t1 t2 : Set Ω), MeasurableSet t1MeasurableSet t2μ (t1 t2) = μ t1 * μ t2
                  theorem ProbabilityTheory.IndepFun.meas_inter {Ω : Type u_1} {β : Type u_3} {γ : Type u_4} :
                  ∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [ : MeasurableSpace β] [ : MeasurableSpace γ] {f : Ωβ} {g : Ωγ}, ProbabilityTheory.IndepFun f g μ∀ {s t : Set Ω}, MeasurableSet sMeasurableSet tμ (s t) = μ s * μ t
                  theorem ProbabilityTheory.IndepSets.symm {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} (h : ProbabilityTheory.IndepSets s₁ s₂ μ) :
                  theorem ProbabilityTheory.Indep.symm {Ω : Type u_1} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (h : ProbabilityTheory.Indep m₁ m₂ μ) :
                  theorem ProbabilityTheory.indepSets_of_indepSets_of_le_left {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} (h_indep : ProbabilityTheory.IndepSets s₁ s₂ μ) (h31 : s₃ s₁) :
                  theorem ProbabilityTheory.indepSets_of_indepSets_of_le_right {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} (h_indep : ProbabilityTheory.IndepSets s₁ s₂ μ) (h32 : s₃ s₂) :
                  theorem ProbabilityTheory.indep_of_indep_of_le_left {Ω : Type u_1} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m₃ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (h_indep : ProbabilityTheory.Indep m₁ m₂ μ) (h31 : m₃ m₁) :
                  theorem ProbabilityTheory.indep_of_indep_of_le_right {Ω : Type u_1} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m₃ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (h_indep : ProbabilityTheory.Indep m₁ m₂ μ) (h32 : m₃ m₂) :
                  theorem ProbabilityTheory.IndepSets.union {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} (h₁ : ProbabilityTheory.IndepSets s₁ s' μ) (h₂ : ProbabilityTheory.IndepSets s₂ s' μ) :
                  @[simp]
                  theorem ProbabilityTheory.IndepSets.union_iff {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} :
                  theorem ProbabilityTheory.IndepSets.iUnion {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet (Set Ω)} {s' : Set (Set Ω)} (hyp : ∀ (n : ι), ProbabilityTheory.IndepSets (s n) s' μ) :
                  ProbabilityTheory.IndepSets (⋃ (n : ι), s n) s' μ
                  theorem ProbabilityTheory.IndepSets.bUnion {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (hyp : nu, ProbabilityTheory.IndepSets (s n) s' μ) :
                  ProbabilityTheory.IndepSets (⋃ nu, s n) s' μ
                  theorem ProbabilityTheory.IndepSets.inter {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ : Set (Set Ω)} {s' : Set (Set Ω)} (s₂ : Set (Set Ω)) (h₁ : ProbabilityTheory.IndepSets s₁ s' μ) :
                  theorem ProbabilityTheory.IndepSets.iInter {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet (Set Ω)} {s' : Set (Set Ω)} (h : ∃ (n : ι), ProbabilityTheory.IndepSets (s n) s' μ) :
                  ProbabilityTheory.IndepSets (⋂ (n : ι), s n) s' μ
                  theorem ProbabilityTheory.IndepSets.bInter {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (h : nu, ProbabilityTheory.IndepSets (s n) s' μ) :
                  ProbabilityTheory.IndepSets (⋂ nu, s n) s' μ
                  theorem ProbabilityTheory.indepSets_singleton_iff {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} {t : Set Ω} :
                  ProbabilityTheory.IndepSets {s} {t} μ μ (s t) = μ s * μ t

                  Deducing Indep from iIndep #

                  theorem ProbabilityTheory.iIndepSets.indepSets {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet (Set Ω)} (h_indep : ProbabilityTheory.iIndepSets s μ) {i : ι} {j : ι} (hij : i j) :
                  theorem ProbabilityTheory.iIndep.indep {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (h_indep : ProbabilityTheory.iIndep m μ) {i : ι} {j : ι} (hij : i j) :
                  theorem ProbabilityTheory.iIndepFun.indepFun {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ιType u_6} {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ωβ i} (hf_Indep : ProbabilityTheory.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.iIndep.iIndepSets {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet (Set Ω)} (hms : ∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)) (h_indep : ProbabilityTheory.iIndep m μ) :

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

                  theorem ProbabilityTheory.IndepSets.indep {Ω : Type u_1} {m1 : MeasurableSpace Ω} {m2 : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {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.IndepSets p1 p2 μ) :
                  theorem ProbabilityTheory.indepSets_piiUnionInter_of_disjoint {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet (Set Ω)} {S : Set ι} {T : Set ι} (h_indep : ProbabilityTheory.iIndepSets s μ) (hST : Disjoint S T) :
                  theorem ProbabilityTheory.iIndepSet.indep_generateFrom_of_disjoint {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iIndepSet s μ) (S : Set ι) (T : Set ι) (hST : Disjoint S T) :
                  ProbabilityTheory.Indep (MeasurableSpace.generateFrom {t : Set Ω | nS, s n = t}) (MeasurableSpace.generateFrom {t : Set Ω | kT, s k = t}) μ
                  theorem ProbabilityTheory.indep_iSup_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (h_le : ∀ (i : ι), m i _mΩ) (h_indep : ProbabilityTheory.iIndep m μ) {S : Set ι} {T : Set ι} (hST : Disjoint S T) :
                  ProbabilityTheory.Indep (⨆ iS, m i) (⨆ iT, m i) μ
                  theorem ProbabilityTheory.indep_iSup_of_directed_le {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} {m1 : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (h_indep : ∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) (h_le : ∀ (i : ι), m i _mΩ) (h_le' : m1 _mΩ) (hm : Directed (fun (x1 x2 : MeasurableSpace Ω) => x1 x2) m) :
                  ProbabilityTheory.Indep (⨆ (i : ι), m i) m1 μ
                  theorem ProbabilityTheory.iIndepSet.indep_generateFrom_lt {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Preorder ι] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iIndepSet s μ) (i : ι) :
                  theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [LinearOrder ι] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iIndepSet s μ) (i : ι) {k : ι} (hk : i < k) :
                  theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le_nat {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} (hsm : ∀ (n : ), MeasurableSet (s n)) (hs : ProbabilityTheory.iIndepSet s μ) (n : ) :
                  theorem ProbabilityTheory.indep_iSup_of_monotone {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} {m1 : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (h_indep : ∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) (h_le : ∀ (i : ι), m i _mΩ) (h_le' : m1 _mΩ) (hm : Monotone m) :
                  ProbabilityTheory.Indep (⨆ (i : ι), m i) m1 μ
                  theorem ProbabilityTheory.indep_iSup_of_antitone {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} {m1 : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (h_indep : ∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) (h_le : ∀ (i : ι), m i _mΩ) (h_le' : m1 _mΩ) (hm : Antitone m) :
                  ProbabilityTheory.Indep (⨆ (i : ι), m i) m1 μ
                  theorem ProbabilityTheory.iIndepSets.piiUnionInter_of_not_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {π : ιSet (Set Ω)} {a : ι} {S : Finset ι} (hp_ind : ProbabilityTheory.iIndepSets π μ) (haS : aS) :
                  theorem ProbabilityTheory.iIndepSets.iIndep {Ω : Type u_1} {ι : Type u_2} {m : ιMeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (h_le : ∀ (i : ι), m i _mΩ) (π : ιSet (Set Ω)) (h_pi : ∀ (n : ι), IsPiSystem (π n)) (h_generate : ∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)) (h_ind : ProbabilityTheory.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.IndepSet.measure_inter_eq_mul {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {s : Set Ω} {t : Set Ω} {μ : MeasureTheory.Measure Ω} (h : ProbabilityTheory.IndepSet s t μ) :
                  μ (s t) = μ s * μ t
                  theorem ProbabilityTheory.IndepSets.indepSet_of_mem {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {s : Set Ω} {t : Set Ω} (S : Set (Set Ω)) (T : Set (Set Ω)) (hs : s S) (ht : t T) (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (h_indep : ProbabilityTheory.IndepSets S T μ) :
                  theorem ProbabilityTheory.Indep.indepSet_of_measurableSet {Ω : Type u_1} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (h_indep : ProbabilityTheory.Indep m₁ m₂ μ) {s : Set Ω} {t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) :
                  theorem ProbabilityTheory.iIndep_comap_mem_iff {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ιSet Ω} :
                  ProbabilityTheory.iIndep (fun (i : ι) => MeasurableSpace.comap (fun (x : Ω) => x f i) ) μ ProbabilityTheory.iIndepSet f μ
                  theorem ProbabilityTheory.iIndepSet.iIndep_comap_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ιSet Ω} :
                  ProbabilityTheory.iIndepSet f μProbabilityTheory.iIndep (fun (i : ι) => MeasurableSpace.comap (fun (x : Ω) => x f i) ) μ

                  Alias of the reverse direction of ProbabilityTheory.iIndep_comap_mem_iff.

                  theorem ProbabilityTheory.iIndepSets_singleton_iff {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ιSet Ω} :
                  ProbabilityTheory.iIndepSets (fun (i : ι) => {s i}) μ ∀ (t : Finset ι), μ (⋂ it, s i) = it, μ (s i)
                  theorem ProbabilityTheory.iIndepSet.meas_biInter {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ιSet Ω} (h : ProbabilityTheory.iIndepSet f μ) (s : Finset ι) :
                  μ (⋂ is, f i) = is, μ (f i)
                  theorem ProbabilityTheory.iIndepSet_iff_iIndepSets_singleton {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ιSet Ω} (hf : ∀ (i : ι), MeasurableSet (f i)) :
                  theorem ProbabilityTheory.iIndepSet_iff_meas_biInter {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ιSet Ω} (hf : ∀ (i : ι), MeasurableSet (f i)) :
                  ProbabilityTheory.iIndepSet f μ ∀ (s : Finset ι), μ (⋂ is, f i) = is, μ (f i)
                  theorem ProbabilityTheory.iIndepSets.iIndepSet_of_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {π : ιSet (Set Ω)} {f : ιSet Ω} (hfπ : ∀ (i : ι), f i π i) (hf : ∀ (i : ι), MeasurableSet (f i)) (hπ : ProbabilityTheory.iIndepSets π μ) :

                  Independence of random variables #

                  theorem ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} :
                  ProbabilityTheory.IndepFun f g μ ∀ (s : Set β) (t : Set β'), MeasurableSet sMeasurableSet tμ (f ⁻¹' s g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)
                  theorem ProbabilityTheory.IndepFun.measure_inter_preimage_eq_mul {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} :
                  ProbabilityTheory.IndepFun f g μ∀ (s : Set β) (t : Set β'), MeasurableSet sMeasurableSet tμ (f ⁻¹' s g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)

                  Alias of the forward direction of ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul.

                  theorem ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_10} {β : ιType u_11} {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ωβ i} :
                  ProbabilityTheory.iIndepFun m f μ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ iS, MeasurableSet (sets i))μ (⋂ iS, f i ⁻¹' sets i) = iS, μ (f i ⁻¹' sets i)
                  theorem ProbabilityTheory.iIndepFun.measure_inter_preimage_eq_mul {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_10} {β : ιType u_11} {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ωβ i} :
                  ProbabilityTheory.iIndepFun m f μ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ iS, MeasurableSet (sets i))μ (⋂ iS, f i ⁻¹' sets i) = iS, μ (f i ⁻¹' sets i)

                  Alias of the forward direction of ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul.

                  theorem ProbabilityTheory.indepFun_iff_indepSet_preimage {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hf : Measurable f) (hg : Measurable g) :
                  ProbabilityTheory.IndepFun f g μ ∀ (s : Set β) (t : Set β'), MeasurableSet sMeasurableSet tProbabilityTheory.IndepSet (f ⁻¹' s) (g ⁻¹' t) μ
                  theorem ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [MeasureTheory.IsFiniteMeasure μ] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                  theorem ProbabilityTheory.IndepFun.symm {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ωβ} {g : Ωβ'} :
                  theorem ProbabilityTheory.IndepFun.ae_eq {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ωβ} {g : Ωβ'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {f' : Ωβ} {g' : Ωβ'} (hfg : ProbabilityTheory.IndepFun f g μ) (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') :
                  theorem ProbabilityTheory.IndepFun.comp {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {γ : Type u_8} {γ' : Type u_9} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ωβ} {g : Ωβ'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} {_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'} {φ : βγ} {ψ : β'γ'} (hfg : ProbabilityTheory.IndepFun f g μ) (hφ : Measurable φ) (hψ : Measurable ψ) :
                  theorem ProbabilityTheory.IndepFun.neg_right {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ωβ} {g : Ωβ'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β'] [MeasurableNeg β'] (hfg : ProbabilityTheory.IndepFun f g μ) :
                  theorem ProbabilityTheory.IndepFun.neg_left {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ωβ} {g : Ωβ'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β] [MeasurableNeg β] (hfg : ProbabilityTheory.IndepFun f g μ) :
                  theorem ProbabilityTheory.iIndepFun.of_subsingleton {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ιType u_10} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} [MeasureTheory.IsProbabilityMeasure μ] [Subsingleton ι] :
                  theorem ProbabilityTheory.iIndepFun.isProbabilityMeasure {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ιType u_10} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (h : ProbabilityTheory.iIndepFun m f μ) :
                  theorem ProbabilityTheory.iIndepFun.indepFun_finset {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ιType u_10} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (S : Finset ι) (T : Finset ι) (hST : Disjoint S T) (hf_Indep : ProbabilityTheory.iIndepFun m f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) :
                  ProbabilityTheory.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.iIndepFun.indepFun_prod_mk {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ιType u_10} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (hf_Indep : ProbabilityTheory.iIndepFun m f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.IndepFun (fun (a : Ω) => (f i a, f j a)) (f k) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_prod_mk_prod_mk {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ιType u_10} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (h_indep : ProbabilityTheory.iIndepFun m f μ) (hf : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i k) (hil : i l) (hjk : j k) (hjl : j l) :
                  ProbabilityTheory.IndepFun (fun (a : Ω) => (f i a, f j a)) (fun (a : Ω) => (f k a, f l a)) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_add_left {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.IndepFun (f i + f j) (f k) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_mul_left {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.IndepFun (f i * f j) (f k) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_add_right {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.IndepFun (f i) (f j + f k) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_mul_right {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.IndepFun (f i) (f j * f k) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_add_add {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.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.IndepFun (f i + f j) (f k + f l) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_mul_mul {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.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.IndepFun (f i * f j) (f k * f l) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_sub_left {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.IndepFun (f i - f j) (f k) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_div_left {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
                  ProbabilityTheory.IndepFun (f i / f j) (f k) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_sub_right {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.IndepFun (f i) (f j - f k) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_div_right {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
                  ProbabilityTheory.IndepFun (f i) (f j / f k) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_sub_sub {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.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.IndepFun (f i - f j) (f k - f l) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_div_div {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ιΩβ} (hf_indep : ProbabilityTheory.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.IndepFun (f i / f j) (f k / f l) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_finset_sum_of_not_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : ιΩβ} (hf_Indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : is) :
                  ProbabilityTheory.IndepFun (∑ js, f j) (f i) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_not_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : ιΩβ} (hf_Indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : is) :
                  ProbabilityTheory.IndepFun (∏ js, f j) (f i) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_sum_range_succ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : Ωβ} (hf_Indep : ProbabilityTheory.iIndepFun (fun (x : ) => m) f μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
                  ProbabilityTheory.IndepFun (∑ jFinset.range n, f j) (f n) μ
                  theorem ProbabilityTheory.iIndepFun.indepFun_prod_range_succ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : Ωβ} (hf_Indep : ProbabilityTheory.iIndepFun (fun (x : ) => m) f μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
                  ProbabilityTheory.IndepFun (∏ jFinset.range n, f j) (f n) μ
                  theorem ProbabilityTheory.iIndepSet.iIndepFun_indicator {Ω : Type u_1} {ι : Type u_2} {β : Type u_6} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Zero β] [One β] {m : MeasurableSpace β} {s : ιSet Ω} (hs : ProbabilityTheory.iIndepSet s μ) :
                  ProbabilityTheory.iIndepFun (fun (_n : ι) => m) (fun (n : ι) => (s n).indicator fun ( : Ω) => 1) μ