English
If f(b) = 1 for all b outside of a finite set s, then HasProd f (∏ b ∈ (↑s ∩ L.support).toFinset, f b) L.
Русский
Если f(b) = 1 вне конечного множества s, тогда HasProd f (произведение по (s ∩ L.support).toFinset) L.
LaTeX
$$$ \forall b \notin s, f(b)=1 \Rightarrow HasProd f (\prod_{b \in (s \cap L.support).toFinset} f(b)) L $$$
Lean4
/-- If a function `f` is `1` outside of a finite set `s`, then it `HasProd` `∏ b ∈ s, f b`. -/
@[to_additive /-- If a function `f` vanishes outside of a finite set `s`, then it `HasSum`
`∑ b ∈ s, f b`. -/
]
theorem hasProd_prod_support_of_ne_finset_one (hf : ∀ b ∈ L.support, b ∉ s → f b = 1) [L.HasSupport]
[DecidablePred (· ∈ L.support)] : HasProd f (∏ b ∈ (↑s ∩ L.support).toFinset, f b) L :=
by
apply tendsto_nhds_of_eventually_eq
have h1 : ⋂ b ∈ (↑s ∩ L.support), {s | b ∈ s} ∈ L.filter :=
(L.filter.biInter_mem (Set.toFinite _)).mpr (fun b hb ↦ hb.2)
filter_upwards [h1, L.eventually_le_support] with t ht ht'
simp only [Set.mem_iInter] at ht
apply Finset.prod_congr_of_eq_on_inter <;>
· simp only [Set.mem_toFinset]
grind
