English
If two pi-systems are independent, then the corresponding sigma-algebras are independent.
Русский
Если две Pi-системы независимы, то соответствующие сигма-алгебры независимы.
LaTeX
$$IndepSets p1 p2 κ μ → Indep (generateFrom p1) (generateFrom p2) κ μ$$
Lean4
/-- The measurable space structures generated by independent pi-systems are independent. -/
theorem indep {m1 m2 m : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ]
{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 κ μ :=
by
rcases eq_zero_or_isMarkovKernel κ with rfl | h
· simp
intro t1 t2 ht1 ht2
induction t1, ht1 using induction_on_inter hpm1 hp1 with
| empty => simp only [Set.empty_inter, measure_empty, zero_mul, Filter.eventually_true]
| basic t ht =>
refine IndepSets.indep_aux h2 hp2 hpm2 hyp ht (h1 _ ?_) ht2
rw [hpm1]
exact measurableSet_generateFrom ht
| compl t ht iht =>
filter_upwards [iht] with a ha
have : tᶜ ∩ t2 = t2 \ (t ∩ t2) := by rw [Set.inter_comm t, Set.diff_self_inter, Set.diff_eq_compl_inter]
rw [this, Set.inter_comm t t2,
measure_diff Set.inter_subset_left ((h2 _ ht2).inter (h1 _ ht)).nullMeasurableSet (measure_ne_top (κ a) _),
Set.inter_comm, ha, measure_compl (h1 _ ht) (measure_ne_top (κ a) t), measure_univ, mul_comm (1 - κ a t),
ENNReal.mul_sub (fun _ _ ↦ measure_ne_top (κ a) _), mul_one, mul_comm]
| iUnion f hf_disj hf_meas h =>
rw [← ae_all_iff] at h
filter_upwards [h] with a ha
rw [Set.inter_comm, Set.inter_iUnion, measure_iUnion]
· rw [measure_iUnion hf_disj (fun i ↦ h1 _ (hf_meas i))]
rw [← ENNReal.tsum_mul_right]
congr 1 with i
rw [Set.inter_comm t2, ha i]
· intro i j hij
rw [Function.onFun, Set.inter_comm t2, Set.inter_comm t2]
exact Disjoint.inter_left _ (Disjoint.inter_right _ (hf_disj hij))
· exact fun i ↦ (h2 _ ht2).inter (h1 _ (hf_meas i))
