iIndepFun_iff_measure_inter_preimage_eq_mul

English

If f is an iIndepFun and g_i are measurable, then the composed family iIndepFun with g_i ∘ f_i is independent.

Русский

Если f образует независимое семейство и каждый g_i измерим, тогда композиция g_i ∘ f_i образует независимое семейство.

LaTeX

$$$iIndepFun f μ \Rightarrow (g_i) \text{ измерим } \Rightarrow iIndepFun (i \mapsto g_i \circ f_i) μ$$$

Lean4

theorem iIndepFun_iff_measure_inter_preimage_eq_mul {ι : Type*} {β : ι → Type*} {m : ∀ x, MeasurableSpace (β x)}
    {f : ∀ i, Ω → β i} :
    iIndepFun f μ ↔
      ∀ (S : Finset ι) {sets : ∀ i : ι, Set (β i)} (_H : ∀ i, i ∈ S → MeasurableSet[m i] (sets i)),
        μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i) :=
  by
  simp only [iIndepFun, Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]

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