indepFun_iff_indepSet_preimage — Mathlib

English

If f_i and g_i are a.e.-equal modulo κ a for all i, then iIndepFun f κ μ iff iIndepFun g κ μ.

Русский

Если f_i и g_i совпадают почти наверняка по модулю κ a для каждого i, то iIndepFun f κ μ эквивалентно iIndepFun g κ μ.

LaTeX

$$$iIndepFun f κ μ \Leftrightarrow iIndepFun g κ μ$ under a.e.-equivalence.$$

Lean4

theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [IsZeroOrMarkovKernel κ]
    (hf : Measurable f) (hg : Measurable g) :
    IndepFun f g κ μ ↔ ∀ s t, MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ :=
  by
  refine indepFun_iff_measure_inter_preimage_eq_mul.trans ?_
  constructor <;> intro h s t hs ht <;> specialize h s t hs ht
  · rwa [indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ]
  · rwa [← indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ]

Похожие утверждения