HepLean Documentation

Mathlib.Data.Complex.BigOperators

Finite sums and products of complex numbers #

source
@[simp]
theorem Complex.ofReal_prod {α : Type u_1} (s : Finset α) (f : α → ℝ) :
↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
source
@[simp]
theorem Complex.ofReal_sum {α : Type u_1} (s : Finset α) (f : α → ℝ) :
↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
source
@[simp]
theorem Complex.ofReal_expect {α : Type u_1} (s : Finset α) (f : α → ℝ) :
↑(s.expect fun (i : α) => f i) = s.expect fun (i : α) => ↑(f i)
source
@[simp]
theorem Complex.ofReal_balance {α : Type u_1} [Fintype α] (f : α → ℝ) (a : α) :
↑(Fintype.balance f a) = Fintype.balance (Complex.ofReal ∘ f) a
source
@[simp]
theorem Complex.ofReal_comp_balance {ι : Type u_2} [Fintype ι] (f : ι → ℝ) :
Complex.ofReal ∘ Fintype.balance f = Fintype.balance (Complex.ofReal ∘ f)
source
@[simp]
theorem Complex.re_sum {α : Type u_1} (s : Finset α) (f : α → ℂ) :
(∑ i ∈ s, f i).re = ∑ i ∈ s, (f i).re
source
@[simp]
theorem Complex.re_expect {α : Type u_1} (s : Finset α) (f : α → ℂ) :
(s.expect fun (i : α) => f i).re = s.expect fun (i : α) => (f i).re
source
@[simp]
theorem Complex.re_balance {α : Type u_1} [Fintype α] (f : α → ℂ) (a : α) :
(Fintype.balance f a).re = Fintype.balance (Complex.re ∘ f) a
source
@[simp]
theorem Complex.re_comp_balance {ι : Type u_2} [Fintype ι] (f : ι → ℂ) :
Complex.re ∘ Fintype.balance f = Fintype.balance (Complex.re ∘ f)
source
@[simp]
theorem Complex.im_sum {α : Type u_1} (s : Finset α) (f : α → ℂ) :
(∑ i ∈ s, f i).im = ∑ i ∈ s, (f i).im
source
@[simp]
theorem Complex.im_expect {α : Type u_1} (s : Finset α) (f : α → ℂ) :
(s.expect fun (i : α) => f i).im = s.expect fun (i : α) => (f i).im
source
@[simp]
theorem Complex.im_balance {α : Type u_1} [Fintype α] (f : α → ℂ) (a : α) :
(Fintype.balance f a).im = Fintype.balance (Complex.im ∘ f) a
source
@[simp]
theorem Complex.im_comp_balance {ι : Type u_2} [Fintype ι] (f : ι → ℂ) :
Complex.im ∘ Fintype.balance f = Fintype.balance (Complex.im ∘ f)