MultipliableLems

theorem Complex.summable_nat_multipliable_one_add (f : ℕ → ℂ) (hf : Summable f) : Multipliable fun (n : ℕ) => 1 + f n

theorem term_ne_zero (z : UpperHalfPlane) (n : ℕ) : 1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z) ≠ 0

theorem ball_pow_ne_1 (x : ℂ) (hx : x ∈ Metric.ball 0 1) (n : ℕ) : 1 + (fun (n : ℕ) => -x ^ (n + 1)) n ≠ 0

theorem multipliable_lt_one (x : ℂ) (hx : x ∈ Metric.ball 0 1) : Multipliable fun (i : ℕ) => 1 - x ^ (i + 1)

theorem MultipliableEtaProductExpansion (z : UpperHalfPlane) : Multipliable fun (n : ℕ) => 1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)

theorem MultipliableEtaProductExpansion_pnat (z : UpperHalfPlane) : Multipliable fun (n : ℕ+) => 1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

theorem tprod_ne_zero (x : UpperHalfPlane) (f : ℕ → UpperHalfPlane → ℂ) (hf : ∀ (i : ℕ) (x : UpperHalfPlane), 1 + f i x ≠ 0) (hu : ∀ (x : UpperHalfPlane), Summable fun (n : ℕ) => f n x) : ∏' (i : ℕ), (1 + f i) x ≠ 0

theorem Multipliable_pow {ι : Type u_1} (f : ι → ℂ) (hf : Multipliable f) (n : ℕ) : Multipliable fun (i : ι) => f i ^ n

theorem MultipliableDeltaProductExpansion_pnat (z : UpperHalfPlane) : Multipliable fun (n : ℕ+) => (1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)) ^ 24

theorem tprod_pow (f : ℕ → ℂ) (hf : Multipliable f) (n : ℕ) : (∏' (i : ℕ), f i) ^ n = ∏' (i : ℕ), f i ^ n

theorem hasProd_le_nonneg {a₁ a₂ : ℝ} {ι : Type u_1} (f g : ι → ℝ) (h : ∀ (i : ι), f i ≤ g i) (h0 : ∀ (i : ι), 0 ≤ f i) (hf : HasProd f a₁) (hg : HasProd g a₂) : a₁ ≤ a₂

theorem HasProd.le_one_nonneg {a : ℝ} (g : ℕ → ℝ) (h : ∀ (i : ℕ), g i ≤ 1) (h0 : ∀ (i : ℕ), 0 ≤ g i) (ha : HasProd g a) : a ≤ 1

theorem one_le_tprod_nonneg (g : ℕ → ℝ) (h : ∀ (i : ℕ), g i ≤ 1) (h0 : ∀ (i : ℕ), 0 ≤ g i) : ∏' (i : ℕ), g i ≤ 1