Library big_minmax
Here we define the maximum and the minimum for many elements and we prove
some basic results about them.
\maxr_(i <- s) F i == \big[Num.max/0]_(i <- s) F i. The maximum
of all F i only if each F i is non-negative.
(since the neutral element is 0).
(see the file bigop.v of SSReflect library for
this notation)
min_seq s == it is the minimum of elements of the sequence s.
This is 0 if s is empty.
min_fT F == if F : fT -> rT where fT is a finType then this
returns the minimum of all F i forall i of Type fT
and 0 if fT is not inhabited.
Import GRing.Theory.
Import Num.Theory.
Import Num.Def.
Set Implicit Arguments.
Import Prenex Implicits.
Reserved Notation "\maxr_ i F"
(at level 41, F at level 41, i at level 0,
format "'[' \maxr_ i '/ ' F ']'").
Reserved Notation "\maxr_ ( i <- r | P ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \maxr_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\maxr_ ( i <- r ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \maxr_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\maxr_ ( m <= i < n | P ) F"
(at level 41, F at level 41, i, m, n at level 50,
format "'[' \maxr_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\maxr_ ( m <= i < n ) F"
(at level 41, F at level 41, i, m, n at level 50,
format "'[' \maxr_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\maxr_ ( i | P ) F"
(at level 41, F at level 41, i at level 50,
format "'[' \maxr_ ( i | P ) '/ ' F ']'").
Reserved Notation "\maxr_ ( i : t | P ) F"
(at level 41, F at level 41, i at level 50,
only parsing).
Reserved Notation "\maxr_ ( i : t ) F"
(at level 41, F at level 41, i at level 50,
only parsing).
Reserved Notation "\maxr_ ( i < n | P ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \maxr_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\maxr_ ( i < n ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \maxr_ ( i < n ) F ']'").
Reserved Notation "\maxr_ ( i 'in' A | P ) F"
(at level 41, F at level 41, i, A at level 50,
format "'[' \maxr_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\maxr_ ( i 'in' A ) F"
(at level 41, F at level 41, i, A at level 50,
format "'[' \maxr_ ( i 'in' A ) '/ ' F ']'").
Section maxr.
Variable T : numDomainType.
Open Scope ring_scope.
Lemma max0r (x : T) : (0 <= x) -> (maxr 0 x = x) .
Lemma real_ler_maxr (x y z : T) :
x \is Num.real -> y \is Num.real -> z \is Num.real ->
(x <= maxr y z) = (x <= y) || (x <= z).
Lemma real_ltr_maxr (x y z : T) :
x \is Num.real -> y \is Num.real -> z \is Num.real ->
(x < maxr y z) = (x < y) || (x < z).
Lemma real_ler_maxl (x y z : T) :
x \is Num.real -> y \is Num.real -> z \is Num.real ->
(maxr x y <= z) = (x <= z) && (y <= z).
Lemma real_ltr_maxl (x y z : T) :
x \is Num.real -> y \is Num.real -> z \is Num.real ->
(maxr x y < z) = (x < z) && (y < z).
End maxr.
Notation "\maxr_ ( i <- r | P ) F" :=
(\big[Num.max/0%R]_(i <- r | P%B) F%R) : ring_scope.
Notation "\maxr_ ( i <- r ) F" :=
(\big[Num.max/0%R]_(i <- r) F%R) : ring_scope.
Notation "\maxr_ ( i | P ) F" :=
(\big[Num.max/0%R]_(i | P%B) F%R) : ring_scope.
Notation "\maxr_ i F" :=
(\big[Num.max/0%R]_i F%R) : ring_scope.
Notation "\maxr_ ( i : I | P ) F" :=
(\big[Num.max/0%R]_(i : I | P%B) F%R) (only parsing) : ring_scope.
Notation "\maxr_ ( i : I ) F" :=
(\big[Num.max/0%R]_(i : I) F%R) (only parsing) : ring_scope.
Notation "\maxr_ ( m <= i < n | P ) F" :=
(\big[Num.max/0%R]_(m <= i < n | P%B) F%R) : ring_scope.
Notation "\maxr_ ( m <= i < n ) F" :=
(\big[Num.max/0%R]_(m <= i < n) F%R) : ring_scope.
Notation "\maxr_ ( i < n | P ) F" :=
(\big[Num.max/0%R]_(i < n | P%B) F%R) : ring_scope.
Notation "\maxr_ ( i < n ) F" :=
(\big[Num.max/0%R]_(i < n) F%R) : ring_scope.
Notation "\maxr_ ( i 'in' A | P ) F" :=
(\big[Num.max/0%R]_(i in A | P%B) F%R) : ring_scope.
Notation "\maxr_ ( i 'in' A ) F" :=
(\big[Num.max/0%R]_(i in A) F%R) : ring_scope.
Section bigmax.
Variable R : numDomainType.
Open Scope ring_scope.
Lemma bigmax_pos (T: numDomainType) (I : Type) (F : I -> T) (s : seq I) :
(forall i, 0 <= F i) -> 0 <= \maxr_(i <- s) F i.
Lemma bigmax_ger (T: numDomainType) (I : eqType) (F : I -> T) (s : seq I) i :
(forall i, 0 <= F i) -> i \in s -> F i <= \maxr_(i <- s) F i.
Lemma bigmax_eq (T : numDomainType) (I : eqType) (F : I -> T) (s : seq I) :
(forall i, 0 <= F i) -> s != [::] ->
{k | (k \in s) && (F k == \maxr_(i <- s) F i)}.
Lemma bigmax_def (I : eqType) (F : I -> R) (s : seq I) x :
(forall i, 0 <= F i) -> {i | (x == F i) && (i \in s) } ->
(forall j, j \in s -> F j <= x) ->
\maxr_(k <- s) F k = x.
Lemma bigmax_distrl (I : eqType) (F : I -> R) (s : seq I) (r : R) :
0 <= r -> (r * \maxr_(i <- s) (F i)) = \maxr_(i <- s) (r * F i).
Lemma bigmax_ler_seq (I : eqType) (F1 F2 : I -> R) (s : seq I) :
(forall i, 0 <= F1 i) -> (forall i, i\in s -> F1 i <= F2 i) ->
\maxr_(i <- s) F1 i <= \maxr_(i <- s) F2 i.
Lemma bigmax_ler (I : finType) (F1 F2 : I -> R) :
(forall i, 0 <= F1 i) -> (forall i, F1 i <= F2 i) ->
\maxr_i F1 i <= \maxr_i F2 i.
Lemma bigmax_ler_sum (I : finType) (F1 F2 : I -> R) :
(forall i, 0 <= F1 i) -> (forall i, 0 <= F2 i) ->
\maxr_i (F1 i + F2 i) <= (\maxr_i F1 i) + \maxr_i F2 i.
Lemma bigmax_le_prod2 (I J : finType) (F1 : I -> R) (F2 : J -> R) :
(forall i, 0 <= F1 i) -> (forall j, 0 <= F2 j) ->
\maxr_i \maxr_j (F1 i * F2 j) <= (\maxr_i F1 i) * \maxr_j F2 j.
Lemma bigmax_le_prod (I : finType) (F1 F2 : I -> R) :
(forall i, 0 <= F1 i) -> (forall i, 0 <= F2 i) ->
\maxr_i (F1 i * F2 i) <= (\maxr_i F1 i) * \maxr_i F2 i.
Lemma bigmax_eq0 (I : eqType) (F : I -> R) (s : seq I) :
(forall i, i \in s -> F i = 0) -> \maxr_(i <- s) F i = 0.
Lemma map_bigmax (I : finType) (T1 : numDomainType)
(f : T1 -> R) (F : I -> T1) :
(forall i, 0 <= F i) -> (f 0 = 0) ->
(forall x y, x <= y -> f x <= f y) ->
f (\maxr_i F i) = \maxr_i f (F i).
End bigmax.
Section bigmin.
Import GRing.Theory.
Import Num.Theory.
Import Num.Def.
Variable R : numDomainType.
Open Scope ring_scope.
Fixpoint min_seq (s : seq R) :=
match s with
| [::] => 0
| [:: x] => x
| x :: s' => minr (min_seq s') x
end.
Definition min_fT (I : finType) (F : I -> R) := min_seq (map F (index_enum I)).
Lemma min_seq_real (s : seq R) : (forall x, x \in s -> x \is Num.real) ->
min_seq s \is Num.real.
Lemma min_seq_le (s : seq R) x : (forall x, x \in s -> x \is Num.real) ->
x \in s -> min_seq s <= x.
Lemma min_fT_le (I : finType) (F : I -> R) (i : I) :
(forall i, F i \is Num.real) -> min_fT F <= F i.
Lemma ex_min_fT (I : finType) (F : I -> R) (a : I) : {k | min_fT F = F k}.
End bigmin.
This page has been generated by coqdoc