English
Independence of a family of sets is equivalent to a family of measurable bi-intersections across finite sets.
Русский
Независимость семейства множеств эквивалентна независимости для би—пересечений измеримых множеств по конечным подмножествам.
LaTeX
$$$iIndepSet f κ μ \Leftrightarrow \forall s, \forall_{sets}, \mathrm{measurable}...$$$
Lean4
theorem congr' {β : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)} {f g : Π i, Ω → β i} (hf : iIndepFun f κ μ)
(h : ∀ i, ∀ᵐ a ∂μ, f i =ᵐ[κ a] g i) : iIndepFun g κ μ :=
by
rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at hf ⊢
intro S sets hmeas
have : ∀ᵐ a ∂μ, ∀ i ∈ S, f i =ᵐ[κ a] g i := (ae_ball_iff (Finset.countable_toSet S)).2 (fun i hi ↦ h i)
filter_upwards [this, hf S hmeas] with a ha h'a
have A i (hi : i ∈ S) : (κ a) (g i ⁻¹' sets i) = (κ a) (f i ⁻¹' sets i) :=
by
apply measure_congr
filter_upwards [ha i hi] with ω hω
change (g i ω ∈ sets i) = (f i ω ∈ sets i)
simp [hω]
have B : (κ a) (⋂ i ∈ S, g i ⁻¹' sets i) = (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) :=
by
apply measure_congr
filter_upwards [(ae_ball_iff (Finset.countable_toSet S)).2 ha] with ω hω
change (ω ∈ ⋂ i ∈ S, g i ⁻¹' sets i) = (ω ∈ ⋂ i ∈ S, f i ⁻¹' sets i)
simp +contextual [hω]
convert h'a using 2 with i hi
exact A i hi
