Documentation

Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Big operators indexed by intervals #

This file proves lemmas about ∏ x ∈ Ixx a b, f x and ∑ x ∈ Ixx a b, f x.

source
theorem Finset.mul_prod_Ico_eq_prod_Icc {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x
source
theorem Finset.add_sum_Ico_eq_sum_Icc {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
f b + ∑ x ∈ Ico a b, f x = ∑ x ∈ Icc a b, f x
source
@[deprecated Finset.mul_prod_Ico_eq_prod_Icc (since := "2025-05-03")]
theorem Finset.right_mul_prod_Ico {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Alias of Finset.mul_prod_Ico_eq_prod_Icc.

source
@[deprecated Finset.add_sum_Ico_eq_sum_Icc (since := "2025-05-03")]
theorem Finset.right_add_sum_Ico {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
f b + ∑ x ∈ Ico a b, f x = ∑ x ∈ Icc a b, f x

Alias of Finset.add_sum_Ico_eq_sum_Icc.

source
theorem Finset.prod_Ico_mul_eq_prod_Icc {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
(∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x
source
theorem Finset.sum_Ico_add_eq_sum_Icc {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
∑ x ∈ Ico a b, f x + f b = ∑ x ∈ Icc a b, f x
source
@[deprecated Finset.prod_Ico_mul_eq_prod_Icc (since := "2025-05-03")]
theorem Finset.prod_Ico_mul_right {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
(∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

Alias of Finset.prod_Ico_mul_eq_prod_Icc.

source
@[deprecated Finset.sum_Ico_add_eq_sum_Icc (since := "2025-05-03")]
theorem Finset.sum_Ico_add_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
∑ x ∈ Ico a b, f x + f b = ∑ x ∈ Icc a b, f x

Alias of Finset.sum_Ico_add_eq_sum_Icc.

source
theorem Finset.mul_prod_Ioc_eq_prod_Icc {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x
source
theorem Finset.add_sum_Ioc_eq_sum_Icc {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
f a + ∑ x ∈ Ioc a b, f x = ∑ x ∈ Icc a b, f x
source
@[deprecated Finset.mul_prod_Ioc_eq_prod_Icc (since := "2025-05-03")]
theorem Finset.left_mul_prod_Ioc {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

Alias of Finset.mul_prod_Ioc_eq_prod_Icc.

source
@[deprecated Finset.add_sum_Ioc_eq_sum_Icc (since := "2025-05-03")]
theorem Finset.left_add_sum_Ioc {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
f a + ∑ x ∈ Ioc a b, f x = ∑ x ∈ Icc a b, f x

Alias of Finset.add_sum_Ioc_eq_sum_Icc.

source
theorem Finset.prod_Ioc_mul_eq_prod_Icc {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
(∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x
source
theorem Finset.sum_Ioc_add_eq_sum_Icc {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
∑ x ∈ Ioc a b, f x + f a = ∑ x ∈ Icc a b, f x
source
@[deprecated Finset.prod_Ioc_mul_eq_prod_Icc (since := "2025-05-03")]
theorem Finset.prod_Ioc_mul_left {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
(∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x

Alias of Finset.prod_Ioc_mul_eq_prod_Icc.

source
@[deprecated Finset.sum_Ioc_add_eq_sum_Icc (since := "2025-05-03")]
theorem Finset.sum_Ioc_add_left {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a ≤ b) :
∑ x ∈ Ioc a b, f x + f a = ∑ x ∈ Icc a b, f x

Alias of Finset.sum_Ioc_add_eq_sum_Icc.

source
theorem Finset.mul_prod_Ioo_eq_prod_Ico {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x
source
theorem Finset.add_sum_Ioo_eq_sum_Ico {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
f a + ∑ x ∈ Ioo a b, f x = ∑ x ∈ Ico a b, f x
source
@[deprecated Finset.mul_prod_Ioo_eq_prod_Ico (since := "2025-05-03")]
theorem Finset.left_mul_prod_Ioo {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x

Alias of Finset.mul_prod_Ioo_eq_prod_Ico.

source
@[deprecated Finset.add_sum_Ioo_eq_sum_Ico (since := "2025-05-03")]
theorem Finset.left_add_sum_Ioo {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
f a + ∑ x ∈ Ioo a b, f x = ∑ x ∈ Ico a b, f x

Alias of Finset.add_sum_Ioo_eq_sum_Ico.

source
theorem Finset.prod_Ioo_mul_eq_prod_Ico {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
(∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x
source
theorem Finset.sum_Ioo_add_eq_sum_Ico {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
∑ x ∈ Ioo a b, f x + f a = ∑ x ∈ Ico a b, f x
source
@[deprecated Finset.prod_Ioo_mul_eq_prod_Ico (since := "2025-05-03")]
theorem Finset.prod_Ioo_mul_left {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
(∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x

Alias of Finset.prod_Ioo_mul_eq_prod_Ico.

source
@[deprecated Finset.sum_Ioo_add_eq_sum_Ico (since := "2025-05-03")]
theorem Finset.sum_Ioo_add_left {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
∑ x ∈ Ioo a b, f x + f a = ∑ x ∈ Ico a b, f x

Alias of Finset.sum_Ioo_add_eq_sum_Ico.

source
theorem Finset.mul_prod_Ioo_eq_prod_Ioc {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x
source
theorem Finset.add_sum_Ioo_eq_sum_Ioc {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
f b + ∑ x ∈ Ioo a b, f x = ∑ x ∈ Ioc a b, f x
source
@[deprecated Finset.mul_prod_Ioo_eq_prod_Ioc (since := "2025-05-03")]
theorem Finset.right_mul_prod_Ioo {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x

Alias of Finset.mul_prod_Ioo_eq_prod_Ioc.

source
@[deprecated Finset.add_sum_Ioo_eq_sum_Ioc (since := "2025-05-03")]
theorem Finset.right_add_sum_Ioo {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
f b + ∑ x ∈ Ioo a b, f x = ∑ x ∈ Ioc a b, f x

Alias of Finset.add_sum_Ioo_eq_sum_Ioc.

source
theorem Finset.prod_Ioo_mul_eq_prod_Ioc {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
(∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x
source
theorem Finset.sum_Ioo_add_eq_sum_Ioc {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
∑ x ∈ Ioo a b, f x + f b = ∑ x ∈ Ioc a b, f x
source
@[deprecated Finset.prod_Ioo_mul_eq_prod_Ioc (since := "2025-05-03")]
theorem Finset.prod_Ioo_mul_right {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
(∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x

Alias of Finset.prod_Ioo_mul_eq_prod_Ioc.

source
@[deprecated Finset.sum_Ioo_add_eq_sum_Ioc (since := "2025-05-03")]
theorem Finset.sum_Ioo_add_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) :
∑ x ∈ Ioo a b, f x + f b = ∑ x ∈ Ioc a b, f x

Alias of Finset.sum_Ioo_add_eq_sum_Ioc.

source
theorem Finset.prod_eq_prod_Ico_succ_bot {M : Type u_2} [CommMonoid M] {a b : ℕ} (hab : a < b) (f : ℕ → M) :
∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k
source
theorem Finset.sum_eq_sum_Ico_succ_bot {M : Type u_2} [AddCommMonoid M] {a b : ℕ} (hab : a < b) (f : ℕ → M) :
∑ k ∈ Ico a b, f k = f a + ∑ k ∈ Ico (a + 1) b, f k
source
theorem Finset.mul_prod_Ioi_eq_prod_Ici {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x
source
theorem Finset.add_sum_Ioi_eq_sum_Ici {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
f a + ∑ x ∈ Ioi a, f x = ∑ x ∈ Ici a, f x
source
@[deprecated Finset.mul_prod_Ioi_eq_prod_Ici (since := "2025-05-03")]
theorem Finset.left_mul_prod_Ioi {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x

Alias of Finset.mul_prod_Ioi_eq_prod_Ici.

source
@[deprecated Finset.add_sum_Ioi_eq_sum_Ici (since := "2025-05-03")]
theorem Finset.left_add_sum_Ioi {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
f a + ∑ x ∈ Ioi a, f x = ∑ x ∈ Ici a, f x

Alias of Finset.add_sum_Ioi_eq_sum_Ici.

source
theorem Finset.prod_Ioi_mul_eq_prod_Ici {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
(∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x
source
theorem Finset.sum_Ioi_add_eq_sum_Ici {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
∑ x ∈ Ioi a, f x + f a = ∑ x ∈ Ici a, f x
source
@[deprecated Finset.prod_Ioi_mul_eq_prod_Ici (since := "2025-05-03")]
theorem Finset.prod_Ioi_mul_left {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
(∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x

Alias of Finset.prod_Ioi_mul_eq_prod_Ici.

source
@[deprecated Finset.sum_Ioi_add_eq_sum_Ici (since := "2025-05-03")]
theorem Finset.sum_Ioi_add_left {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
∑ x ∈ Ioi a, f x + f a = ∑ x ∈ Ici a, f x

Alias of Finset.sum_Ioi_add_eq_sum_Ici.

source
theorem Finset.mul_prod_Iio_eq_prod_Iic {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) :
f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x
source
theorem Finset.add_sum_Iio_eq_sum_Iic {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) :
f a + ∑ x ∈ Iio a, f x = ∑ x ∈ Iic a, f x
source
@[deprecated Finset.mul_prod_Iio_eq_prod_Iic (since := "2025-05-03")]
theorem Finset.right_mul_prod_Iio {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) :
f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x

Alias of Finset.mul_prod_Iio_eq_prod_Iic.

source
@[deprecated Finset.add_sum_Iio_eq_sum_Iic (since := "2025-05-03")]
theorem Finset.right_add_sum_Iio {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) :
f a + ∑ x ∈ Iio a, f x = ∑ x ∈ Iic a, f x

Alias of Finset.add_sum_Iio_eq_sum_Iic.

source
theorem Finset.prod_Iio_mul_eq_prod_Iic {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) :
(∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x
source
theorem Finset.sum_Iio_add_eq_sum_Iic {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) :
∑ x ∈ Iio a, f x + f a = ∑ x ∈ Iic a, f x
source
@[deprecated Finset.prod_Iio_mul_eq_prod_Iic (since := "2025-05-03")]
theorem Finset.prod_Iio_mul_right {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) :
(∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x

Alias of Finset.prod_Iio_mul_eq_prod_Iic.

source
@[deprecated Finset.sum_Iio_add_eq_sum_Iic (since := "2025-05-03")]
theorem Finset.sum_Iio_add_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) :
∑ x ∈ Iio a, f x + f a = ∑ x ∈ Iic a, f x

Alias of Finset.sum_Iio_add_eq_sum_Iic.

source
theorem Finset.sum_Ico_add_eq_sum_Ico_add_one {α : Type u_1} {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [AddMonoidWithOne α] [SuccAddOrder α] [NoMaxOrder α] {M : Type u_3} [AddCommMonoid M] (hab : a ≤ b) (f : α → M) :
∑ x ∈ Ico a b, f x + f b = ∑ x ∈ Ico a (b + 1), f x
source
theorem Finset.prod_Ico_mul_eq_prod_Ico_add_one {α : Type u_1} {M : Type u_2} [CommMonoid M] {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [AddMonoidWithOne α] [SuccAddOrder α] [NoMaxOrder α] (hab : a ≤ b) (f : α → M) :
(∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Ico a (b + 1), f x
source
theorem Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag {α : Type u_1} {M : Type u_2} [CommMonoid M] [LinearOrder α] [Fintype α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (f : α → α → M) :
∏ i : α, ∏ j ∈ Ioi i, f j i * f i j = ∏ i : α, ∏ j ∈ {i}ᶜ, f j i
source
theorem Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [LinearOrder α] [Fintype α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (f : α → α → M) :
∑ i : α, ∑ j ∈ Ioi i, (f j i + f i j) = ∑ i : α, ∑ j ∈ {i}ᶜ, f j i