English
For an iIndepSet f κ μ and a Finset s, almost surely the measure of the intersection equals the product of the measures for each i in s.
Русский
Для iIndepSet f κ μ и конечного множества s почти наверняка мера пересечения равна произведению мер по каждому i в s.
LaTeX
$$$\forall s, \mathrm{ae}_{μ} κ a (\bigcap_{i\in s} f_i) = \prod_{i\in s} κ a (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)),
∀ᵐ a ∂μ, κ a (⋂ i ∈ S, (f i) ⁻¹' (sets i)) = ∏ i ∈ S, κ a ((f i) ⁻¹' (sets i)) :=
by
refine ⟨fun h S sets h_meas => h _ fun i hi_mem => ⟨sets i, h_meas i hi_mem, rfl⟩, ?_⟩
intro h S setsΩ h_meas
classical
let setsβ : ∀ i : ι, Set (β i) := fun i => dite (i ∈ S) (fun hi_mem => (h_meas i hi_mem).choose) fun _ => Set.univ
have h_measβ : ∀ i ∈ S, MeasurableSet[m i] (setsβ i) :=
by
intro i hi_mem
simp_rw [setsβ, dif_pos hi_mem]
exact (h_meas i hi_mem).choose_spec.1
have h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i :=
by
intro i hi_mem
simp_rw [setsβ, dif_pos hi_mem]
exact (h_meas i hi_mem).choose_spec.2.symm
simp_all
