English
If HasProd f c holds, and s is finite with f(a) ≠ 0 for a in s, and f(a) = g(a) for a ∉ s, then HasProd g with updated constant c · ((∏ i∈s g i) / (∏ i∈s f i)).
Русский
Если имеет место HasProd f c, и множество s конечно такое, что f(a) ≠ 0 для a в s, и f(a) = g(a) для a не в s, тогда HasProd g с обновленной константой c · ((∏ i∈s g i) / (∏ i∈s f i)).
LaTeX
$$$$\text{HasProd } f c \rightarrow \\forall s, (\forall a \in s, f(a) \neq 0) \rightarrow (\forall a \notin s, f(a) = g(a)) \rightarrow \text{HasProd } g\left(c \cdot \frac{\prod_{i\in s} g(i)}{\prod_{i\in s} f(i)}\right). $$$$
Lean4
theorem congr_cofinite₀ {c : K} (hc : HasProd f c) {s : Finset α} (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) :
HasProd g (c * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)) := by
classical
refine (Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_
filter_upwards [eventually_ge_atTop s] with t ht
calc
(∏ i ∈ t, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
_ = ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * _ := by
conv_lhs =>
rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff, prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]
_ = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i :=
by
rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
exact prod_ne_zero_iff.mpr hs
_ = ∏ i ∈ t, g i := by rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]
