Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
let μ_inter := μ.restrict t1
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
let ν := μ t1 • μ
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
have h_univ : μ_inter Set.univ = ν Set.univ := by
  rw [Measure.restrict_apply_univ, Measure.smul_apply, smul_eq_mul, measure_univ, mul_one]
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
haveI : IsFiniteMeasure μ_inter := @Restrict.isFiniteMeasure Ω _ t1 μ ⟨measure_lt_top μ t1⟩
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
⊢ ↑↑(Measure.restrict μ t1) t2 = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
rw [Set.inter_comm, ← Measure.restrict_apply (h2 t2 ht2m)]
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
⊢ ↑↑μ_inter t = ↑↑ν t
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
⊢ ↑↑(Measure.restrict μ t1) t2 = ↑↑μ t1 * ↑↑μ t2
refine' ext_on_measurableSpace_of_generate_finite m p2 (fun t ht => _) h2 hpm2 hp2 h_univ ht2m
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
ht2 : MeasurableSet t
⊢ ↑↑μ_inter t = ↑↑ν t
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
⊢ ↑↑μ_inter t = ↑↑ν t
have ht2 : MeasurableSet[m] t := by
  refine' h2 _ _
  rw [hpm2]
  exact measurableSet_generateFrom ht
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
ht2 : MeasurableSet t
⊢ ↑↑μ (t1 ∩ t) = ↑↑μ t1 • ↑↑μ t
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
ht2 : MeasurableSet t
⊢ ↑↑μ_inter t = ↑↑ν t
rw [Measure.restrict_apply ht2, Measure.smul_apply, Set.inter_comm]
no goals
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
ht2 : MeasurableSet t
⊢ ↑↑μ (t1 ∩ t) = ↑↑μ t1 • ↑↑μ t
exact hyp t1 t ht1 ht
no goals
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
⊢ ↑↑μ_inter Set.univ = ↑↑ν Set.univ
rw [Measure.restrict_apply_univ, Measure.smul_apply, smul_eq_mul, measure_univ, mul_one]
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
⊢ MeasurableSet t
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
⊢ MeasurableSet t
refine' h2 _ _
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
⊢ MeasurableSet t
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
⊢ MeasurableSet t
rw [hpm2]
no goals
Ω : Type u_1
ι : Type ?u.1680679
m2 m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
p1 p2 : Set (Set Ω)
h2 : m2 ≤ m
hp2 : IsPiSystem p2
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht2m : MeasurableSet t2
μ_inter : MeasureTheory.Measure Ω := Measure.restrict μ t1
ν : MeasureTheory.Measure Ω := ↑↑μ t1 • μ
h_univ : ↑↑μ_inter Set.univ = ↑↑ν Set.univ
this : IsFiniteMeasure μ_inter
t : Set Ω
ht : t ∈ p2
⊢ MeasurableSet t
exact measurableSet_generateFrom ht