English
For a Multipliable sequence f, HasProd f m is equivalent to the sequence of finite products tending to m along natural numbers.
Русский
Для умножаемой последовательности f: HasProd f m эквивалентно тому, что последовательность частичных произведений по натуральным числам сходится к m.
LaTeX
$$$\\text{HasProd}(f,m) \\iff \\operatorname{Tendsto}(n \\mapsto \\prod_{i=0}^{n-1} f(i))\\;\\text{atTop}\\; (\\mathcal{nhds} \\, m)$$$
Lean4
/-- You can compute a product over an encodable type by multiplying over the natural numbers and
taking a supremum. -/
@[to_additive /-- You can compute a sum over an encodable type by summing over the natural numbers
and taking a supremum. This is useful for outer measures. -/
]
theorem tprod_iSup_decode₂ [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (s : β → α) :
∏' i : ℕ, m (⨆ b ∈ decode₂ β i, s b) = ∏' b : β, m (s b) :=
by
rw [← tprod_extend_one (@encode_injective β _)]
refine tprod_congr fun n ↦ ?_
rcases em (n ∈ Set.range (encode : β → ℕ)) with ⟨a, rfl⟩ | hn
· simp [encode_injective.extend_apply]
· rw [extend_apply' _ _ _ hn]
rw [← decode₂_ne_none_iff, ne_eq, not_not] at hn
simp [hn, m0]
