English
Let γ : β → Type and f : (Σ b, γ b) → α, g : β → α, a ∈ α. If for every b HasProd (λ c, f⟨b, c⟩) (g b) and HasProd g a, and the finite partial products ∏ i ∈ s f i form a Cauchy sequence, then HasProd f a. This is a sigma-decomposition criterion for products.
Русский
Пусть γ : β → Type, f : (Σ b, γ b) → α, g : β → α и a ∈ α. Если для каждого b имеет место HasProd (λ c, f⟨b, c⟩) (g b), и HasProd g a, и последовательность частичных произведений ∏ i∈s f i является последовательностью Коши, тогда HasProd f a. Это критерий по сигма-разложению для произведений.
LaTeX
$$$$ \text{If } \forall b, \mathrm{HasProd}(\lambda c, f\langle b,c\rangle)(g b) \text{ and } \mathrm{HasProd}(g,a) \text{ and } h: \text{CauchySeq}(s \mapsto \prod_{i\in s} f i), \text{then } \mathrm{HasProd}(f,a). $$$$
Lean4
@[to_additive]
theorem of_sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α}
(hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hg : HasProd g a)
(h : CauchySeq (fun (s : Finset (Σ b : β, γ b)) ↦ ∏ i ∈ s, f i)) : HasProd f a := by
classical
apply le_nhds_of_cauchy_adhp h
simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, frequently_atTop, ge_iff_le, le_eq_subset]
intro u hu s
rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
obtain ⟨t0, st0, ht0⟩ : ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ s.image Sigma.fst ⊆ t0 :=
by
have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)
exact (A.and (Ici_mem_atTop _)).exists
have L : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ t0, f p) atTop (𝓝 <| ∏ b ∈ t0, g b) :=
by
simp only [← sigma_preimage_mk, prod_sigma]
refine tendsto_finset_prod _ fun b _ ↦ ?_
change Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
have : ∃ t, ∏ p ∈ t with p.1 ∈ t0, f p ∈ v ∧ s ⊆ t :=
((Tendsto.eventually_mem L (v_open.mem_nhds st0)).and (Ici_mem_atTop _)).exists
obtain ⟨t, tv, st⟩ := this
refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩
simpa only [mem_filter, st hx, true_and] using ht0 (mem_image_of_mem Sigma.fst hx)
