Vanishing products of 1 - a n

For a sequence with 0 ≤ a n ≤ 1, the partial products ∏ k < n, (1 - a k) tend to zero exactly when some factor vanishes or the series ∑ a n diverges. When the series diverges, the products are squeezed below exp (-∑ k < n, a k); when it converges and no factor vanishes, they converge to a nonzero infinite product.

Main results

• Real.tendsto_prod_range_one_sub_nhds_zero_iff
• ENNReal.tendsto_prod_range_one_sub_nhds_zero_iff

theorem Real.tendsto_prod_range_one_sub_nhds_zero_iff {a : ℕ → ℝ} (h0 : ∀ (n : ℕ), 0 ≤ a n) (h1 : ∀ (n : ℕ), a n ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ∏ k ∈ Finset.range n, (1 - a k)) Filter.atTop (nhds 0) ↔ (∃ (n : ℕ), a n = 1) ∨ ¬Summable a

theorem ENNReal.tendsto_prod_range_one_sub_nhds_zero_iff {a : ℕ → ENNReal} (h1 : ∀ (n : ℕ), a n ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ∏ k ∈ Finset.range n, (1 - a k)) Filter.atTop (nhds 0) ↔ (∃ (n : ℕ), a n = 1) ∨ ∑' (n : ℕ), a n = ⊤