English
Independence of functions f and g with respect to a kernel κ μ is equivalent to the statement that for all measurable sets S, T, the measure of the preimages under f and g intersecting equals the product of the measures of the preimages.
Русский
Независимость функций f и g относительно κ μ эквивалентна тому, что для всех измеримых множеств S, T мера пересечения их образов равна произведению мер preimage.
LaTeX
$$$IndepFun f g κ μ \Leftrightarrow \forall S,T, MeasurableSet S → MeasurableSet T → \forall^* a\, κ a (f^{-1}(S) ∩ g^{-1}(T)) = κ a(f^{-1}(S)) · κ a(g^{-1}(T))$$$
Lean4
theorem indepSet_of_measurableSet {m₁ m₂ _ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
(h_indep : Indep m₁ m₂ κ μ) {s t : Set Ω} (hs : MeasurableSet[m₁] s) (ht : MeasurableSet[m₂] t) :
IndepSet s t κ μ := by
refine fun s' t' hs' ht' => h_indep s' t' ?_ ?_
·
induction s', hs' using generateFrom_induction with
| hC t ht => exact ht ▸ hs
| empty => exact @MeasurableSet.empty _ m₁
| compl u _ hu => exact hu.compl
| iUnion f _ hf => exact .iUnion hf
·
induction t', ht' using generateFrom_induction with
| hC s hs => exact hs ▸ ht
| empty => exact @MeasurableSet.empty _ m₂
| compl u _ hu => exact hu.compl
| iUnion f _ hf => exact .iUnion hf
