English
A variant formulation of iIndepSets singleton criterion using the product over a finite index set.
Русский
Вариант формулировки для iIndepSets singleton с использованием произведения по конечному индексу.
LaTeX
$$iIndepSets (fun i ↦ {s i}) κ μ ↔ ∀ S : Finset ι, ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, s i) = ∏ i ∈ S, κ a (s i)$$
Lean4
theorem indepSets {s : ι → Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
(h_indep : iIndepSets s κ μ) {i j : ι} (hij : i ≠ j) : IndepSets (s i) (s j) κ μ := by
classical
intro t₁ t₂ ht₁ ht₂
have hf_m : ∀ x : ι, x ∈ ({ i, j } : Finset ι) → ite (x = i) t₁ t₂ ∈ s x :=
by
intro x hx
rcases Finset.mem_insert.mp hx with hx | hx
· simp [hx, ht₁]
· simp [Finset.mem_singleton.mp hx, hij.symm, ht₂]
have h1 : t₁ = ite (i = i) t₁ t₂ := by simp only [if_true]
have h2 : t₂ = ite (j = i) t₁ t₂ := by simp only [hij.symm, if_false]
have h_inter : ⋂ (t : ι) (_ : t ∈ ({ i, j } : Finset ι)), ite (t = i) t₁ t₂ = ite (i = i) t₁ t₂ ∩ ite (j = i) t₁ t₂ :=
by simp only [Finset.set_biInter_singleton, Finset.set_biInter_insert]
filter_upwards [h_indep { i, j } hf_m] with a h_indep'
have h_prod :
(∏ t ∈ ({ i, j } : Finset ι), κ a (ite (t = i) t₁ t₂)) = κ a (ite (i = i) t₁ t₂) * κ a (ite (j = i) t₁ t₂) := by
simp only [hij, Finset.prod_singleton, Finset.prod_insert, not_false_iff, Finset.mem_singleton]
grind
