English
Independence of two sigma-algebras is equivalent to independence of all pairs of single sets; equivalently, indep(m1,m2) iff ∀ s,t measurable, IndepSet s t κ μ.
Русский
Независимость двух сигма-алгебр эквивалентна независимости для всех пар одиночных множеств; эквивалентно indep(m1,m2) ⇔ ∀ s,t измеримые, IndepSet s t κ μ.
LaTeX
$$$Indep m_1 m_2 κ μ \Leftrightarrow \forall s t, MeasurableSet[m_1] s \to MeasurableSet[m_2] t \to IndepSet s t κ μ$$$
Lean4
theorem congr' {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g κ μ)
(hf : ∀ᵐ a ∂μ, f =ᵐ[κ a] f') (hg : ∀ᵐ a ∂μ, g =ᵐ[κ a] g') : IndepFun f' g' κ μ :=
by
rintro _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩
filter_upwards [hf, hg, hfg _ _ ⟨_, hA, rfl⟩ ⟨_, hB, rfl⟩] with a hf' hg' hfg'
have h1 : f ⁻¹' A =ᵐ[κ a] f' ⁻¹' A := hf'.fun_comp A
have h2 : g ⁻¹' B =ᵐ[κ a] g' ⁻¹' B := hg'.fun_comp B
rwa [← measure_congr h1, ← measure_congr h2, ← measure_congr (h1.inter h2)]
