Sum of gaps #
This file proves that given a function g on [a, b], g b - g a can be split according to a
given finite collection of pairwise disjoint closed subintervals of [a, b]. It is the sum of two
terms:
- the sum of
g y - g xfor[x, y]in the collection, - the sum of
g y - g xfor[x, y]in the complement (modulo endpoints) of the union of the collection in[a, b].
We use Finset.intervalGapsWithin to encode the complement.
We provide the multiplication versions in Finset.prod_intervalGapsWithin_mul_prod_eq_div,
Finset.prod_intervalGapsWithin_eq_div_div_prod, and the additive versions in
Finset.sum_intervalGapsWithin_add_sum_eq_sub, Finset.sum_intervalGapsWithin_eq_sub_sub_sum.
Technically, we don't require pairwise disjointness or endpoints to be within [a, b] or even
require that a ≤ b, but it makes the most sense if they are actually satisfied.
theorem
Finset.prod_eq_prod_range_intervalGapsWithin
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[CommGroup β]
(F : Finset (α × α))
{k : ℕ}
(h : F.card = k)
{a b : α}
(f : α → α → β)
:
∏ z ∈ F, f z.1 z.2 = ∏ i ∈ range k, f (F.intervalGapsWithin h a b ↑i).2 (F.intervalGapsWithin h a b ↑i.succ).1
theorem
Finset.sum_eq_sum_range_intervalGapsWithin
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[AddCommGroup β]
(F : Finset (α × α))
{k : ℕ}
(h : F.card = k)
{a b : α}
(f : α → α → β)
:
∑ z ∈ F, f z.1 z.2 = ∑ i ∈ range k, f (F.intervalGapsWithin h a b ↑i).2 (F.intervalGapsWithin h a b ↑i.succ).1
theorem
Finset.prod_intervalGapsWithin_mul_prod_eq_div
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[CommGroup β]
(F : Finset (α × α))
{k : ℕ}
(h : F.card = k)
{a b : α}
(g : α → β)
:
(∏ i ∈ range (k + 1), g (F.intervalGapsWithin h a b ↑i).2 / g (F.intervalGapsWithin h a b ↑i).1) * ∏ z ∈ F, g z.2 / g z.1 = g b / g a
theorem
Finset.sum_intervalGapsWithin_add_sum_eq_sub
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[AddCommGroup β]
(F : Finset (α × α))
{k : ℕ}
(h : F.card = k)
{a b : α}
(g : α → β)
:
∑ i ∈ range (k + 1), (g (F.intervalGapsWithin h a b ↑i).2 - g (F.intervalGapsWithin h a b ↑i).1) + ∑ z ∈ F, (g z.2 - g z.1) = g b - g a
theorem
Finset.prod_intervalGapsWithin_eq_div_div_prod
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[CommGroup β]
(F : Finset (α × α))
{k : ℕ}
(h : F.card = k)
{a b : α}
(g : α → β)
:
∏ i ∈ range (k + 1), g (F.intervalGapsWithin h a b ↑i).2 / g (F.intervalGapsWithin h a b ↑i).1 = g b / g a / ∏ z ∈ F, g z.2 / g z.1
theorem
Finset.sum_intervalGapsWithin_eq_sub_sub_sum
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[AddCommGroup β]
(F : Finset (α × α))
{k : ℕ}
(h : F.card = k)
{a b : α}
(g : α → β)
:
∑ i ∈ range (k + 1), (g (F.intervalGapsWithin h a b ↑i).2 - g (F.intervalGapsWithin h a b ↑i).1) = g b - g a - ∑ z ∈ F, (g z.2 - g z.1)