English
Let f_i: Ω → β be a family such that f_i is AE-measurable with respect to κ ∘ μ and κ a kernel. If the family is independent in the iIndepFun sense and each f_i is AE-measurable, then for any finite s and i ∉ s, IndepFun (∏ j∈s f_j) (f_i) κ μ.
Русский
Пусть f_i: Ω → β — семейство, для которого каждый f_i имеет AE-измеримость относительно κ ∘ μ, и семейство независимо в смысле iIndepFun. Тогда для любого конечного подмножества s и любого i, не принадлежащего s, независимость выполняется: IndepFun (∏_{j∈s} f_j) (f_i) κ μ.
LaTeX
$$$\\text{IndepFun}\\left(\\prod_{j \\in s} (f_j)\\right)\\left(f_i\\right)\\kappa\\mu$$$
Lean4
@[to_additive]
theorem indepFun_finset_prod_of_notMem₀ (hf_Indep : iIndepFun f κ μ) (hf_meas : ∀ i, AEMeasurable (f i) (κ ∘ₘ μ))
{s : Finset ι} {i : ι} (hi : i ∉ s) : IndepFun (∏ j ∈ s, f j) (f i) κ μ :=
by
have h : IndepFun (∏ j ∈ s, (hf_meas j).mk (f j)) ((hf_meas i).mk (f i)) κ μ :=
by
refine iIndepFun.indepFun_finset_prod_of_notMem ?_ (fun i ↦ (hf_meas i).measurable_mk) hi
exact iIndepFun.congr' hf_Indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
refine IndepFun.congr' h ?_ ?_
· have : ∀ᵐ a ∂μ, ∀ (i : s), f i =ᵐ[κ a] (hf_meas i).mk :=
by
rw [ae_all_iff]
exact fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
filter_upwards [this] with a ha
filter_upwards [ae_all_iff.2 ha] with ω hω
simp only [Finset.prod_apply]
exact Finset.prod_congr rfl fun i hi ↦ (hω ⟨i, hi⟩).symm
· exact Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk.symm
