Section Maximum.

Section Max_function.

Maximum, Minimum and Absolute Value



Let x and y be reals (we will define the maximum of x and y).

Variables x y : IR.

Definition Max_seq : N -> IR.
Defined.

Lemma Max_seq_char : forall n,
 0 [<] x[-]y and Max_seq n [=] x or x[-]y [<] one_div_succ n and Max_seq n [=] y.

Lemma Cauchy_Max_seq : Cauchy_prop Max_seq.

Definition Max_CauchySeq : CauchySeqR.
Defined.

Definition MAX : IR.
Defined.

Constructively, the elementary properties of the maximum function are:
  • x ≤ Max (x,y),
  • x ≤ Max (y,x),
  • z < Max(x,y) -> z < x or z < y.


(This can be more concisely expressed as z < Max(x,y) ⇔ z < x or z < y). From these elementary properties we can prove all other properties, including strong extensionality. With strong extensionality, we can make the binary operation Max. (So Max is MAX coupled with some proofs.)

Lemma lft_leEq_MAX : x [<=] MAX.

Lemma rht_leEq_MAX : y [<=] MAX.

Lemma less_MAX_imp : forall z : IR, z [<] MAX -> z [<] x or z [<] y.

End Max_function.

Lemma MAX_strext : bin_op_strext _ MAX.

Lemma MAX_wd : bin_op_wd IR MAX.

Section properties_of_Max.

Maximum


Definition Max := Build_CSetoid_bin_op _ MAX MAX_strext.

Lemma Max_wd_unfolded : forall x y x' y',
 x [=] x' -> y [=] y' -> Max x y [=] Max x' y'.

Lemma lft_leEq_Max : forall x y : IR, x [<=] Max x y.

Lemma rht_leEq_Max : forall x y : IR, y [<=] Max x y.

Lemma less_Max_imp : forall x y z : IR, z [<] Max x y -> z [<] x or z [<] y.

Lemma Max_leEq : forall x y z : IR, x [<=] z -> y [<=] z -> Max x y [<=] z.

Lemma Max_less : forall x y z : IR, x [<] z -> y [<] z -> Max x y [<] z.











Lemma equiv_imp_eq_max : forall x x' m, (forall y, x [<=] y -> x' [<=] y -> m [<=] y) ->
 (forall y, m [<=] y -> x [<=] y) -> (forall y, m [<=] y -> x' [<=] y) -> Max x x' [=] m.

Lemma Max_id : forall x : IR, Max x x [=] x.

Lemma Max_comm : forall x y : IR, Max x y [=] Max y x.

Lemma leEq_imp_Max_is_rht : forall x y : IR, x [<=] y -> Max x y [=] y.

Lemma Max_is_rht_imp_leEq : forall x y : IR, Max x y [=] y -> x [<=] y.

Lemma Max_minus_eps_leEq : forall x y e,
 0 [<] e -> {Max x y[-]e [<=] x} + {Max x y[-]e [<=] y}.

Lemma max_one_ap_zero : forall x : IR, Max x 1 [#] 0.

Lemma pos_max_one : forall x : IR, 0 [<] Max x 1.

Lemma x_div_Max_leEq_x :
 forall x y : IR, 0 [<] x -> (x[/] Max y 1[//]max_one_ap_zero _) [<=] x.

Lemma max_plus : forall (a b c : IR),
Max (a[+]c) (b[+]c) [=] Max a b [+] c.

Lemma max_mult : forall (a b c : IR), 0 [<=] c ->
(Max (c[*]a) (c[*]b)) [=] c[*](Max a b).

End properties_of_Max.

End Maximum.


Section Minimum.

Mininum



The minimum is defined by the formula Min(x,y) = −Max( −x,[--]y).

Definition MIN (x y : IR) : IR := [--] (Max [--]x [--]y).

Lemma MIN_wd : bin_op_wd _ MIN.

Lemma MIN_strext : bin_op_strext _ MIN.

Definition Min : CSetoid_bin_op IR := Build_CSetoid_bin_op _ MIN MIN_strext.

Lemma Min_wd_unfolded : forall x y a b,
 x [=] a /\ y [=] b -> (Min x y) [=] (Min a b).

Lemma Min_strext_unfolded : forall x y a b,
 (Min x y) [#] (Min a b) -> x [#] a or y [#] b.

Lemma Min_leEq_lft : forall x y : IR, Min x y [<=] x.

Lemma Min_leEq_rht : forall x y : IR, Min x y [<=] y.

Lemma Min_less_imp : forall x y z : IR, Min x y [<] z -> x [<] z or y [<] z.

Lemma leEq_Min : forall x y z : IR, z [<=] x -> z [<=] y -> z [<=] Min x y.

Lemma less_Min : forall x y z : IR, z [<] x -> z [<] y -> z [<] Min x y.

Lemma equiv_imp_eq_min : forall x x' m, (forall y, y [<=] x -> y [<=] x' -> y [<=] m) ->
 (forall y, y [<=] m -> y [<=] x) -> (forall y, y [<=] m -> y [<=] x') -> Min x x' [=] m.

Lemma Min_id : forall x : IR, Min x x [=] x.

Lemma Min_comm : forall x y : IR, Min x y [=] Min y x.

Lemma leEq_imp_Min_is_lft : forall x y : IR, x [<=] y -> Min x y [=] x.

Lemma Min_is_lft_imp_leEq : forall x y : IR, Min x y [=] x -> x [<=] y.

Lemma leEq_Min_plus_eps : forall x y e,
 0 [<] e -> {x [<=] Min x y[+]e} + {y [<=] Min x y[+]e}.

Variables a b : IR.

Lemma Min_leEq_Max : Min a b [<=] Max a b.

Lemma Min_leEq_Max' : forall z : IR, Min a z [<=] Max b z.

Lemma Min3_leEq_Max3 : forall c : IR, Min (Min a b) c [<=] Max (Max a b) c.

Lemma Min_less_Max : forall c d : IR, a [<] b -> Min a c [<] Max b d.

Lemma ap_imp_Min_less_Max : a [#] b -> Min a b [<] Max a b.

Lemma Min_less_Max_imp_ap : Min a b [<] Max a b -> a [#] b.

Lemma Max_monotone : forall (f: PartIR),
 (forall (x y:IR) Hx Hy, (Min a b)[<=]x -> x[<=]y -> y[<=](Max a b) ->
   (f x Hx)[<=](f y Hy)) ->
forall Ha Hb Hc, (Max (f a Ha) (f b Hb)) [=] f (Max a b) Hc.

Lemma Min_monotone : forall (f: PartIR),
 (forall (x y:IR) Hx Hy, (Min a b)[<=]x -> x[<=]y -> y[<=](Max a b) ->
   (f x Hx)[<=](f y Hy)) ->
forall Ha Hb Hc, (Min (f a Ha) (f b Hb)) [=] f (Min a b) Hc.

End Minimum.

Section Absolute.

Absolute value


Definition ABSIR (x : IR) : IR := Max x [--]x.

Lemma ABSIR_strext : un_op_strext _ ABSIR.


Lemma ABSIR_wd : un_op_wd _ ABSIR.

Definition AbsIR : CSetoid_un_op IR := Build_CSetoid_un_op _ ABSIR ABSIR_strext.

Lemma AbsIR_wd : forall x y : IR, x [=] y -> AbsIR x [=] AbsIR y.

Lemma AbsIR_wdl : forall x y e, x [=] y -> AbsIR x [<] e -> AbsIR y [<] e.

Lemma AbsIR_wdr : forall x y e, x [=] y -> e [<] AbsIR x -> e [<] AbsIR y.

Lemma AbsIRz_isz : AbsIR 0 [=] 0.


Lemma AbsIR_nonneg : forall x : IR, 0 [<=] AbsIR x.

Lemma AbsIR_pos : forall x : IR, x [#] 0 -> 0 [<] AbsIR x.

Lemma AbsIR_cancel_ap_zero : forall x : IR, AbsIR x [#] 0 -> x [#] 0.

Lemma AbsIR_resp_ap_zero : forall x : IR, x [#] 0 -> AbsIR x [#] 0.

Lemma leEq_AbsIR : forall x : IR, x [<=] AbsIR x.

Lemma inv_leEq_AbsIR : forall x : IR, [--]x [<=] AbsIR x.

Lemma AbsSmall_e : forall e x : IR, AbsSmall e x -> 0 [<=] e.

Lemma AbsSmall_imp_AbsIR : forall x y : IR, AbsSmall y x -> AbsIR x [<=] y.

Lemma AbsIR_eq_AbsSmall : forall x e : IR, [--]e [<=] x -> x [<=] e -> AbsSmall e x.

Lemma AbsIR_imp_AbsSmall : forall x y : IR, AbsIR x [<=] y -> AbsSmall y x.

Lemma AbsSmall_transitive : forall e x y : IR,
 AbsSmall e x -> AbsIR y [<=] AbsIR x -> AbsSmall e y.

Lemma zero_less_AbsIR_plus_one : forall q : IR, 0 [<] AbsIR q[+]1.

Lemma AbsIR_inv : forall x : IR, AbsIR x [=] AbsIR [--]x.

Lemma AbsIR_minus : forall x y : IR, AbsIR (x[-]y) [=] AbsIR (y[-]x).

Lemma AbsIR_mult : forall (x c: IR) (H : 0 [<=]c),
c[*] AbsIR (x) [=] AbsIR (c[*]x).

Lemma AbsIR_eq_x : forall x : IR, 0 [<=] x -> AbsIR x [=] x.

Lemma AbsIR_eq_inv_x : forall x : IR, x [<=] 0 -> AbsIR x [=] [--]x.

Lemma less_AbsIR : forall x y, 0 [<] x -> x [<] AbsIR y -> x [<] y or y [<] [--]x.

Lemma leEq_distr_AbsIR : forall x y : IR,
 0 [<] x -> x [<=] AbsIR y -> {x [<=] y} + {y [<=] [--]x}.







Lemma AbsIR_approach_zero : forall x, (forall e, 0 [<] e -> AbsIR x [<=] e) -> x [=] 0.

Lemma AbsSmall_approach :
forall (a b : IR),
  (forall (e : IR), 0[<]e -> AbsSmall (a[+]e) b) -> AbsSmall a b.



Lemma AbsIR_eq_zero : forall x : IR, AbsIR x [=] 0 -> x [=] 0.

Lemma Abs_Max : forall a b : IR, AbsIR (a[-]b) [=] Max a b[-]Min a b.

Lemma AbsIR_str_bnd : forall a b e : IR, AbsIR (a[-]b) [<] e -> b [<] a[+]e.

Lemma AbsIR_bnd : forall a b e : IR, AbsIR (a[-]b) [<=] e -> b [<=] a[+]e.

Lemma AbsIR_less : forall a b, a[<]b -> [--]b[<]a -> AbsIR a[<]b.

Lemma AbsIR_Qabs : forall (a:Q), AbsIR (inj_Q IR a)[=]inj_Q IR (Qabs a).

End Absolute.


Section SeqMax.

Bound of sequence


Variable seq : N -> IR.

Fixpoint SeqBound0 (n : N) : IR :=
    match n with
     | O => 0
     | S m => Max (AbsIR (seq m)) (SeqBound0 m)
    end.

Lemma SeqBound0_greater : forall (m n : N),
m < n -> AbsIR (seq m) [<=] SeqBound0 n.



End SeqMax.

Section Part_Function_Max.

Functional Operators



The existence of these operators allows us to lift them to functions. We will define the maximum, minimum and absolute value of two partial functions.

Let F,G:PartIR and denote by P and Q their respective domains.

Variables F G : PartIR.


Lemma part_function_Max_strext : forall x y (Hx : Conj P Q x) (Hy : Conj P Q y),
 Max (F x (Prj1 Hx)) (G x (Prj2 Hx)) [#] Max (F y (Prj1 Hy)) (G y (Prj2 Hy)) ->
 x [#] y.


Definition FMax := Build_PartFunct IR _ (conj_wd (dom_wd _ _) (dom_wd _ _))
 (fun x Hx => Max (F x (Prj1 Hx)) (G x (Prj2 Hx))) part_function_Max_strext.

End Part_Function_Max.

Section Part_Function_Abs.

Variables F G : PartIR.


Definition FMin := {--} (FMax {--}F {--}G).
Definition FAbs := FMax F {--}F.

Lemma FMin_char : forall x Hx Hx' Hx'', FMin x Hx [=] Min (F x Hx') (G x Hx'').


Lemma FAbs_char : forall x Hx Hx', FAbs x Hx [=] AbsIR (F x Hx').

End Part_Function_Abs.


Lemma FAbs_char' : forall F x Hx, AbsIR (FAbs F x Hx) [=] AbsIR (F x (ProjIR1 Hx)).

Lemma FAbs_nonneg : forall F x Hx, 0 [<=] FAbs F x Hx.


Section Inclusion.

Variables F G : PartIR.


Let R:IR->CProp.

Variable R : IR -> CProp.

Lemma included_FMax : ⊆ R P -> ⊆ R Q -> ⊆ R (Dom (FMax F G)).

Lemma included_FMax' : ⊆ R (Dom (FMax F G)) -> ⊆ R P.

Lemma included_FMax'' : ⊆ R (Dom (FMax F G)) -> ⊆ R Q.

Lemma included_FMin : ⊆ R P -> ⊆ R Q -> ⊆ R (Dom (FMin F G)).

Lemma included_FMin' : ⊆ R (Dom (FMin F G)) -> ⊆ R P.

Lemma included_FMin'' : ⊆ R (Dom (FMin F G)) -> ⊆ R Q.

Lemma included_FAbs : ⊆ R P -> ⊆ R (Dom (FAbs F)).

Lemma included_FAbs' : ⊆ R (Dom (FAbs F)) -> ⊆ R P.

End Inclusion.