English
Under bottom filter, the unconditional product equals the finite product over the support, when the support is finite; otherwise it equals 1.
Русский
При нижнем фильтре произведение по L равно конечному произведению по опоре, если опора конечна; иначе — единице.
LaTeX
$$$ tprod f L = finprod (f) \text{ over } L.support \text{ when support finite; else } 1 $$$
Lean4
/-- If the summation filter is the trivial filter `⊥`, then the topological product is equal to the
finite product (which is taken to be 1 if the multiplicative support of `f` is infinite).
Note that in this case `HasProd f a` is satisfied for *every* element `a` of the target, so the
value assigned to the `tprod` is a question of conventions. -/
@[to_additive /-- If the summation filter is the trivial filter `⊥`, then the topological sum is
equal to the finite sum (which is taken to be 1 if the support of `f` is infinite).
Note that in this case `HasSum f a` is satisfied for *every* element `a` of the target, so the
value assigned to the `tsum` is a question of conventions. -/
]
theorem tprod_bot (hL : ¬L.NeBot) (f : β → α) : ∏'[L] b, f b = ∏ᶠ b, f b :=
by
simp only [tprod_def, dif_pos (multipliable_bot hL f)]
haveI : L.LeAtTop := L.leAtTop_of_not_NeBot hL
rw [L.support_eq_univ, Set.inter_univ, Set.mulIndicator_univ]
by_cases hf : (mulSupport f).Finite
· rw [eq_true_intro hf, if_pos]
simp only [and_true]
infer_instance
· rwa [if_neg (by tauto), if_pos (hasProd_bot hL _ _), finprod_of_infinite_mulSupport]
