diff --git a/library/data/int/bigops.lean b/library/data/int/bigops.lean new file mode 100644 index 000000000..8f830733a --- /dev/null +++ b/library/data/int/bigops.lean @@ -0,0 +1,165 @@ +/- +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jeremy Avigad + +Finite products and sums on the integers. +-/ +import data.int.order algebra.group_bigops algebra.group_set_bigops +open list + +namespace int +open [classes] algebra +local attribute int.decidable_linear_ordered_comm_ring [instance] +variables {A : Type} [deceqA : decidable_eq A] + +/- Prodl -/ + +definition Prodl (l : list A) (f : A → int) : int := algebra.Prodl l f +notation `∏` binders `←` l, r:(scoped f, Prodl l f) := r + +theorem Prodl_nil (f : A → int) : Prodl [] f = 1 := algebra.Prodl_nil f +theorem Prodl_cons (f : A → int) (a : A) (l : list A) : Prodl (a::l) f = f a * Prodl l f := + algebra.Prodl_cons f a l +theorem Prodl_append (l₁ l₂ : list A) (f : A → int) : Prodl (l₁++l₂) f = Prodl l₁ f * Prodl l₂ f := + algebra.Prodl_append l₁ l₂ f +theorem Prodl_mul (l : list A) (f g : A → int) : + Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := algebra.Prodl_mul l f g +section deceqA + include deceqA + theorem Prodl_insert_of_mem (f : A → int) {a : A} {l : list A} (H : a ∈ l) : + Prodl (insert a l) f = Prodl l f := algebra.Prodl_insert_of_mem f H + theorem Prodl_insert_of_not_mem (f : A → int) {a : A} {l : list A} (H : a ∉ l) : + Prodl (insert a l) f = f a * Prodl l f := algebra.Prodl_insert_of_not_mem f H + theorem Prodl_union {l₁ l₂ : list A} (f : A → int) (d : disjoint l₁ l₂) : + Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d + theorem Prodl_one (l : list A) : Prodl l (λ x, 1) = 1 := algebra.Prodl_one l +end deceqA + +/- Prod over finset -/ + +namespace finset +open finset + +definition Prod (s : finset A) (f : A → int) : int := algebra.finset.Prod s f +notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r + +theorem Prod_empty (f : A → int) : Prod ∅ f = 1 := algebra.finset.Prod_empty f +theorem Prod_mul (s : finset A) (f g : A → int) : Prod s (λx, f x * g x) = Prod s f * Prod s g := + algebra.finset.Prod_mul s f g +section deceqA + include deceqA + theorem Prod_insert_of_mem (f : A → int) {a : A} {s : finset A} (H : a ∈ s) : + Prod (insert a s) f = Prod s f := algebra.finset.Prod_insert_of_mem f H + theorem Prod_insert_of_not_mem (f : A → int) {a : A} {s : finset A} (H : a ∉ s) : + Prod (insert a s) f = f a * Prod s f := algebra.finset.Prod_insert_of_not_mem f H + theorem Prod_union (f : A → int) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.finset.Prod_union f disj + theorem Prod_ext {s : finset A} {f g : A → int} (H : ∀x, x ∈ s → f x = g x) : + Prod s f = Prod s g := algebra.finset.Prod_ext H + theorem Prod_one (s : finset A) : Prod s (λ x, 1) = 1 := algebra.finset.Prod_one s +end deceqA + +end finset + +/- Prod over set -/ + +namespace set +open set + +noncomputable definition Prod (s : set A) (f : A → int) : int := algebra.set.Prod s f +notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r + +theorem Prod_empty (f : A → int) : Prod ∅ f = 1 := algebra.set.Prod_empty f +theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → int) : Prod s f = 1 := + algebra.set.Prod_of_not_finite nfins f +theorem Prod_mul (s : set A) (f g : A → int) : Prod s (λx, f x * g x) = Prod s f * Prod s g := + algebra.set.Prod_mul s f g +theorem Prod_insert_of_mem (f : A → int) {a : A} {s : set A} (H : a ∈ s) : + Prod (insert a s) f = Prod s f := algebra.set.Prod_insert_of_mem f H +theorem Prod_insert_of_not_mem (f : A → int) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + Prod (insert a s) f = f a * Prod s f := algebra.set.Prod_insert_of_not_mem f H +theorem Prod_union (f : A → int) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.set.Prod_union f disj +theorem Prod_ext {s : set A} {f g : A → int} (H : ∀x, x ∈ s → f x = g x) : + Prod s f = Prod s g := algebra.set.Prod_ext H +theorem Prod_one (s : set A) : Prod s (λ x, 1) = 1 := algebra.set.Prod_one s + +end set + +/- Suml -/ + +definition Suml (l : list A) (f : A → int) : int := algebra.Suml l f +notation `∑` binders `←` l, r:(scoped f, Suml l f) := r + +theorem Suml_nil (f : A → int) : Suml [] f = 0 := algebra.Suml_nil f +theorem Suml_cons (f : A → int) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f := + algebra.Suml_cons f a l +theorem Suml_append (l₁ l₂ : list A) (f : A → int) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f := + algebra.Suml_append l₁ l₂ f +theorem Suml_add (l : list A) (f g : A → int) : Suml l (λx, f x + g x) = Suml l f + Suml l g := + algebra.Suml_add l f g +section deceqA + include deceqA + theorem Suml_insert_of_mem (f : A → int) {a : A} {l : list A} (H : a ∈ l) : + Suml (insert a l) f = Suml l f := algebra.Suml_insert_of_mem f H + theorem Suml_insert_of_not_mem (f : A → int) {a : A} {l : list A} (H : a ∉ l) : + Suml (insert a l) f = f a + Suml l f := algebra.Suml_insert_of_not_mem f H + theorem Suml_union {l₁ l₂ : list A} (f : A → int) (d : disjoint l₁ l₂) : + Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d + theorem Suml_zero (l : list A) : Suml l (λ x, 0) = 0 := algebra.Suml_zero l +end deceqA + +/- Sum over a finset -/ + +namespace finset +open finset +definition Sum (s : finset A) (f : A → int) : int := algebra.finset.Sum s f +notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r + +theorem Sum_empty (f : A → int) : Sum ∅ f = 0 := algebra.finset.Sum_empty f +theorem Sum_add (s : finset A) (f g : A → int) : Sum s (λx, f x + g x) = Sum s f + Sum s g := + algebra.finset.Sum_add s f g +section deceqA + include deceqA + theorem Sum_insert_of_mem (f : A → int) {a : A} {s : finset A} (H : a ∈ s) : + Sum (insert a s) f = Sum s f := algebra.finset.Sum_insert_of_mem f H + theorem Sum_insert_of_not_mem (f : A → int) {a : A} {s : finset A} (H : a ∉ s) : + Sum (insert a s) f = f a + Sum s f := algebra.finset.Sum_insert_of_not_mem f H + theorem Sum_union (f : A → int) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.finset.Sum_union f disj + theorem Sum_ext {s : finset A} {f g : A → int} (H : ∀x, x ∈ s → f x = g x) : + Sum s f = Sum s g := algebra.finset.Sum_ext H + theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = 0 := algebra.finset.Sum_zero s +end deceqA + +end finset + +/- Sum over a set -/ + +namespace set +open set + +noncomputable definition Sum (s : set A) (f : A → int) : int := algebra.set.Sum s f +notation `∏` binders `∈` s, r:(scoped f, Sum s f) := r + +theorem Sum_empty (f : A → int) : Sum ∅ f = 0 := algebra.set.Sum_empty f +theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → int) : Sum s f = 0 := + algebra.set.Sum_of_not_finite nfins f +theorem Sum_add (s : set A) (f g : A → int) : Sum s (λx, f x + g x) = Sum s f + Sum s g := + algebra.set.Sum_add s f g +theorem Sum_insert_of_mem (f : A → int) {a : A} {s : set A} (H : a ∈ s) : + Sum (insert a s) f = Sum s f := algebra.set.Sum_insert_of_mem f H +theorem Sum_insert_of_not_mem (f : A → int) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + Sum (insert a s) f = f a + Sum s f := algebra.set.Sum_insert_of_not_mem f H +theorem Sum_union (f : A → int) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.set.Sum_union f disj +theorem Sum_ext {s : set A} {f g : A → int} (H : ∀x, x ∈ s → f x = g x) : + Sum s f = Sum s g := algebra.set.Sum_ext H +theorem Sum_zero (s : set A) : Sum s (λ x, 0) = 0 := algebra.set.Sum_zero s + +end set + +end int diff --git a/library/data/int/default.lean b/library/data/int/default.lean index c71c4f767..5e3478af4 100644 --- a/library/data/int/default.lean +++ b/library/data/int/default.lean @@ -3,4 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad -/ -import .basic .order .div .power .gcd +import .basic .order .div .power .gcd .bigops diff --git a/library/data/int/int.md b/library/data/int/int.md index 701972b58..83b470039 100644 --- a/library/data/int/int.md +++ b/library/data/int/int.md @@ -8,3 +8,4 @@ The integers. * [div](div.lean) : div and mod * [power](power.lean) * [gcd](gcd.lean) : gcd, lcm, and coprime +* [bigops](bigops.lean) \ No newline at end of file diff --git a/library/data/rat/bigops.lean b/library/data/rat/bigops.lean new file mode 100644 index 000000000..0ff99b7b5 --- /dev/null +++ b/library/data/rat/bigops.lean @@ -0,0 +1,165 @@ +/- +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jeremy Avigad + +Finite products and sums on the rationals. +-/ +import data.rat.order algebra.group_bigops algebra.group_set_bigops +open list + +namespace rat +open [classes] algebra +local attribute rat.discrete_linear_ordered_field [instance] +variables {A : Type} [deceqA : decidable_eq A] + +/- Prodl -/ + +definition Prodl (l : list A) (f : A → rat) : rat := algebra.Prodl l f +notation `∏` binders `←` l, r:(scoped f, Prodl l f) := r + +theorem Prodl_nil (f : A → rat) : Prodl [] f = 1 := algebra.Prodl_nil f +theorem Prodl_cons (f : A → rat) (a : A) (l : list A) : Prodl (a::l) f = f a * Prodl l f := + algebra.Prodl_cons f a l +theorem Prodl_append (l₁ l₂ : list A) (f : A → rat) : Prodl (l₁++l₂) f = Prodl l₁ f * Prodl l₂ f := + algebra.Prodl_append l₁ l₂ f +theorem Prodl_mul (l : list A) (f g : A → rat) : + Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := algebra.Prodl_mul l f g +section deceqA + include deceqA + theorem Prodl_insert_of_mem (f : A → rat) {a : A} {l : list A} (H : a ∈ l) : + Prodl (insert a l) f = Prodl l f := algebra.Prodl_insert_of_mem f H + theorem Prodl_insert_of_not_mem (f : A → rat) {a : A} {l : list A} (H : a ∉ l) : + Prodl (insert a l) f = f a * Prodl l f := algebra.Prodl_insert_of_not_mem f H + theorem Prodl_union {l₁ l₂ : list A} (f : A → rat) (d : disjoint l₁ l₂) : + Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d + theorem Prodl_one (l : list A) : Prodl l (λ x, 1) = 1 := algebra.Prodl_one l +end deceqA + +/- Prod over finset -/ + +namespace finset +open finset + +definition Prod (s : finset A) (f : A → rat) : rat := algebra.finset.Prod s f +notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r + +theorem Prod_empty (f : A → rat) : Prod ∅ f = 1 := algebra.finset.Prod_empty f +theorem Prod_mul (s : finset A) (f g : A → rat) : Prod s (λx, f x * g x) = Prod s f * Prod s g := + algebra.finset.Prod_mul s f g +section deceqA + include deceqA + theorem Prod_insert_of_mem (f : A → rat) {a : A} {s : finset A} (H : a ∈ s) : + Prod (insert a s) f = Prod s f := algebra.finset.Prod_insert_of_mem f H + theorem Prod_insert_of_not_mem (f : A → rat) {a : A} {s : finset A} (H : a ∉ s) : + Prod (insert a s) f = f a * Prod s f := algebra.finset.Prod_insert_of_not_mem f H + theorem Prod_union (f : A → rat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.finset.Prod_union f disj + theorem Prod_ext {s : finset A} {f g : A → rat} (H : ∀x, x ∈ s → f x = g x) : + Prod s f = Prod s g := algebra.finset.Prod_ext H + theorem Prod_one (s : finset A) : Prod s (λ x, 1) = 1 := algebra.finset.Prod_one s +end deceqA + +end finset + +/- Prod over set -/ + +namespace set +open set + +noncomputable definition Prod (s : set A) (f : A → rat) : rat := algebra.set.Prod s f +notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r + +theorem Prod_empty (f : A → rat) : Prod ∅ f = 1 := algebra.set.Prod_empty f +theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → rat) : Prod s f = 1 := + algebra.set.Prod_of_not_finite nfins f +theorem Prod_mul (s : set A) (f g : A → rat) : Prod s (λx, f x * g x) = Prod s f * Prod s g := + algebra.set.Prod_mul s f g +theorem Prod_insert_of_mem (f : A → rat) {a : A} {s : set A} (H : a ∈ s) : + Prod (insert a s) f = Prod s f := algebra.set.Prod_insert_of_mem f H +theorem Prod_insert_of_not_mem (f : A → rat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + Prod (insert a s) f = f a * Prod s f := algebra.set.Prod_insert_of_not_mem f H +theorem Prod_union (f : A → rat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.set.Prod_union f disj +theorem Prod_ext {s : set A} {f g : A → rat} (H : ∀x, x ∈ s → f x = g x) : + Prod s f = Prod s g := algebra.set.Prod_ext H +theorem Prod_one (s : set A) : Prod s (λ x, 1) = 1 := algebra.set.Prod_one s + +end set + +/- Suml -/ + +definition Suml (l : list A) (f : A → rat) : rat := algebra.Suml l f +notation `∑` binders `←` l, r:(scoped f, Suml l f) := r + +theorem Suml_nil (f : A → rat) : Suml [] f = 0 := algebra.Suml_nil f +theorem Suml_cons (f : A → rat) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f := + algebra.Suml_cons f a l +theorem Suml_append (l₁ l₂ : list A) (f : A → rat) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f := + algebra.Suml_append l₁ l₂ f +theorem Suml_add (l : list A) (f g : A → rat) : Suml l (λx, f x + g x) = Suml l f + Suml l g := + algebra.Suml_add l f g +section deceqA + include deceqA + theorem Suml_insert_of_mem (f : A → rat) {a : A} {l : list A} (H : a ∈ l) : + Suml (insert a l) f = Suml l f := algebra.Suml_insert_of_mem f H + theorem Suml_insert_of_not_mem (f : A → rat) {a : A} {l : list A} (H : a ∉ l) : + Suml (insert a l) f = f a + Suml l f := algebra.Suml_insert_of_not_mem f H + theorem Suml_union {l₁ l₂ : list A} (f : A → rat) (d : disjoint l₁ l₂) : + Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d + theorem Suml_zero (l : list A) : Suml l (λ x, 0) = 0 := algebra.Suml_zero l +end deceqA + +/- Sum over a finset -/ + +namespace finset +open finset +definition Sum (s : finset A) (f : A → rat) : rat := algebra.finset.Sum s f +notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r + +theorem Sum_empty (f : A → rat) : Sum ∅ f = 0 := algebra.finset.Sum_empty f +theorem Sum_add (s : finset A) (f g : A → rat) : Sum s (λx, f x + g x) = Sum s f + Sum s g := + algebra.finset.Sum_add s f g +section deceqA + include deceqA + theorem Sum_insert_of_mem (f : A → rat) {a : A} {s : finset A} (H : a ∈ s) : + Sum (insert a s) f = Sum s f := algebra.finset.Sum_insert_of_mem f H + theorem Sum_insert_of_not_mem (f : A → rat) {a : A} {s : finset A} (H : a ∉ s) : + Sum (insert a s) f = f a + Sum s f := algebra.finset.Sum_insert_of_not_mem f H + theorem Sum_union (f : A → rat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.finset.Sum_union f disj + theorem Sum_ext {s : finset A} {f g : A → rat} (H : ∀x, x ∈ s → f x = g x) : + Sum s f = Sum s g := algebra.finset.Sum_ext H + theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = 0 := algebra.finset.Sum_zero s +end deceqA + +end finset + +/- Sum over a set -/ + +namespace set +open set + +noncomputable definition Sum (s : set A) (f : A → rat) : rat := algebra.set.Sum s f +notation `∏` binders `∈` s, r:(scoped f, Sum s f) := r + +theorem Sum_empty (f : A → rat) : Sum ∅ f = 0 := algebra.set.Sum_empty f +theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → rat) : Sum s f = 0 := + algebra.set.Sum_of_not_finite nfins f +theorem Sum_add (s : set A) (f g : A → rat) : Sum s (λx, f x + g x) = Sum s f + Sum s g := + algebra.set.Sum_add s f g +theorem Sum_insert_of_mem (f : A → rat) {a : A} {s : set A} (H : a ∈ s) : + Sum (insert a s) f = Sum s f := algebra.set.Sum_insert_of_mem f H +theorem Sum_insert_of_not_mem (f : A → rat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + Sum (insert a s) f = f a + Sum s f := algebra.set.Sum_insert_of_not_mem f H +theorem Sum_union (f : A → rat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.set.Sum_union f disj +theorem Sum_ext {s : set A} {f g : A → rat} (H : ∀x, x ∈ s → f x = g x) : + Sum s f = Sum s g := algebra.set.Sum_ext H +theorem Sum_zero (s : set A) : Sum s (λ x, 0) = 0 := algebra.set.Sum_zero s + +end set + +end rat diff --git a/library/data/rat/default.lean b/library/data/rat/default.lean index a9cb20ed7..a9b26fa4b 100644 --- a/library/data/rat/default.lean +++ b/library/data/rat/default.lean @@ -3,4 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad -/ -import .basic .order +import .basic .order .bigops diff --git a/library/data/rat/rat.md b/library/data/rat/rat.md index 18157f983..d3f80867d 100644 --- a/library/data/rat/rat.md +++ b/library/data/rat/rat.md @@ -5,3 +5,4 @@ The rational numbers. * [basic](basic.lean) : the rationals as a field * [order](order.lean) : the order relations and the sign function +* [bigops](bigops.lean) \ No newline at end of file diff --git a/library/data/real/bigops.lean b/library/data/real/bigops.lean new file mode 100644 index 000000000..10d6d3b66 --- /dev/null +++ b/library/data/real/bigops.lean @@ -0,0 +1,167 @@ +/- +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jeremy Avigad + +Finite products and sums on the reals. +-/ +import data.real.division algebra.group_bigops algebra.group_set_bigops +open list + +namespace real +open [classes] algebra +local attribute real.ordered_ring [instance] +local attribute real.comm_ring [instance] + +variables {A : Type} [deceqA : decidable_eq A] + +/- Prodl -/ + +definition Prodl (l : list A) (f : A → real) : real := algebra.Prodl l f +notation `∏` binders `←` l, r:(scoped f, Prodl l f) := r + +theorem Prodl_nil (f : A → real) : Prodl [] f = 1 := algebra.Prodl_nil f +theorem Prodl_cons (f : A → real) (a : A) (l : list A) : Prodl (a::l) f = f a * Prodl l f := + algebra.Prodl_cons f a l +theorem Prodl_append (l₁ l₂ : list A) (f : A → real) : Prodl (l₁++l₂) f = Prodl l₁ f * Prodl l₂ f := + algebra.Prodl_append l₁ l₂ f +theorem Prodl_mul (l : list A) (f g : A → real) : + Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := algebra.Prodl_mul l f g +section deceqA + include deceqA + theorem Prodl_insert_of_mem (f : A → real) {a : A} {l : list A} (H : a ∈ l) : + Prodl (insert a l) f = Prodl l f := algebra.Prodl_insert_of_mem f H + theorem Prodl_insert_of_not_mem (f : A → real) {a : A} {l : list A} (H : a ∉ l) : + Prodl (insert a l) f = f a * Prodl l f := algebra.Prodl_insert_of_not_mem f H + theorem Prodl_union {l₁ l₂ : list A} (f : A → real) (d : disjoint l₁ l₂) : + Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d + theorem Prodl_one (l : list A) : Prodl l (λ x, 1) = 1 := algebra.Prodl_one l +end deceqA + +/- Prod over finset -/ + +namespace finset +open finset + +definition Prod (s : finset A) (f : A → real) : real := algebra.finset.Prod s f +notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r + +theorem Prod_empty (f : A → real) : Prod ∅ f = 1 := algebra.finset.Prod_empty f +theorem Prod_mul (s : finset A) (f g : A → real) : Prod s (λx, f x * g x) = Prod s f * Prod s g := + algebra.finset.Prod_mul s f g +section deceqA + include deceqA + theorem Prod_insert_of_mem (f : A → real) {a : A} {s : finset A} (H : a ∈ s) : + Prod (insert a s) f = Prod s f := algebra.finset.Prod_insert_of_mem f H + theorem Prod_insert_of_not_mem (f : A → real) {a : A} {s : finset A} (H : a ∉ s) : + Prod (insert a s) f = f a * Prod s f := algebra.finset.Prod_insert_of_not_mem f H + theorem Prod_union (f : A → real) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.finset.Prod_union f disj + theorem Prod_ext {s : finset A} {f g : A → real} (H : ∀x, x ∈ s → f x = g x) : + Prod s f = Prod s g := algebra.finset.Prod_ext H + theorem Prod_one (s : finset A) : Prod s (λ x, 1) = 1 := algebra.finset.Prod_one s +end deceqA + +end finset + +/- Prod over set -/ + +namespace set +open set + +noncomputable definition Prod (s : set A) (f : A → real) : real := algebra.set.Prod s f +notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r + +theorem Prod_empty (f : A → real) : Prod ∅ f = 1 := algebra.set.Prod_empty f +theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → real) : Prod s f = 1 := + algebra.set.Prod_of_not_finite nfins f +theorem Prod_mul (s : set A) (f g : A → real) : Prod s (λx, f x * g x) = Prod s f * Prod s g := + algebra.set.Prod_mul s f g +theorem Prod_insert_of_mem (f : A → real) {a : A} {s : set A} (H : a ∈ s) : + Prod (insert a s) f = Prod s f := algebra.set.Prod_insert_of_mem f H +theorem Prod_insert_of_not_mem (f : A → real) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + Prod (insert a s) f = f a * Prod s f := algebra.set.Prod_insert_of_not_mem f H +theorem Prod_union (f : A → real) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.set.Prod_union f disj +theorem Prod_ext {s : set A} {f g : A → real} (H : ∀x, x ∈ s → f x = g x) : + Prod s f = Prod s g := algebra.set.Prod_ext H +theorem Prod_one (s : set A) : Prod s (λ x, 1) = 1 := algebra.set.Prod_one s + +end set + +/- Suml -/ + +definition Suml (l : list A) (f : A → real) : real := algebra.Suml l f +notation `∑` binders `←` l, r:(scoped f, Suml l f) := r + +theorem Suml_nil (f : A → real) : Suml [] f = 0 := algebra.Suml_nil f +theorem Suml_cons (f : A → real) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f := + algebra.Suml_cons f a l +theorem Suml_append (l₁ l₂ : list A) (f : A → real) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f := + algebra.Suml_append l₁ l₂ f +theorem Suml_add (l : list A) (f g : A → real) : Suml l (λx, f x + g x) = Suml l f + Suml l g := + algebra.Suml_add l f g +section deceqA + include deceqA + theorem Suml_insert_of_mem (f : A → real) {a : A} {l : list A} (H : a ∈ l) : + Suml (insert a l) f = Suml l f := algebra.Suml_insert_of_mem f H + theorem Suml_insert_of_not_mem (f : A → real) {a : A} {l : list A} (H : a ∉ l) : + Suml (insert a l) f = f a + Suml l f := algebra.Suml_insert_of_not_mem f H + theorem Suml_union {l₁ l₂ : list A} (f : A → real) (d : disjoint l₁ l₂) : + Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d + theorem Suml_zero (l : list A) : Suml l (λ x, 0) = 0 := algebra.Suml_zero l +end deceqA + +/- Sum over a finset -/ + +namespace finset +open finset +definition Sum (s : finset A) (f : A → real) : real := algebra.finset.Sum s f +notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r + +theorem Sum_empty (f : A → real) : Sum ∅ f = 0 := algebra.finset.Sum_empty f +theorem Sum_add (s : finset A) (f g : A → real) : Sum s (λx, f x + g x) = Sum s f + Sum s g := + algebra.finset.Sum_add s f g +section deceqA + include deceqA + theorem Sum_insert_of_mem (f : A → real) {a : A} {s : finset A} (H : a ∈ s) : + Sum (insert a s) f = Sum s f := algebra.finset.Sum_insert_of_mem f H + theorem Sum_insert_of_not_mem (f : A → real) {a : A} {s : finset A} (H : a ∉ s) : + Sum (insert a s) f = f a + Sum s f := algebra.finset.Sum_insert_of_not_mem f H + theorem Sum_union (f : A → real) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.finset.Sum_union f disj + theorem Sum_ext {s : finset A} {f g : A → real} (H : ∀x, x ∈ s → f x = g x) : + Sum s f = Sum s g := algebra.finset.Sum_ext H + theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = 0 := algebra.finset.Sum_zero s +end deceqA + +end finset + +/- Sum over a set -/ + +namespace set +open set + +noncomputable definition Sum (s : set A) (f : A → real) : real := algebra.set.Sum s f +notation `∏` binders `∈` s, r:(scoped f, Sum s f) := r + +theorem Sum_empty (f : A → real) : Sum ∅ f = 0 := algebra.set.Sum_empty f +theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → real) : Sum s f = 0 := + algebra.set.Sum_of_not_finite nfins f +theorem Sum_add (s : set A) (f g : A → real) : Sum s (λx, f x + g x) = Sum s f + Sum s g := + algebra.set.Sum_add s f g +theorem Sum_insert_of_mem (f : A → real) {a : A} {s : set A} (H : a ∈ s) : + Sum (insert a s) f = Sum s f := algebra.set.Sum_insert_of_mem f H +theorem Sum_insert_of_not_mem (f : A → real) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + Sum (insert a s) f = f a + Sum s f := algebra.set.Sum_insert_of_not_mem f H +theorem Sum_union (f : A → real) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.set.Sum_union f disj +theorem Sum_ext {s : set A} {f g : A → real} (H : ∀x, x ∈ s → f x = g x) : + Sum s f = Sum s g := algebra.set.Sum_ext H +theorem Sum_zero (s : set A) : Sum s (λ x, 0) = 0 := algebra.set.Sum_zero s + +end set + +end real diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 062d3c553..e4b28d96d 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -1011,7 +1011,6 @@ theorem under_lowest_bound : ∀ y : ℝ, ub y → sup_under ≤ y := theorem under_over_equiv : p_under_seq ≡ p_over_seq := begin - rewrite ↑equiv, intros, apply rat.le.trans, have H : p_under_seq n < p_over_seq n, from !under_seq_lt_over_seq, diff --git a/library/data/real/default.lean b/library/data/real/default.lean index 21e4a435f..4567ee42f 100644 --- a/library/data/real/default.lean +++ b/library/data/real/default.lean @@ -3,4 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Robert Y. Lewis -/ -import .basic .order .division .complete +import .basic .order .division .complete .bigops diff --git a/library/data/real/real.md b/library/data/real/real.md index 5e05818fd..3a19476a7 100644 --- a/library/data/real/real.md +++ b/library/data/real/real.md @@ -6,4 +6,5 @@ The real numbers: classically, as a quotient type; constructively, as a setoid. * [basic](basic.lean) : the reals as a commutative ring (constructive) * [order](order.lean) : the reals as an ordered ring (constructive) * [division](division.lean) : the reals as a discrete linear ordered field (classical) -* [complete](complete.lean) : the reals are Cauchy complete (classical) \ No newline at end of file +* [complete](complete.lean) : the reals are Cauchy complete (classical) +* [bigops](bigops.lean) \ No newline at end of file