Documentation

SpherePacking.ModularForms.multipliable_lems

source
theorem Complex.summable_nat_multipliable_one_add (f : ℕ → ℂ) (hf : Summable f) :
Multipliable fun (n : ℕ) => 1 + f n
source
theorem term_ne_zero (z : UpperHalfPlane) (n : ℕ) :
1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z) ≠ 0
source
theorem ball_pow_ne_1 (x : ℂ) (hx : x ∈ Metric.ball 0 1) (n : ℕ) :
1 + (fun (n : ℕ) => -x ^ (n + 1)) n ≠ 0
source
theorem multipliable_lt_one (x : ℂ) (hx : x ∈ Metric.ball 0 1) :
Multipliable fun (i : ℕ) => 1 - x ^ (i + 1)
source
theorem MultipliableEtaProductExpansion (z : UpperHalfPlane) :
Multipliable fun (n : ℕ) => 1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)
source
theorem MultipliableEtaProductExpansion_pnat (z : UpperHalfPlane) :
Multipliable fun (n : ℕ+) => 1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)
source
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
source
theorem Multipliable_pow {ι : Type u_1} (f : ι → ℂ) (hf : Multipliable f) (n : ℕ) :
Multipliable fun (i : ι) => f i ^ n
source
theorem MultipliableDeltaProductExpansion_pnat (z : UpperHalfPlane) :
Multipliable fun (n : ℕ+) => (1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)) ^ 24
source
theorem tprod_pow (f : ℕ → ℂ) (hf : Multipliable f) (n : ℕ) :
(∏' (i : ℕ), f i) ^ n = ∏' (i : ℕ), f i ^ n
source
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₂
source
theorem hasSum_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₂
source
theorem HasProd.le_one_nonneg {a : ℝ} (g : ℕ → ℝ) (h : ∀ (i : ℕ), g i ≤ 1) (h0 : ∀ (i : ℕ), 0 ≤ g i) (ha : HasProd g a) :
a ≤ 1
source
theorem HasSum.nonpos_nonneg {a : ℝ} (g : ℕ → ℝ) (h : ∀ (i : ℕ), g i ≤ 1) (h0 : ∀ (i : ℕ), 0 ≤ g i) (ha : HasProd g a) :
a ≤ 1
source
theorem one_le_tprod_nonneg (g : ℕ → ℝ) (h : ∀ (i : ℕ), g i ≤ 1) (h0 : ∀ (i : ℕ), 0 ≤ g i) :
∏' (i : ℕ), g i ≤ 1
source
theorem nonneg_tsum_nonneg (g : ℕ → ℝ) (h : ∀ (i : ℕ), g i ≤ 1) (h0 : ∀ (i : ℕ), 0 ≤ g i) :
∏' (i : ℕ), g i ≤ 1