lean2/library/data/nat/bigops.lean

100 lines
4.6 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
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 natural numbers.
-/
import data.nat.basic data.nat.order algebra.group_bigops
open list finset
namespace nat
open [classes] algebra
local attribute nat.comm_semiring [instance]
variables {A : Type} [deceqA : decidable_eq A]
/- Prodl -/
definition Prodl (l : list A) (f : A → nat) : nat := algebra.Prodl l f
notation `∏` binders `←` l, r:(scoped f, Prodl l f) := r
theorem Prodl_nil (f : A → nat) : Prodl [] f = 1 := algebra.Prodl_nil f
theorem Prodl_cons (f : A → nat) (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 → nat) : 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 → nat) :
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 → nat) {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 → nat) {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 → nat) (d : disjoint l₁ l₂) :
Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d
end deceqA
/- Prod -/
definition Prod (s : finset A) (f : A → nat) : nat := algebra.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → nat) : Prod ∅ f = 1 := algebra.Prod_empty f
theorem Prod_mul (s : finset A) (f g : A → nat) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
algebra.Prod_mul s f g
section deceqA
include deceqA
theorem Prod_insert_of_mem (f : A → nat) {a : A} {s : finset A} (H : a ∈ s) :
Prod (insert a s) f = Prod s f := algebra.Prod_insert_of_mem f H
theorem Prod_insert_of_not_mem (f : A → nat) {a : A} {s : finset A} (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f := algebra.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → nat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Prod (s₁ s₂) f = Prod s₁ f * Prod s₂ f := algebra.Prod_union f disj
theorem Prod_ext {s : finset A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) :
Prod s f = Prod s g := algebra.Prod_ext H
end deceqA
/- Suml -/
definition Suml (l : list A) (f : A → nat) : nat := algebra.Suml l f
notation `∑` binders `←` l, r:(scoped f, Suml l f) := r
theorem Suml_nil (f : A → nat) : Suml [] f = 0 := algebra.Suml_nil f
theorem Suml_cons (f : A → nat) (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 → nat) : 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 → nat) : 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 → nat) {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 → nat) {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 → nat) (d : disjoint l₁ l₂) :
Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d
end deceqA
/- Sum -/
definition Sum (s : finset A) (f : A → nat) : nat := algebra.Sum s f
notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → nat) : Sum ∅ f = 0 := algebra.Sum_empty f
theorem Sum_add (s : finset A) (f g : A → nat) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
algebra.Sum_add s f g
section deceqA
include deceqA
theorem Sum_insert_of_mem (f : A → nat) {a : A} {s : finset A} (H : a ∈ s) :
Sum (insert a s) f = Sum s f := algebra.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → nat) {a : A} {s : finset A} (H : a ∉ s) :
Sum (insert a s) f = f a + Sum s f := algebra.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → nat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Sum (s₁ s₂) f = Sum s₁ f + Sum s₂ f := algebra.Sum_union f disj
theorem Sum_ext {s : finset A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := algebra.Sum_ext H
end deceqA
end nat