feat(library/algebra/ring_bigops): make start on file with more properties of sums and products
This commit is contained in:
Jeremy Avigad
parent
0e3b13f1a0
commit
baf11d0018
5 changed files with 248 additions and 55 deletions
|
|
@ -18,5 +18,6 @@ Algebraic structures.
|
|||
* [field](field.lean)
|
||||
* [ordered_field](ordered_field.lean)
|
||||
* [ring_power](ring_power.lean) : power in ring structures
|
||||
* [ring_bigops](ring_bigops.lean) : products and sums in various structures
|
||||
* [bundled](bundled.lean) : bundled versions of the algebraic structures
|
||||
* [category](category/category.md) : category theory (outdated, see HoTT category theory folder)
|
||||
|
|
|
|||
|
|
@ -104,6 +104,46 @@ section comm_monoid
|
|||
by rewrite [*Prodl_cons, IH, *mul.assoc, mul.left_comm (Prodl l f)])
|
||||
end comm_monoid
|
||||
|
||||
/- Suml: sum indexed by a list -/
|
||||
|
||||
section add_monoid
|
||||
variable [amB : add_monoid B]
|
||||
include amB
|
||||
local attribute add_monoid.to_monoid [trans_instance]
|
||||
|
||||
definition Suml (l : list A) (f : A → B) : B := Prodl l f
|
||||
|
||||
-- ∑ x ← l, f x
|
||||
notation `∑` binders `←` l, r:(scoped f, Suml l f) := r
|
||||
|
||||
theorem Suml_nil (f : A → B) : Suml [] f = 0 := Prodl_nil f
|
||||
theorem Suml_cons (f : A → B) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f :=
|
||||
Prodl_cons f a l
|
||||
theorem Suml_append (l₁ l₂ : list A) (f : A → B) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f :=
|
||||
Prodl_append l₁ l₂ f
|
||||
|
||||
section deceqA
|
||||
include deceqA
|
||||
theorem Suml_insert_of_mem (f : A → B) {a : A} {l : list A} (H : a ∈ l) :
|
||||
Suml (insert a l) f = Suml l f := Prodl_insert_of_mem f H
|
||||
theorem Suml_insert_of_not_mem (f : A → B) {a : A} {l : list A} (H : a ∉ l) :
|
||||
Suml (insert a l) f = f a + Suml l f := Prodl_insert_of_not_mem f H
|
||||
theorem Suml_union {l₁ l₂ : list A} (f : A → B) (d : disjoint l₁ l₂) :
|
||||
Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := Prodl_union f d
|
||||
end deceqA
|
||||
|
||||
theorem Suml_zero (l : list A) : Suml l (λ x, 0) = (0:B) := Prodl_one l
|
||||
end add_monoid
|
||||
|
||||
section add_comm_monoid
|
||||
variable [acmB : add_comm_monoid B]
|
||||
include acmB
|
||||
local attribute add_comm_monoid.to_comm_monoid [trans_instance]
|
||||
|
||||
theorem Suml_add (l : list A) (f g : A → B) : Suml l (λx, f x + g x) = Suml l f + Suml l g :=
|
||||
Prodl_mul l f g
|
||||
end add_comm_monoid
|
||||
|
||||
/-
|
||||
-- finset versions
|
||||
-/
|
||||
|
|
@ -172,45 +212,7 @@ namespace finset
|
|||
quot.induction_on s (take u, !Prodl_one)
|
||||
end finset
|
||||
|
||||
section add_monoid
|
||||
variable [amB : add_monoid B]
|
||||
include amB
|
||||
local attribute add_monoid.to_monoid [trans_instance]
|
||||
|
||||
definition Suml (l : list A) (f : A → B) : B := Prodl l f
|
||||
|
||||
-- ∑ x ← l, f x
|
||||
notation `∑` binders `←` l, r:(scoped f, Suml l f) := r
|
||||
|
||||
theorem Suml_nil (f : A → B) : Suml [] f = 0 := Prodl_nil f
|
||||
theorem Suml_cons (f : A → B) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f :=
|
||||
Prodl_cons f a l
|
||||
theorem Suml_append (l₁ l₂ : list A) (f : A → B) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f :=
|
||||
Prodl_append l₁ l₂ f
|
||||
|
||||
section deceqA
|
||||
include deceqA
|
||||
theorem Suml_insert_of_mem (f : A → B) {a : A} {l : list A} (H : a ∈ l) :
|
||||
Suml (insert a l) f = Suml l f := Prodl_insert_of_mem f H
|
||||
theorem Suml_insert_of_not_mem (f : A → B) {a : A} {l : list A} (H : a ∉ l) :
|
||||
Suml (insert a l) f = f a + Suml l f := Prodl_insert_of_not_mem f H
|
||||
theorem Suml_union {l₁ l₂ : list A} (f : A → B) (d : disjoint l₁ l₂) :
|
||||
Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := Prodl_union f d
|
||||
end deceqA
|
||||
|
||||
theorem Suml_zero (l : list A) : Suml l (λ x, 0) = (0:B) := Prodl_one l
|
||||
end add_monoid
|
||||
|
||||
section add_comm_monoid
|
||||
variable [acmB : add_comm_monoid B]
|
||||
include acmB
|
||||
local attribute add_comm_monoid.to_comm_monoid [trans_instance]
|
||||
|
||||
theorem Suml_add (l : list A) (f g : A → B) : Suml l (λx, f x + g x) = Suml l f + Suml l g :=
|
||||
Prodl_mul l f g
|
||||
end add_comm_monoid
|
||||
|
||||
/- Sum -/
|
||||
/- Sum: sum indexed by a finset -/
|
||||
|
||||
namespace finset
|
||||
variable [acmB : add_comm_monoid B]
|
||||
|
|
@ -257,7 +259,7 @@ section Prod
|
|||
noncomputable definition Prod (s : set A) (f : A → B) : B := finset.Prod (to_finset s) f
|
||||
|
||||
-- ∏ x ∈ s, f x
|
||||
notation `∏` binders `∈` s, r:(scoped f, prod s f) := r
|
||||
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
|
||||
|
||||
theorem Prod_empty (f : A → B) : Prod ∅ f = 1 :=
|
||||
by rewrite [↑Prod, to_finset_empty]
|
||||
|
|
@ -304,7 +306,7 @@ section Prod
|
|||
by rewrite [↑Prod, finset.Prod_one]
|
||||
end Prod
|
||||
|
||||
/- Sum -/
|
||||
/- Sum: sum indexed by a set -/
|
||||
|
||||
section Sum
|
||||
variable [acmB : add_comm_monoid B]
|
||||
|
|
@ -313,6 +315,8 @@ section Sum
|
|||
|
||||
noncomputable definition Sum (s : set A) (f : A → B) : B := Prod s f
|
||||
|
||||
proposition Sum_def (s : set A) (f : A → B) : Sum s f = finset.Sum (to_finset s) f := rfl
|
||||
|
||||
-- ∑ x ∈ s, f x
|
||||
notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r
|
||||
|
||||
|
|
|
|||
184
library/algebra/ring_bigops.lean
Normal file
184
library/algebra/ring_bigops.lean
Normal file
|
|
@ -0,0 +1,184 @@
|
|||
/-
|
||||
Copyright (c) 2015 Jeremy Avigad. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Jeremy Avigad
|
||||
|
||||
Properties of finite sums and products in various structures, including ordered rings and fields.
|
||||
There are two versions of every theorem: one for finsets, and one for finite sets.
|
||||
-/
|
||||
import .group_bigops .ordered_field
|
||||
|
||||
variables {A B : Type}
|
||||
variable [deceqA : decidable_eq A]
|
||||
|
||||
/-
|
||||
-- finset versions
|
||||
-/
|
||||
|
||||
namespace finset
|
||||
|
||||
section comm_semiring
|
||||
variable [csB : comm_semiring B]
|
||||
include deceqA csB
|
||||
|
||||
proposition mul_Sum (f : A → B) {s : finset A} (b : B) :
|
||||
b * (∑ x ∈ s, f x) = ∑ x ∈ s, b * f x :=
|
||||
begin
|
||||
induction s with a s ans ih,
|
||||
{rewrite [+Sum_empty, mul_zero]},
|
||||
rewrite [Sum_insert_of_not_mem f ans, Sum_insert_of_not_mem (λ x, b * f x) ans],
|
||||
rewrite [-ih, left_distrib]
|
||||
end
|
||||
|
||||
proposition Sum_mul (f : A → B) {s : finset A} (b : B) :
|
||||
(∑ x ∈ s, f x) * b = ∑ x ∈ s, f x * b :=
|
||||
by rewrite [mul.comm _ b, mul_Sum]; apply Sum_ext; intros; apply mul.comm
|
||||
|
||||
proposition Prod_eq_zero (f : A → B) {s : finset A} {a : A} (H : a ∈ s) (fa0 : f a = 0) :
|
||||
(∏ x ∈ s, f x) = 0 :=
|
||||
begin
|
||||
induction s with b s bns ih,
|
||||
{exact absurd H !not_mem_empty},
|
||||
rewrite [Prod_insert_of_not_mem f bns],
|
||||
have a = b ∨ a ∈ s, from eq_or_mem_of_mem_insert H,
|
||||
cases this with aeqb ains,
|
||||
{rewrite [-aeqb, fa0, zero_mul]},
|
||||
rewrite [ih ains, mul_zero]
|
||||
end
|
||||
end comm_semiring
|
||||
|
||||
section ordered_comm_group
|
||||
variable [ocgB : ordered_comm_group B]
|
||||
include deceqA ocgB
|
||||
|
||||
proposition Sum_le_Sum (f g : A → B) {s : finset A} (H: ∀ x, x ∈ s → f x ≤ g x) :
|
||||
(∑ x ∈ s, f x) ≤ (∑ x ∈ s, g x) :=
|
||||
begin
|
||||
induction s with a s ans ih,
|
||||
{exact le.refl _},
|
||||
have H1 : f a ≤ g a, from H _ !mem_insert,
|
||||
have H2 : (∑ x ∈ s, f x) ≤ (∑ x ∈ s, g x), from ih (forall_of_forall_insert H),
|
||||
rewrite [Sum_insert_of_not_mem f ans, Sum_insert_of_not_mem g ans],
|
||||
apply add_le_add H1 H2
|
||||
end
|
||||
|
||||
proposition Sum_nonneg (f : A → B) {s : finset A} (H : ∀x, x ∈ s → f x ≥ 0) :
|
||||
(∑ x ∈ s, f x) ≥ 0 :=
|
||||
calc
|
||||
0 = (∑ x ∈ s, 0) : Sum_zero
|
||||
... ≤ (∑ x ∈ s, f x) : Sum_le_Sum (λ x, 0) f H
|
||||
|
||||
proposition Sum_nonpos (f : A → B) {s : finset A} (H : ∀x, x ∈ s → f x ≤ 0) :
|
||||
(∑ x ∈ s, f x) ≤ 0 :=
|
||||
calc
|
||||
0 = (∑ x ∈ s, 0) : Sum_zero
|
||||
... ≥ (∑ x ∈ s, f x) : Sum_le_Sum f (λ x, 0) H
|
||||
end ordered_comm_group
|
||||
|
||||
section decidable_linear_ordered_comm_group
|
||||
variable [dloocgB : decidable_linear_ordered_comm_group B]
|
||||
include deceqA dloocgB
|
||||
|
||||
proposition abs_Sum_le (f : A → B) (s : finset A) : abs (∑ x ∈ s, f x) ≤ (∑ x ∈ s, abs (f x)) :=
|
||||
begin
|
||||
induction s with a s ans ih,
|
||||
{rewrite [+Sum_empty, abs_zero], apply le.refl},
|
||||
rewrite [Sum_insert_of_not_mem f ans, Sum_insert_of_not_mem _ ans],
|
||||
apply le.trans,
|
||||
apply abs_add_le_abs_add_abs,
|
||||
apply add_le_add_left ih
|
||||
end
|
||||
end decidable_linear_ordered_comm_group
|
||||
|
||||
end finset
|
||||
|
||||
/-
|
||||
-- set versions
|
||||
-/
|
||||
|
||||
namespace set
|
||||
open classical
|
||||
|
||||
section comm_semiring
|
||||
variable [csB : comm_semiring B]
|
||||
include csB
|
||||
|
||||
proposition mul_Sum (f : A → B) {s : set A} (b : B) :
|
||||
b * (∑ x ∈ s, f x) = ∑ x ∈ s, b * f x :=
|
||||
begin
|
||||
cases (em (finite s)) with fins nfins,
|
||||
rotate 1,
|
||||
{rewrite [+Sum_of_not_finite nfins, mul_zero]},
|
||||
induction fins with a s fins ans ih,
|
||||
{rewrite [+Sum_empty, mul_zero]},
|
||||
rewrite [Sum_insert_of_not_mem f ans, Sum_insert_of_not_mem (λ x, b * f x) ans],
|
||||
rewrite [-ih, left_distrib]
|
||||
end
|
||||
|
||||
proposition Sum_mul (f : A → B) {s : set A} (b : B) :
|
||||
(∑ x ∈ s, f x) * b = ∑ x ∈ s, f x * b :=
|
||||
by rewrite [mul.comm _ b, mul_Sum]; apply Sum_ext; intros; apply mul.comm
|
||||
|
||||
proposition Prod_eq_zero (f : A → B) {s : set A} [fins : finite s] {a : A} (H : a ∈ s) (fa0 : f a = 0) :
|
||||
(∏ x ∈ s, f x) = 0 :=
|
||||
begin
|
||||
induction fins with b s fins bns ih,
|
||||
{exact absurd H !not_mem_empty},
|
||||
rewrite [Prod_insert_of_not_mem f bns],
|
||||
have a = b ∨ a ∈ s, from eq_or_mem_of_mem_insert H,
|
||||
cases this with aeqb ains,
|
||||
{rewrite [-aeqb, fa0, zero_mul]},
|
||||
rewrite [ih ains, mul_zero]
|
||||
end
|
||||
end comm_semiring
|
||||
|
||||
section ordered_comm_group
|
||||
variable [ocgB : ordered_comm_group B]
|
||||
include ocgB
|
||||
|
||||
proposition Sum_le_Sum (f g : A → B) {s : set A} (H: ∀₀ x ∈ s, f x ≤ g x) :
|
||||
(∑ x ∈ s, f x) ≤ (∑ x ∈ s, g x) :=
|
||||
begin
|
||||
cases (em (finite s)) with fins nfins,
|
||||
{induction fins with a s fins ans ih,
|
||||
{rewrite +Sum_empty; apply le.refl},
|
||||
{rewrite [Sum_insert_of_not_mem f ans, Sum_insert_of_not_mem g ans],
|
||||
have H1 : f a ≤ g a, from H !mem_insert,
|
||||
have H2 : (∑ x ∈ s, f x) ≤ (∑ x ∈ s, g x), from ih (forall_of_forall_insert H),
|
||||
apply add_le_add H1 H2}},
|
||||
rewrite [+Sum_of_not_finite nfins],
|
||||
apply le.refl
|
||||
end
|
||||
|
||||
proposition Sum_nonneg (f : A → B) {s : set A} (H : ∀₀ x ∈ s, f x ≥ 0) :
|
||||
(∑ x ∈ s, f x) ≥ 0 :=
|
||||
calc
|
||||
0 = (∑ x ∈ s, 0) : Sum_zero
|
||||
... ≤ (∑ x ∈ s, f x) : Sum_le_Sum (λ x, 0) f H
|
||||
|
||||
proposition Sum_nonpos (f : A → B) {s : set A} (H : ∀₀ x ∈ s, f x ≤ 0) :
|
||||
(∑ x ∈ s, f x) ≤ 0 :=
|
||||
calc
|
||||
0 = (∑ x ∈ s, 0) : Sum_zero
|
||||
... ≥ (∑ x ∈ s, f x) : Sum_le_Sum f (λ x, 0) H
|
||||
end ordered_comm_group
|
||||
|
||||
section decidable_linear_ordered_comm_group
|
||||
variable [dloocgB : decidable_linear_ordered_comm_group B]
|
||||
include deceqA dloocgB
|
||||
|
||||
proposition abs_Sum_le (f : A → B) (s : set A) : abs (∑ x ∈ s, f x) ≤ (∑ x ∈ s, abs (f x)) :=
|
||||
begin
|
||||
cases (em (finite s)) with fins nfins,
|
||||
rotate 1,
|
||||
{rewrite [+Sum_of_not_finite nfins, abs_zero], apply le.refl},
|
||||
induction fins with a s fins ans ih,
|
||||
{rewrite [+Sum_empty, abs_zero], apply le.refl},
|
||||
rewrite [Sum_insert_of_not_mem f ans, Sum_insert_of_not_mem _ ans],
|
||||
apply le.trans,
|
||||
apply abs_add_le_abs_add_abs,
|
||||
apply add_le_add_left ih
|
||||
end
|
||||
end decidable_linear_ordered_comm_group
|
||||
|
||||
end set
|
||||
|
|
@ -3,9 +3,7 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Jeremy Avigad
|
||||
|
||||
Properties of the power operation in an ordered ring or field.
|
||||
|
||||
(Right now, this file is just a stub. More soon.)
|
||||
Properties of the power operation in various structures, including ordered rings and fields.
|
||||
-/
|
||||
import .group_power .ordered_field
|
||||
open nat
|
||||
|
|
|
|||
|
|
@ -274,6 +274,12 @@ ext (λ x, eq.substr (mem_insert_eq x a s)
|
|||
theorem insert.comm (x y : X) (s : set X) : insert x (insert y s) = insert y (insert x s) :=
|
||||
ext (take a, by rewrite [*mem_insert_eq, propext !or.left_comm])
|
||||
|
||||
-- useful in proofs by induction
|
||||
theorem forall_of_forall_insert {P : X → Prop} {a : X} {s : set X}
|
||||
(H : ∀ x, x ∈ insert a s → P x) :
|
||||
∀ x, x ∈ s → P x :=
|
||||
λ x xs, H x (!mem_insert_of_mem xs)
|
||||
|
||||
/- singleton -/
|
||||
|
||||
theorem mem_singleton_iff (a b : X) : a ∈ '{b} ↔ a = b :=
|
||||
|
|
@ -402,9 +408,9 @@ section
|
|||
suppose x ∈ Union b,
|
||||
obtain i (Hi : x ∈ b i), from this,
|
||||
show x ∈ c, from H i Hi
|
||||
|
||||
theorem sUnion_insert (s : set (set X)) (a : set X) :
|
||||
sUnion (insert a s) = a ∪ sUnion s :=
|
||||
|
||||
theorem sUnion_insert (s : set (set X)) (a : set X) :
|
||||
sUnion (insert a s) = a ∪ sUnion s :=
|
||||
ext (take x, iff.intro
|
||||
(suppose x ∈ sUnion (insert a s),
|
||||
obtain c [(cias : c ∈ insert a s) (xc : x ∈ c)], from this,
|
||||
|
|
@ -422,11 +428,11 @@ ext (take x, iff.intro
|
|||
obtain c [(cs : c ∈ s) (xc : x ∈ c)], from this,
|
||||
have c ∈ insert a s, from or.inr cs,
|
||||
show x ∈ sUnion (insert a s), from exists.intro c (and.intro this `x ∈ c`))))
|
||||
|
||||
|
||||
lemma sInter_insert (s : set (set X)) (a : set X) :
|
||||
sInter (insert a s) = a ∩ sInter s :=
|
||||
sInter (insert a s) = a ∩ sInter s :=
|
||||
ext (take x, iff.intro
|
||||
(suppose x ∈ sInter (insert a s),
|
||||
(suppose x ∈ sInter (insert a s),
|
||||
have ∀c, c ∈ insert a s → x ∈ c, from this,
|
||||
have x ∈ a, from (this a) !mem_insert,
|
||||
show x ∈ a ∩ sInter s, from and.intro
|
||||
|
|
@ -435,18 +441,18 @@ ext (take x, iff.intro
|
|||
suppose c ∈ s,
|
||||
(`∀c, c ∈ insert a s → x ∈ c` c) (!mem_insert_of_mem this))
|
||||
(suppose x ∈ a ∩ sInter s,
|
||||
show ∀c, c ∈ insert a s → x ∈ c, from
|
||||
show ∀c, c ∈ insert a s → x ∈ c, from
|
||||
take c,
|
||||
suppose c ∈ insert a s,
|
||||
have c = a → x ∈ c, from
|
||||
have c = a → x ∈ c, from
|
||||
suppose c = a,
|
||||
show x ∈ c, from this⁻¹ ▸ and.elim_left `x ∈ a ∩ sInter s`,
|
||||
have c ∈ s → x ∈ c, from
|
||||
have c ∈ s → x ∈ c, from
|
||||
suppose c ∈ s,
|
||||
have ∀c, c ∈ s → x ∈ c, from and.elim_right `x ∈ a ∩ sInter s`,
|
||||
have ∀c, c ∈ s → x ∈ c, from and.elim_right `x ∈ a ∩ sInter s`,
|
||||
show x ∈ c, from (this c) `c ∈ s`,
|
||||
show x ∈ c, from !or.elim `c ∈ insert a s` `c = a → x ∈ c` this))
|
||||
|
||||
|
||||
end
|
||||
|
||||
end set
|
||||
|
|
|
|||
Loading…
Reference in a new issue