English
From an independence statement of pi-systems, obtain independence of generated sigma-algebras.
Русский
Из независимости пи-систем получить независимость порожденных сигма-алгебр.
LaTeX
$$indep'(hp1m,hp2m,hp1,hp2,hyp) : Indep(generateFrom p1) (generateFrom p2) κ μ$$
Lean4
theorem indep_aux {m₂ m : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ]
{p1 p2 : Set (Set Ω)} (h2 : m₂ ≤ m) (hp2 : IsPiSystem p2) (hpm2 : m₂ = generateFrom p2) (hyp : IndepSets p1 p2 κ μ)
{t1 t2 : Set Ω} (ht1 : t1 ∈ p1) (ht1m : MeasurableSet[m] t1) (ht2m : MeasurableSet[m₂] t2) :
∀ᵐ a ∂μ, κ a (t1 ∩ t2) = κ a t1 * κ a t2 :=
by
rcases eq_zero_or_isMarkovKernel κ with rfl | h
· simp
induction t2, ht2m using induction_on_inter hpm2 hp2 with
| empty => simp
| basic u hu => exact hyp t1 u ht1 hu
| compl u hu ihu =>
filter_upwards [ihu] with a ha
rw [← Set.diff_eq, ← Set.diff_self_inter,
measure_diff inter_subset_left (ht1m.inter (h2 _ hu)).nullMeasurableSet (measure_ne_top _ _), ha,
measure_compl (h2 _ hu) (measure_ne_top _ _), measure_univ, ENNReal.mul_sub, mul_one]
exact fun _ _ ↦ measure_ne_top _ _
| iUnion f hfd hfm ihf =>
rw [← ae_all_iff] at ihf
filter_upwards [ihf] with a ha
rw [inter_iUnion, measure_iUnion, measure_iUnion hfd fun i ↦ h2 _ (hfm i)]
· simp only [ENNReal.tsum_mul_left, ha]
· exact hfd.mono fun i j h ↦ (h.inter_left' _).inter_right' _
· exact fun i ↦ .inter ht1m (h2 _ <| hfm i)
