[GOAL]
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
⊢ iIndepSets π ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ (i : ι), i ∈ s → f i ∈ π i) → ↑↑μ (⋂ (i : ι) (_ : i ∈ s), f i) = ∏ i in s, ↑↑μ (f i)
[PROOFSTEP]
simp only [iIndepSets, kernel.iIndepSets, ae_dirac_eq, Filter.eventually_pure, kernel.const_apply]
[GOAL]
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s1 s2 : Set (Set Ω)
μ : Measure Ω
⊢ IndepSets s1 s2 ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
[PROOFSTEP]
simp only [IndepSets, kernel.IndepSets, ae_dirac_eq, Filter.eventually_pure, kernel.const_apply]
[GOAL]
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
inst✝ : MeasurableSpace Ω
μ : Measure Ω
⊢ iIndep m ↔ iIndepSets fun x => {s | MeasurableSet s}
[PROOFSTEP]
simp only [iIndep, iIndepSets, kernel.iIndep]
[GOAL]
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
inst✝ : MeasurableSpace Ω
μ : Measure Ω
⊢ iIndep m ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ (i : ι), i ∈ s → MeasurableSet (f i)) → ↑↑μ (⋂ (i : ι) (_ : i ∈ s), f i) = ∏ i in s, ↑↑μ (f i)
[PROOFSTEP]
simp only [iIndep_iff_iIndepSets, iIndepSets_iff]
[GOAL]
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
inst✝ : MeasurableSpace Ω
μ : Measure Ω
⊢ (∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ (i : ι), i ∈ s → f i ∈ {s | MeasurableSet s}) → ↑↑μ (⋂ (i : ι) (_ : i ∈ s), f i) = ∏ i in s, ↑↑μ (f i)) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ (i : ι), i ∈ s → MeasurableSet (f i)) → ↑↑μ (⋂ (i : ι) (_ : i ∈ s), f i) = ∏ i in s, ↑↑μ (f i)
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
ι : Type u_2
m₁ m₂ inst✝ : MeasurableSpace Ω
μ : Measure Ω
⊢ Indep m₁ m₂ ↔ IndepSets {s | MeasurableSet s} {s | MeasurableSet s}
[PROOFSTEP]
simp only [Indep, IndepSets, kernel.Indep]
[GOAL]
Ω : Type u_1
ι : Type u_2
m₁ m₂ inst✝ : MeasurableSpace Ω
μ : Measure Ω
⊢ Indep m₁ m₂ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
[PROOFSTEP]
rw [Indep_iff_IndepSets, IndepSets_iff]
[GOAL]
Ω : Type u_1
ι : Type u_2
m₁ m₂ inst✝ : MeasurableSpace Ω
μ : Measure Ω
⊢ (∀ (t1 t2 : Set Ω), t1 ∈ {s | MeasurableSet s} → t2 ∈ {s | MeasurableSet s} → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2) ↔
    ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set Ω
μ : Measure Ω
⊢ iIndepSet s ↔ iIndep fun i => generateFrom {s i}
[PROOFSTEP]
simp only [iIndepSet, iIndep, kernel.iIndepSet]
[GOAL]
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set Ω
μ : Measure Ω
⊢ iIndepSet s ↔
    ∀ (s' : Finset ι) {f : ι → Set Ω},
      (∀ (i : ι), i ∈ s' → MeasurableSet (f i)) → ↑↑μ (⋂ (i : ι) (_ : i ∈ s'), f i) = ∏ i in s', ↑↑μ (f i)
[PROOFSTEP]
simp only [iIndepSet_iff_iIndep, iIndep_iff]
[GOAL]
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
⊢ IndepSet s t ↔ Indep (generateFrom {s}) (generateFrom {t})
[PROOFSTEP]
simp only [IndepSet, Indep, kernel.IndepSet]
[GOAL]
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
⊢ IndepSet s t ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
[PROOFSTEP]
simp only [IndepSet_iff_Indep, Indep_iff]
[GOAL]
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
μ : Measure Ω
⊢ iIndepFun m f ↔ iIndep fun x => MeasurableSpace.comap (f x) (m x)
[PROOFSTEP]
simp only [iIndepFun, iIndep, kernel.iIndepFun]
[GOAL]
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
μ : Measure Ω
⊢ iIndepFun m f ↔
    ∀ (s : Finset ι) {f' : ι → Set Ω},
      (∀ (i : ι), i ∈ s → MeasurableSet (f' i)) → ↑↑μ (⋂ (i : ι) (_ : i ∈ s), f' i) = ∏ i in s, ↑↑μ (f' i)
[PROOFSTEP]
simp only [iIndepFun_iff_iIndep, iIndep_iff]
[GOAL]
Ω : Type u_1
ι : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace Ω
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
⊢ IndepFun f g ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ)
[PROOFSTEP]
simp only [IndepFun, Indep, kernel.IndepFun]
[GOAL]
Ω : Type u_1
ι : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace Ω
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
⊢ IndepFun f g ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
[PROOFSTEP]
rw [IndepFun_iff_Indep, Indep_iff]
[GOAL]
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
⊢ IndepSets {s} {t} ↔ ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t
[PROOFSTEP]
simp only [IndepSets, kernel.indepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure, kernel.const_apply]
[GOAL]
Ω : Type u_1
ι : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
⊢ IndepFun f g ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
[PROOFSTEP]
simp only [IndepFun, kernel.indepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq, Filter.eventually_pure,
  kernel.const_apply]
[GOAL]
Ω : Type u_1
ι✝ : Type u_2
β✝ : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → β✝
g : Ω → β'
ι : Type u_7
β : ι → Type u_8
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
⊢ iIndepFun m f ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ (i : ι), i ∈ S → MeasurableSet (sets i)) →
        ↑↑μ (⋂ (i : ι) (_ : i ∈ S), f i ⁻¹' sets i) = ∏ i in S, ↑↑μ (f i ⁻¹' sets i)
[PROOFSTEP]
simp only [iIndepFun, kernel.iIndepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq, Filter.eventually_pure,
  kernel.const_apply]
[GOAL]
Ω : Type u_1
ι : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
⊢ IndepFun f g ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t)
[PROOFSTEP]
simp only [IndepFun, IndepSet, kernel.indepFun_iff_indepSet_preimage hf hg, ae_dirac_eq, Filter.eventually_pure,
  kernel.const_apply]
[GOAL]
Ω : Type u_1
ι : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
⊢ IndepFun f' g'
[PROOFSTEP]
refine kernel.IndepFun.ae_eq hfg ?_ ?_
[GOAL]
case refine_1
Ω : Type u_1
ι : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
⊢ ∀ᵐ (a : Unit) ∂Measure.dirac (), f =ᵐ[↑(kernel.const Unit μ) a] f'
[PROOFSTEP]
simp only [ae_dirac_eq, Filter.eventually_pure, kernel.const_apply]
[GOAL]
case refine_2
Ω : Type u_1
ι : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
⊢ ∀ᵐ (a : Unit) ∂Measure.dirac (), g =ᵐ[↑(kernel.const Unit μ) a] g'
[PROOFSTEP]
simp only [ae_dirac_eq, Filter.eventually_pure, kernel.const_apply]
[GOAL]
case refine_1
Ω : Type u_1
ι : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
⊢ f =ᵐ[μ] f'
case refine_2
Ω : Type u_1
ι : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
⊢ g =ᵐ[μ] g'
[PROOFSTEP]
exacts [hf, hg]
