awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
x : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
⊢ IndepSet s t μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
simp only [IndepSet_iff_Indep, Indep_iff]

Premises used: ProbabilityTheory.Indep_iff, ProbabilityTheory.IndepSet_iff_Indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
β : ι → Type u_7
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
μ : Measure Ω
⊢ iIndepFun (β := β) f μ ↔ iIndep (fun (x : ι) ↦ MeasurableSpace.comap (f x) (m x)) μ

Tactic:
simp only [iIndepFun, iIndep, Kernel.iIndepFun]

Premises used: ProbabilityTheory.iIndepFun, ProbabilityTheory.Kernel.iIndepFun, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
inst : Subsingleton ι
m : ι → Set (Set Ω)
inst_1 : IsProbabilityMeasure μ
⊢ iIndepSets m μ

Tactic:
Kernel.iIndepSets.of_subsingleton

Premises used: ProbabilityTheory.iIndepSets, ProbabilityTheory.Kernel.iIndepSets.of_subsingleton
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
inst : Subsingleton ι
m : ι → MeasurableSpace Ω
inst_1 : IsProbabilityMeasure μ
⊢ iIndep m μ

Tactic:
Kernel.iIndep.of_subsingleton

Premises used: ProbabilityTheory.Kernel.iIndep.of_subsingleton, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
inst : Subsingleton ι
β : ι → Type u_7
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
⊢ iIndepFun (β := β) f μ

Tactic:
Kernel.iIndepFun.of_subsingleton

Premises used: ProbabilityTheory.Kernel.iIndepFun.of_subsingleton, ProbabilityTheory.iIndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
κ : ι → Type u_5
x : MeasurableSpace Ω
μ : Measure Ω
m : (i : ι) → MeasurableSpace (κ i)
f : (x : ι) → Ω → κ x
hf : iIndepFun (β := κ) f μ
⊢ iIndep (fun (x : ι) ↦ MeasurableSpace.comap (f x) (m x)) μ

Tactic:
hf

Premises used: ProbabilityTheory.Kernel.iIndepFun, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
β : ι → Type u_7
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
μ : Measure Ω
⊢ iIndepFun (β := β) f μ ↔
    ∀ (s : Finset ι) {f' : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f' i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f' i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f' i) : ℝ≥0∞)

Tactic:
simp only [iIndepFun_iff_iIndep, iIndep_iff]

Premises used: ProbabilityTheory.iIndepFun_iff_iIndep, ProbabilityTheory.iIndep_iff
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
κ : ι → Type u_5
x : MeasurableSpace Ω
μ : Measure Ω
S : Finset ι
s : ι → Set Ω
m : (i : ι) → MeasurableSpace (κ i)
f : (x : ι) → Ω → κ x
hf : iIndepFun (β := κ) f μ
hs : ∀ i ∈ S, MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞) (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
hf.iIndep.meas_biInter hs

Premises used: ProbabilityTheory.iIndep.meas_biInter, ProbabilityTheory.iIndepFun.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
κ : ι → Type u_5
x : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
inst : Fintype ι
m : (i : ι) → MeasurableSpace (κ i)
f : (x : ι) → Ω → κ x
hf : iIndepFun (β := κ) f μ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
hf.iIndep.meas_iInter hs

Premises used: ProbabilityTheory.iIndepFun.iIndep, ProbabilityTheory.iIndep.meas_iInter
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_3
γ : Type u_4
x : MeasurableSpace Ω
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
⊢ f ⟂ᵢ[μ] g ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ

Tactic:
simp only [IndepFun, Indep, Kernel.IndepFun]

Premises used: ProbabilityTheory.Kernel.IndepFun, ProbabilityTheory.Indep, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
x : MeasurableSpace Ω
β : Type u_7
γ : Type u_8
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
rw :
  Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
rw₁ rw₂ :
  (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ f ⟂ᵢ[μ] g ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
rw [IndepFun_iff_Indep, Indep_iff]

Premises used: ProbabilityTheory.IndepFun_iff_Indep, ProbabilityTheory.Indep_iff
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_3
γ : Type u_4
x : MeasurableSpace Ω
μ : Measure Ω
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hfg : f ⟂ᵢ[μ] g
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
(IndepFun_iff _ _ _).1 hfg _ _ hs ht

Premises used: Iff.mp, ProbabilityTheory.IndepFun_iff
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x : MeasurableSpace Ω
μ : Measure Ω
ι' : Type u_6
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π μ
⊢ iIndepSets (π ∘ g) μ

Tactic:
Kernel.iIndepSets.precomp hg h

Premises used: ProbabilityTheory.Kernel.iIndepSets.precomp, ProbabilityTheory.iIndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x : MeasurableSpace Ω
μ : Measure Ω
ι' : Type u_6
g : ι' → ι
hg : Function.Surjective g
h : iIndepSets (π ∘ g) μ
⊢ iIndepSets π μ

Tactic:
Kernel.iIndepSets.of_precomp hg h

Premises used: ProbabilityTheory.iIndepSets, ProbabilityTheory.Kernel.iIndepSets.of_precomp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x : MeasurableSpace Ω
μ : Measure Ω
ι' : Type u_6
g : ι' → ι
hg : Function.Bijective g
⊢ iIndepSets (π ∘ g) μ ↔ iIndepSets π μ

Tactic:
Kernel.iIndepSets_precomp_of_bijective hg

Premises used: ProbabilityTheory.Kernel.iIndepSets_precomp_of_bijective, ProbabilityTheory.iIndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
x : MeasurableSpace Ω
μ : Measure Ω
ι' : Type u_6
g : ι' → ι
hg : Function.Injective g
h : iIndep m μ
⊢ iIndep (m ∘ g) μ

Tactic:
Kernel.iIndep.precomp hg h

Premises used: ProbabilityTheory.Kernel.iIndep.precomp, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
x : MeasurableSpace Ω
μ : Measure Ω
ι' : Type u_6
g : ι' → ι
hg : Function.Surjective g
h : iIndep (m ∘ g) μ
⊢ iIndep m μ

Tactic:
Kernel.iIndep.of_precomp hg h

Premises used: ProbabilityTheory.Kernel.iIndep.of_precomp, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
x : MeasurableSpace Ω
μ : Measure Ω
ι' : Type u_6
g : ι' → ι
hg : Function.Bijective g
⊢ iIndep (m ∘ g) μ ↔ iIndep m μ

Tactic:
Kernel.iIndep_precomp_of_bijective hg

Premises used: ProbabilityTheory.Kernel.iIndep_precomp_of_bijective, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
ι' : Type u_6
g : ι' → ι
hg : Function.Injective g
h : iIndepSet s μ
⊢ iIndepSet (s ∘ g) μ

Tactic:
Kernel.iIndepSet.precomp hg h

Premises used: ProbabilityTheory.iIndepSet, ProbabilityTheory.Kernel.iIndepSet.precomp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
ι' : Type u_6
g : ι' → ι
hg : Function.Surjective g
h : iIndepSet (s ∘ g) μ
⊢ iIndepSet s μ

Tactic:
Kernel.iIndepSet.of_precomp hg h

Premises used: ProbabilityTheory.iIndepSet, ProbabilityTheory.Kernel.iIndepSet.of_precomp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
ι' : Type u_6
g : ι' → ι
hg : Function.Bijective g
⊢ iIndepSet (s ∘ g) μ ↔ iIndepSet s μ

Tactic:
Kernel.iIndepSet_precomp_of_bijective hg

Premises used: ProbabilityTheory.iIndepSet, ProbabilityTheory.Kernel.iIndepSet_precomp_of_bijective
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
ι' : Type u_6
g : ι' → ι
β : ι → Type u_7
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hg : Function.Injective g
h : iIndepFun (β := β) f μ
⊢ iIndepFun (β := fun (i : ι') ↦ β (g i)) (fun (i : ι') ↦ f (g i)) μ

Tactic:
Kernel.iIndepFun.precomp hg h

Premises used: ProbabilityTheory.iIndepFun, ProbabilityTheory.Kernel.iIndepFun.precomp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
ι' : Type u_6
g : ι' → ι
β : ι → Type u_7
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hg : Function.Surjective g
h : iIndepFun (β := fun (i : ι') ↦ β (g i)) (fun (i : ι') ↦ f (g i)) μ
⊢ iIndepFun (β := β) f μ

Tactic:
Kernel.iIndepFun.of_precomp hg h

Premises used: ProbabilityTheory.iIndepFun, ProbabilityTheory.Kernel.iIndepFun.of_precomp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
ι' : Type u_6
g : ι' → ι
β : ι → Type u_7
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hg : Function.Bijective g
⊢ iIndepFun (β := fun (i : ι') ↦ β (g i)) (fun (i : ι') ↦ f (g i)) μ ↔ iIndepFun (β := β) f μ

Tactic:
Kernel.iIndepFun_precomp_of_bijective hg

Premises used: ProbabilityTheory.iIndepFun, ProbabilityTheory.Kernel.iIndepFun_precomp_of_bijective
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ μ
⊢ IndepSets s₂ s₁ μ

Tactic:
Kernel.IndepSets.symm h

Premises used: ProbabilityTheory.Kernel.IndepSets.symm, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
h : Indep m₁ m₂ μ
⊢ Indep m₂ m₁ μ

Tactic:
IndepSets.symm h

Premises used: ProbabilityTheory.Kernel.Indep, ProbabilityTheory.Indep, ProbabilityTheory.IndepSets.symm
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m' _mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
⊢ Indep m' ⊥ μ

Tactic:
Kernel.indep_bot_right m'

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.indep_bot_right
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m' _mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
⊢ Indep ⊥ m' μ

Tactic:
(indep_bot_right m').symm

Premises used: ProbabilityTheory.Indep.symm, ProbabilityTheory.indep_bot_right
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
s : Set Ω
⊢ IndepSet s ∅ μ

Tactic:
Kernel.indepSet_empty_right s

Premises used: ProbabilityTheory.IndepSet, ProbabilityTheory.Kernel.indepSet_empty_right
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
s : Set Ω
⊢ IndepSet ∅ s μ

Tactic:
Kernel.indepSet_empty_left s

Premises used: ProbabilityTheory.IndepSet, ProbabilityTheory.Kernel.indepSet_empty_left
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s₁ s₂ s₃ : Set (Set Ω)
h_indep : IndepSets s₁ s₂ μ
h31 : s₃ ⊆ s₁
⊢ IndepSets s₃ s₂ μ

Tactic:
Kernel.indepSets_of_indepSets_of_le_left h_indep h31

Premises used: ProbabilityTheory.IndepSets, ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_left
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s₁ s₂ s₃ : Set (Set Ω)
h_indep : IndepSets s₁ s₂ μ
h32 : s₃ ⊆ s₂
⊢ IndepSets s₁ s₃ μ

Tactic:
Kernel.indepSets_of_indepSets_of_le_right h_indep h32

Premises used: ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_right, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m₁ m₂ m₃ _mΩ : MeasurableSpace Ω
μ : Measure Ω
h_indep : Indep m₁ m₂ μ
h31 : m₃ ≤ m₁
⊢ Indep m₃ m₂ μ

Tactic:
Kernel.indep_of_indep_of_le_left h_indep h31

Premises used: ProbabilityTheory.Kernel.indep_of_indep_of_le_left, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m₁ m₂ m₃ _mΩ : MeasurableSpace Ω
μ : Measure Ω
h_indep : Indep m₁ m₂ μ
h32 : m₃ ≤ m₂
⊢ Indep m₁ m₃ μ

Tactic:
Kernel.indep_of_indep_of_le_right h_indep h32

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.indep_of_indep_of_le_right
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m₁ m₂ m₃ m₄ _mΩ : MeasurableSpace Ω
μ : Measure Ω
h_indep : Indep m₁ m₂ μ
h31 : m₃ ≤ m₁
h42 : m₄ ≤ m₂
⊢ Indep m₃ m₄ μ

Tactic:
Kernel.indep_of_indep_of_le h_indep h31 h42

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.indep_of_indep_of_le
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
m₁ m₂ : ι → MeasurableSpace Ω
h_indep : iIndep m₂ μ
h_le : ∀ (i : ι), m₁ i ≤ m₂ i
⊢ iIndep m₁ μ

Tactic:
Kernel.iIndep_of_iIndep_of_le h_indep h_le

Premises used: ProbabilityTheory.Kernel.iIndep_of_iIndep_of_le, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s₁ s₂ s' : Set (Set Ω)
h₁ : IndepSets s₁ s' μ
h₂ : IndepSets s₂ s' μ
⊢ IndepSets (s₁ ∪ s₂) s' μ

Tactic:
Kernel.IndepSets.union h₁ h₂

Premises used: ProbabilityTheory.IndepSets, ProbabilityTheory.Kernel.IndepSets.union
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s₁ s₂ s' : Set (Set Ω)
⊢ IndepSets (s₁ ∪ s₂) s' μ ↔ IndepSets s₁ s' μ ∧ IndepSets s₂ s' μ

Tactic:
Kernel.IndepSets.union_iff

Premises used: ProbabilityTheory.Kernel.IndepSets.union_iff, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
hyp : ∀ (n : ι), IndepSets (s n) s' μ
⊢ IndepSets (⋃ (n : ι), s n) s' μ

Tactic:
Kernel.IndepSets.iUnion hyp

Premises used: ProbabilityTheory.Kernel.IndepSets.iUnion, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' μ
⊢ IndepSets (⋃ n ∈ u, s n) s' μ

Tactic:
Kernel.IndepSets.biUnion hyp

Premises used: ProbabilityTheory.Kernel.IndepSets.biUnion, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s₁ s' s₂ : Set (Set Ω)
h₁ : IndepSets s₁ s' μ
⊢ IndepSets (s₁ ∩ s₂) s' μ

Tactic:
Kernel.IndepSets.inter s₂ h₁

Premises used: ProbabilityTheory.IndepSets, ProbabilityTheory.Kernel.IndepSets.inter
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
h : ∃ (n : ι), IndepSets (s n) s' μ
⊢ IndepSets (⋂ (n : ι), s n) s' μ

Tactic:
Kernel.IndepSets.iInter h

Premises used: ProbabilityTheory.Kernel.IndepSets.iInter, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
u : Set ι
h : ∃ n ∈ u, IndepSets (s n) s' μ
⊢ IndepSets (⋂ n ∈ u, s n) s' μ

Tactic:
Kernel.IndepSets.bInter h

Premises used: ProbabilityTheory.Kernel.IndepSets.bInter, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
⊢ IndepSets {s} {t} μ ↔
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [IndepSets, Kernel.indepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]

Premises used: MeasureTheory.ae_dirac_eq, ProbabilityTheory.IndepSets, Filter.eventually_pure, ProbabilityTheory.Kernel.const_apply, ProbabilityTheory.Kernel.indepSets_singleton_iff
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
𝒜 ℬ : Set (Set Ω)
h : ∀ A ∈ 𝒜, IndepSets {A} ℬ μ
rw : IndepSets (⋃ x ∈ 𝒜, {x}) ℬ μ
⊢ IndepSets 𝒜 ℬ μ

Tactic:
rw [← 𝒜.biUnion_of_singleton]

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
𝒜 ℬ : Set (Set Ω)
h : ∀ A ∈ 𝒜, IndepSets {A} ℬ μ
⊢ IndepSets (⋃ x ∈ 𝒜, {x}) ℬ μ

Tactic:
IndepSets.biUnion h

Premises used: ProbabilityTheory.IndepSets.biUnion
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
𝒜 ℬ : Set (Set Ω)
h : ∀ A ∈ 𝒜, IndepSets {A} ℬ μ
⊢ IndepSets (⋃ x ∈ 𝒜, {x}) ℬ μ

Tactic:
exact IndepSets.biUnion h

Premises used: ProbabilityTheory.IndepSets.biUnion
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set (Set Ω)
h_indep : iIndepSets s μ
i j : ι
hij : i ≠ j
⊢ IndepSets (s i) (s j) μ

Tactic:
Kernel.iIndepSets.indepSets h_indep hij

Premises used: ProbabilityTheory.Kernel.iIndepSets.indepSets, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
h_indep : iIndep m μ
i j : ι
hij : i ≠ j
⊢ Indep (m i) (m j) μ

Tactic:
Kernel.iIndep.indep h_indep hij

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.iIndep.indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_6
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf_Indep : iIndepFun (β := β) f μ
i j : ι
hij : i ≠ j
⊢ f i ⟂ᵢ[μ] f j

Tactic:
Kernel.iIndepFun.indepFun hf_Indep hij

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set (Set Ω)
hms : ∀ (n : ι), m n = generateFrom (s n)
h_indep : iIndep m μ
⊢ ProbabilityTheory.iIndepSets s μ

Tactic:
Kernel.iIndep.iIndepSets hms h_indep

Premises used: ProbabilityTheory.Kernel.iIndep.iIndepSets, ProbabilityTheory.iIndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s1 s2 : Set (Set Ω)
h_indep : Indep (generateFrom s1) (generateFrom s2) μ
⊢ IndepSets s1 s2 μ

Tactic:
Kernel.Indep.indepSets h_indep

Premises used: ProbabilityTheory.IndepSets, ProbabilityTheory.Kernel.Indep.indepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m1 m2 _mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ _mΩ
h2 : m2 ≤ _mΩ
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 μ
⊢ Indep m1 m2 μ

Tactic:
Kernel.IndepSets.indep h1 h2 hp1 hp2 hpm1 hpm2 hyp

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.IndepSets.indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
p1 p2 : Set (Set Ω)
hp1m : ∀ s ∈ p1, MeasurableSet s
hp2m : ∀ s ∈ p2, MeasurableSet s
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hyp : IndepSets p1 p2 μ
⊢ Indep (generateFrom p1) (generateFrom p2) μ

Tactic:
Kernel.IndepSets.indep' hp1m hp2m hp1 hp2 hyp

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.IndepSets.indep'
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s μ
hST : Disjoint S T
⊢ IndepSets (piiUnionInter s S) (piiUnionInter s T) μ

Tactic:
Kernel.indepSets_piiUnionInter_of_disjoint h_indep hST

Premises used: ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
S T : Set ι
hST : Disjoint S T
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) μ

Tactic:
Kernel.iIndepSet.indep_generateFrom_of_disjoint hsm hs S T hST

Premises used: ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m μ
S T : Set ι
hST : Disjoint S T
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) μ

Tactic:
Kernel.indep_iSup_of_disjoint h_le h_indep hST

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.indep_iSup_of_disjoint
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
m1 _mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m1 μ
h_le : ∀ (i : ι), m i ≤ _mΩ
h_le' : m1 ≤ _mΩ
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
⊢ Indep (⨆ (i : ι), m i) m1 μ

Tactic:
Kernel.indep_iSup_of_directed_le h_indep h_le h_le' hm

Premises used: ProbabilityTheory.Kernel.indep_iSup_of_directed_le, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
i : ι
⊢ Indep (generateFrom {s i}) (generateFrom {t : Set Ω | ∃ j < i, s j = t}) μ

Tactic:
Kernel.iIndepSet.indep_generateFrom_lt hsm hs i

Premises used: ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_lt, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
i k : ι
hk : i < k
⊢ Indep (generateFrom {s k}) (generateFrom {t : Set Ω | ∃ j ≤ i, s j = t}) μ

Tactic:
Kernel.iIndepSet.indep_generateFrom_le hsm hs i hk

Premises used: ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le, ProbabilityTheory.Indep