condExp_indicator_filtrationOfSet_ae_eq

English

If a family of measurable maps is independent, then the comapped sigma-algebras along a natural filtration are independent as well.

Русский

Если множество взаимно независимых отображений, то их сопряженные сигма-алгебры через естественную фильтрацию независимы.

LaTeX

$$$$\forall f,\; (hf) \;\Rightarrow \; Indep (MeasurableSpace.comap (f j) mβ) (Filtration.natural f hf i) μ.$$$

Lean4

theorem condExp_indicator_filtrationOfSet_ae_eq (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s μ) (hij : i < j) :
    μ[(s j).indicator (fun _ => 1 : Ω → ℝ)|filtrationOfSet hsm i] =ᵐ[μ] fun _ => μ.real (s j) :=
  by
  rw [Filtration.filtrationOfSet_eq_natural (β := ℝ) hsm]
  refine (iIndepFun.condExp_natural_ae_eq_of_lt _ hs.iIndepFun_indicator hij).trans ?_
  simp only [integral_indicator_const _ (hsm _), Algebra.id.smul_eq_mul, mul_one]; rfl

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