Library Uprop

Uprop.v : Properties of operators on [0,1]

Require Export Utheory.
Require Export Arith.
Require Export Omega.

Open Local Scope U_scope.

Direct consequences of axioms

Lemma Uplus_le_compat_right : ∀ x y z:U, y ≤ z → x + y ≤ x + z.
Hint Resolve Uplus_le_compat_right.

Instance Uplus_mon2 : monotonic2 Uplus.
Save.
Hint Resolve Uplus_mon2.

Lemma Uplus_le_compat_left : ∀ x y z:U, x ≤ y → x + z ≤ y + z.
Hint Resolve Uplus_le_compat_left.

Lemma Uplus_le_compat : ∀ x y z t, x ≤ y → z ≤ t → x + z ≤ y + t.
Hint Immediate Uplus_le_compat.

Lemma Uplus_eq_compat_left : ∀ x y z:U, x ≈ y → x + z ≈ y + z.
Hint Resolve Uplus_eq_compat_left.

Lemma Uplus_eq_compat_right : ∀ x y z:U, x ≈ y → (z + x) ≈ (z + y).

Hint Resolve Uplus_eq_compat_left Uplus_eq_compat_right.

Add Morphism Uplus with signature Oeq ⇾ Oeq ⇾ Oeq as Uplus_eq_compat.
Qed.
Hint Immediate Uplus_eq_compat.

Add Morphism Uinv with signature Oeq ⇾ Oeq as Uinv_eq_compat.
Qed.
Hint Resolve Uinv_eq_compat.

Lemma Uplus_zero_right : ∀ x:U, x + 0 ≈ x.
Hint Resolve Uplus_zero_right.

Lemma Uinv_opp_left : ∀ x, [1-] x + x ≈ 1.
Hint Resolve Uinv_opp_left.

Lemma Uinv_opp_right : ∀ x, x + [1-] x ≈ 1.
Hint Resolve Uinv_opp_right.

Lemma Uinv_inv : ∀ x : U, [1-] [1-] x ≈ x.
Hint Resolve Uinv_inv.

Lemma Unit : ∀ x:U, x ≤ 1.
Hint Resolve Unit.

Lemma Uinv_zero : [1-] 0 = 1.

Lemma Ueq_class : ∀ x y:U, class (x ≈ y).

Lemma Ueq_double_neg : ∀ x y : U, ¬ ¬ (x ≈ y) → x ≈ y.
Hint Resolve Ueq_class.
Hint Immediate Ueq_double_neg.

Lemma Ule_orc : ∀ x y : U, orc (x ≤ y) (¬ x ≤ y).
Implicit Arguments Ule_orc [].

Lemma Ueq_orc : ∀ x y:U, orc (x ≈ y) (¬ x ≈ y).
Implicit Arguments Ueq_orc [].

Lemma Upos : ∀ x:U, 0 ≤ x.

Lemma Ule_0_1 : 0 ≤ 1.

Hint Resolve Upos Ule_0_1.

Properties of ≈ derived from properties of ≤

Definition UPlus : U -m > U -m > U := mon2 Uplus.

Definition UPlus_simpl : ∀ x y, UPlus x y = x+y.
Save.

Instance Uplus_continuous2 : continuous2 (mon2 Uplus).
Save.

Hint Resolve Uplus_continuous2.

Lemma Uplus_lub_eq : ∀ f g : nat -m > U,
lub f + lub g ≈ lub ((UPlus @² f) g).

Lemma Umult_le_compat_right : ∀ x y z:U, y ≤ z → x * y ≤ x * z.
Hint Resolve Umult_le_compat_right.

Instance Umult_mon2 : monotonic2 Umult.
Save.

Lemma Umult_le_compat_left : ∀ x y z:U, x ≤ y → x * z ≤ y * z.
Hint Resolve Umult_le_compat_left.

Lemma Umult_le_compat : ∀ x y z t, x ≤ y → z ≤ t → x * z ≤ y * t.
Hint Immediate Umult_le_compat.

Definition UMult : U -m > U -m > U := mon2 Umult.

Lemma Umult_eq_compat_left : ∀ x y z:U, x ≈ y → (x * z) ≈ (y * z).
Hint Resolve Umult_eq_compat_left.

Lemma Umult_eq_compat_right : ∀ x y z:U, x ≈ y → (z * x) ≈ (z * y).

Hint Resolve Umult_eq_compat_left Umult_eq_compat_right.

Definition UMult_simpl : ∀ x y, UMult x y = x*y.
Save.

Instance Umult_continuous2 : continuous2 (mon2 Umult).
Save.
Hint Resolve Umult_continuous2.

Lemma Umult_lub_eq : ∀ f g : nat -m > U,
lub f * lub g ≈ lub ((UMult @² f) g).

U is a setoid

Add Morphism Umult with signature Oeq ⇾ Oeq ⇾ Oeq
as Umult_eq_compat.
Qed.

Hint Immediate Umult_eq_compat.

Instance Uinv_mon : monotonic (o1:=Iord U) Uinv.
Save.

Definition UInv : U --m > U := mon (o1:=Iord U) Uinv.

Definition UInv_simpl : ∀ x, UInv x = [1-]x.
Save.

Lemma Ule_eq_compat :
∀ x1 x2 : U, x1 ≈ x2 → ∀ x3 x4 : U, x3 ≈ x4 → x1 ≤ x3 → x2 ≤ x4.

Definition and properties of x < y

Definition Ult (r1 r2:U) : Prop := ¬ (r2 ≤ r1).

Infix "<" := Ult : U_scope.

Hint Unfold Ult.

Add Morphism Ult with signature Oeq ⇾ Oeq ⇾ iff as Ult_eq_compat_iff.
Save.

Lemma Ult_eq_compat :
∀ x1 x2 : U, x1 ≈ x2 → ∀ x3 x4 : U, x3 ≈ x4 → x1 < x3 → x2 < x4.

Lemma Ult_class : ∀ x y, class (x<y).
Hint Resolve Ult_class.

Properties of x ≤ y

Lemma Ule_zero_eq : ∀ x:U, x ≤ 0 → x ≈ 0.

Lemma Uge_one_eq : ∀ x:U, 1 ≤ x → x ≈ 1.

Hint Immediate Ule_zero_eq Uge_one_eq.

Properties of x < y

Lemma Ult_neq : ∀ x y:U, x < y → ¬x ≈ y.

Lemma Ult_neq_rev : ∀ x y:U, x < y → ¬y ≈ x.

Lemma Ult_trans : ∀ x y z, x < y → y < z → x < z.

Lemma Ult_le : ∀ x y, x < y → x ≤ y.

Lemma Ule_diff_lt : ∀ x y : U, x ≤ y → ¬x ≈ y → x < y.

Hint Immediate Ult_neq Ult_neq_rev Ult_le.
Hint Resolve Ule_diff_lt.

Lemma Ult_neq_zero : ∀ x, ¬0 ≈ x → 0 < x.

Hint Resolve Ule_total Ult_neq_zero.

Properties of + and *

Lemma Udistr_plus_left : ∀ x y z, y ≤ [1-] z → x * (y + z) ≈ x * y + x * z.

Lemma Udistr_inv_left : ∀ x y, [1-](x * y) ≈ (x * ([1-] y)) + [1-] x.

Hint Resolve Uinv_eq_compat Udistr_plus_left Udistr_inv_left.

Lemma Uplus_perm2 : ∀ x y z:U, x + (y + z) ≈ y + (x + z).

Lemma Umult_perm2 : ∀ x y z:U, x * (y * z) ≈ y * (x * z).

Lemma Uplus_perm3 : ∀ x y z : U, (x + (y + z)) ≈ z + (x + y).

Lemma Umult_perm3 : ∀ x y z : U, (x * (y * z)) ≈ z * (x * y).

Hint Resolve Uplus_perm2 Umult_perm2 Uplus_perm3 Umult_perm3.

Lemma Uinv_simpl : ∀ x y : U, [1-] x ≈ [1-] y → x ≈ y.

Hint Immediate Uinv_simpl.

Lemma Umult_decomp : ∀ x y, x ≈ x * y + x * [1-]y.
Hint Resolve Umult_decomp.

More properties on + and * and Uinv

Lemma Umult_one_right : ∀ x:U, x * 1 ≈ x.
Hint Resolve Umult_one_right.

Lemma Umult_one_right_eq : ∀ x y:U, y ≈ 1 → x * y ≈ x.
Hint Resolve Umult_one_right_eq.

Lemma Umult_one_left_eq : ∀ x y:U, x ≈ 1 → x * y ≈ y.
Hint Resolve Umult_one_left_eq.

Lemma Udistr_plus_left_le : ∀ x y z : U, x * (y + z) ≤ x * y + x * z.

Lemma Uplus_eq_simpl_right :
∀ x y z:U, z ≤ [1-] x → z ≤ [1-] y → (x + z) ≈ (y + z) → x ≈ y.

Lemma Ule_plus_right : ∀ x y, x ≤ x + y.

Lemma Ule_plus_left : ∀ x y, y ≤ x + y.
Hint Resolve Ule_plus_right Ule_plus_left.

Lemma Ule_mult_right : ∀ x y, x * y ≤ x .

Lemma Ule_mult_left : ∀ x y, x * y ≤ y.
Hint Resolve Ule_mult_right Ule_mult_left.

Lemma Uinv_le_perm_right : ∀ x y:U, x ≤ [1-] y → y ≤ [1-] x.
Hint Immediate Uinv_le_perm_right.

Lemma Uinv_le_perm_left : ∀ x y:U, [1-] x ≤ y → [1-] y ≤ x.
Hint Immediate Uinv_le_perm_left.

Lemma Uinv_le_simpl : ∀ x y:U, [1-] x ≤ [1-] y → y ≤ x.
Hint Immediate Uinv_le_simpl.

Lemma Uinv_double_le_simpl_right : ∀ x y, x ≤ y → x ≤ [1-][1-]y.
Hint Resolve Uinv_double_le_simpl_right.

Lemma Uinv_double_le_simpl_left : ∀ x y, x ≤ y → [1-][1-]x ≤ y.
Hint Resolve Uinv_double_le_simpl_left.

Lemma Uinv_eq_perm_left : ∀ x y:U, x ≈ [1-] y → [1-] x ≈ y.
Hint Immediate Uinv_eq_perm_left.

Lemma Uinv_eq_perm_right : ∀ x y:U, [1-] x ≈ y → x ≈ [1-] y.

Hint Immediate Uinv_eq_perm_right.

Lemma Uinv_eq_simpl : ∀ x y:U, [1-] x ≈ [1-] y → x ≈ y.
Hint Immediate Uinv_eq_simpl.

Lemma Uinv_double_eq_simpl_right : ∀ x y, x ≈ y → x ≈ [1-][1-]y.
Hint Resolve Uinv_double_eq_simpl_right.

Lemma Uinv_double_eq_simpl_left : ∀ x y, x ≈ y → [1-][1-]x ≈ y.
Hint Resolve Uinv_double_eq_simpl_left.

Lemma Uinv_plus_right : ∀ x y, y ≤ [1-] x → [1-] (x + y) + y ≈ [1-] x.
Hint Resolve Uinv_plus_right.

Lemma Uplus_eq_simpl_left :
∀ x y z:U, x ≤ [1-] y → x ≤ [1-] z → (x + y) ≈ (x + z) → y ≈ z.

Lemma Uplus_eq_zero_left : ∀ x y:U, x ≤ [1-] y → (x + y) ≈ y → x ≈ 0.

Lemma Uinv_le_trans : ∀ x y z t, x ≤ [1-] y → z ≤ x → t ≤ y → z ≤ [1-] t.

Lemma Uinv_plus_left_le : ∀ x y, [1-]y ≤ [1-](x+y) +x.

Lemma Uinv_plus_right_le : ∀ x y, [1-]x ≤ [1-](x+y) +y.

Hint Resolve Uinv_plus_left_le Uinv_plus_right_le.

Disequality

Lemma neq_sym : ∀ x y:U, ¬x ≈ y → ¬y ≈ x.
Hint Immediate neq_sym.

Lemma Uinv_neq_compat : ∀ x y, ¬x ≈ y → ¬ [1-] x ≈ [1-] y.

Lemma Uinv_neq_simpl : ∀ x y, ¬ [1-] x ≈ [1-] y→ ¬x ≈ y.

Hint Resolve Uinv_neq_compat.
Hint Immediate Uinv_neq_simpl.

Lemma Uinv_neq_left : ∀ x y, ¬x ≈ [1-] y → ¬ [1-] x ≈ y.

Lemma Uinv_neq_right : ∀ x y, ¬ [1-] x ≈ y → ¬x ≈ [1-] y.

Properties of <

Lemma Ult_antirefl : ∀ x:U, ¬x < x.

Lemma Ult_0_1 : (0 < 1).

Lemma Ule_lt_trans : ∀ x y z:U, x ≤ y → y < z → x < z.

Lemma Ult_le_trans : ∀ x y z:U, x < y → y ≤ z → x < z.

Hint Resolve Ult_0_1 Ult_antirefl.

Lemma Ule_neq_zero : ∀ (x y:U), ¬0 ≈ x → x ≤ y → ¬ 0 ≈ y.

Lemma Uplus_neq_zero_left : ∀ x y, ¬0 ≈ x → ¬0 ≈ x+y.

Lemma Uplus_neq_zero_right : ∀ x y, ¬0 ≈ y → ¬0 ≈ x+y.

Lemma not_Ult_le : ∀ x y, ¬x < y → y ≤ x.

Lemma Ule_not_lt : ∀ x y, x ≤ y → ¬y < x.

Hint Immediate not_Ult_le Ule_not_lt.

Theorem Uplus_le_simpl_left : ∀ x y z : U, z ≤ [1-] x → z + x ≤ z + y → x ≤ y.

Lemma Uplus_lt_compat_left : ∀ x y z:U, z ≤ [1-] y → x < y → (x + z) < (y + z).

Lemma Uplus_lt_compat_right : ∀ x y z:U, z ≤ [1-] y → x < y → (z + x) < (z + y).

Hint Resolve Uplus_lt_compat_right Uplus_lt_compat_left.

Lemma Uplus_lt_compat :
∀ x y z t:U, z ≤ [1-] x → t ≤ [1-] y → x < y → z < t → (x + z) < (y + t).

Hint Immediate Uplus_lt_compat.

Lemma Uplus_lt_simpl_left : ∀ x y z:U, z ≤ [1-] y → (z + x) < (z + y) → x < y.

Lemma Uplus_lt_simpl_right : ∀ x y z:U, z ≤ [1-] y → (x + z) < (y + z) → x < y.

Lemma Uplus_one_le : ∀ x y, x + y ≈ 1 → [1-] y ≤ x.
Hint Immediate Uplus_one_le.

Theorem Uplus_eq_zero : ∀ x, x ≤ [1-] x → (x + x) ≈ x → x ≈ 0.

Lemma Umult_zero_left : ∀ x, 0 * x ≈ 0.
Hint Resolve Umult_zero_left.

Lemma Umult_zero_right : ∀ x, (x * 0) ≈ 0.
Hint Resolve Uplus_eq_zero Umult_zero_right.

Lemma Umult_zero_left_eq : ∀ x y, x ≈ 0 → x * y ≈ 0.

Lemma Umult_zero_right_eq : ∀ x y, y ≈ 0 → x * y ≈ 0.

Lemma Umult_zero_eq : ∀ x y z, x ≈ 0 → x * y ≈ x * z.

Compatibility of operations with respect to order.

Lemma Umult_le_simpl_right : ∀ x y z, ¬0 ≈ z → (x * z) ≤ (y * z) → x ≤ y.
Hint Resolve Umult_le_simpl_right.

Lemma Umult_simpl_right : ∀ x y z, ¬0 ≈ z → (x * z) ≈ (y * z) → x ≈ y.

Lemma Umult_simpl_left : ∀ x y z, ¬0 ≈ x → (x * y) ≈ (x * z) → y ≈ z.

Lemma Umult_lt_compat_left : ∀ x y z, ¬0 ≈ z→ x < y → (x * z) < (y * z).

Lemma Umult_lt_compat_right : ∀ x y z, ¬0 ≈ z → x < y → (z * x) < (z * y).

Lemma Umult_lt_simpl_right : ∀ x y z, ¬0 ≈ z → (x * z) < (y * z) → x < y.

Lemma Umult_lt_simpl_left : ∀ x y z, ¬0 ≈ z → (z * x) < (z * y) → x < y.

Hint Resolve Umult_lt_compat_left Umult_lt_compat_right.

Lemma Umult_zero_simpl_right : ∀ x y, 0 ≈ x*y → ¬0 ≈ x → 0 ≈ y.

Lemma Umult_zero_simpl_left : ∀ x y, 0 ≈ x*y → ¬0 ≈ y → 0 ≈ x.

Lemma Umult_neq_zero : ∀ x y, ¬0 ≈ x → ¬0 ≈ y → ¬0 ≈ x*y.
Hint Resolve Umult_neq_zero.

Lemma Umult_lt_zero : ∀ x y, 0 < x → 0 < y → 0 < x*y.
Hint Resolve Umult_lt_zero.

Lemma Umult_lt_compat : ∀ x y z t, x < y → z < t → x * z < y * t.

More Properties

Lemma Uplus_one : ∀ x y, [1-] x ≤ y → x + y ≈ 1.
Hint Resolve Uplus_one.

Lemma Uplus_one_right : ∀ x, x + 1 ≈ 1.

Lemma Uplus_one_left : ∀ x:U, 1 + x ≈ 1.
Hint Resolve Uplus_one_right Uplus_one_left.

Lemma Uinv_mult_simpl : ∀ x y z t, x ≤ [1-] y → (x * z) ≤ [1-] (y * t).
Hint Resolve Uinv_mult_simpl.

Lemma Umult_inv_plus : ∀ x y, x * [1-] y + y ≈ x + y * [1-] x.
Hint Resolve Umult_inv_plus.

Lemma Umult_inv_plus_le : ∀ x y z, y ≤ z → x * [1-] y + y ≤ x * [1-] z + z.
Hint Resolve Umult_inv_plus_le.

Lemma Uplus_lt_Uinv : ∀ x y, x+y < 1 → x ≤ [1-] y.

Lemma Uinv_lt_perm_left: ∀ x y : U, [1-] x < y → [1-] y < x.

Lemma Uinv_lt_perm_right: ∀ x y : U, x < [1-] y → y < [1-] x.

Hint Immediate Uinv_lt_perm_left Uinv_lt_perm_right.

Lemma Uinv_lt_one : ∀ x, 0 < x → [1-]x < 1.

Lemma Uinv_lt_zero : ∀ x, x < 1 → 0 < [1-]x.

Hint Resolve Uinv_lt_one Uinv_lt_zero.

Lemma orc_inv_plus_one : ∀ x y, orc (x ≤ [1-]y) (x+y ≈ 1).

Lemma Umult_lt_right : ∀ p q, p <1 → 0 < q → p * q < q.

Lemma Umult_lt_left : ∀ p q, 0 < p → q < 1 → p * q < p.

Hint Resolve Umult_lt_right Umult_lt_left.

Definition of x ^ n

Fixpoint Uexp (x:U) (n:nat) {struct n} : U :=
   match n with 0 ⇒ 1 | (S p) ⇒ x * Uexp x p end.

Infix "^" := Uexp : U_scope.

Lemma Uexp_1 : ∀ x, x^1 ≈ x.

Lemma Uexp_0 : ∀ x, x^0 ≈ 1.

Lemma Uexp_zero : ∀ n, (0<n)%nat → 0^n ≈ 0.

Lemma Uexp_one : ∀ n, 1^n ≈ 1.

Lemma Uexp_le_compat_right :
      ∀ x n m, (n ≤ m)%nat → x^m ≤ x^n.

Lemma Uexp_le_compat_left : ∀ x y n, x ≤ y → x^n ≤ y^n.
Hint Resolve Uexp_le_compat_left Uexp_le_compat_right.

Lemma Uexp_le_compat : ∀ x y (n m:nat),
        x ≤ y → n ≤ m → x^m ≤ y^n.

Instance Uexp_mon2 : monotonic2 (o1:=Iord U) (o3:=Iord U) Uexp.
Save.

Definition UExp : U --m > (nat -m → U ) := mon2 Uexp.

Add Morphism Uexp with signature Oeq ⇾ eq ⇾ Oeq as Uexp_eq_compat.
Save.

Lemma Uexp_inv_S : ∀ x n, ([1-]x^(S n)) ≈ x * ([1-]x^n)+[1-]x.

Lemma Uexp_lt_compat : ∀ p q n, (O <n)%nat → p<q → (p^n<q^n).

Hint Resolve Uexp_lt_compat.

Lemma Uexp_lt_zero : ∀ p n, (0<p) → (0<p^n).
Hint Resolve Uexp_lt_zero.

Lemma Uexp_lt_one : ∀ p n, (0<n)%nat → p<1 → (p^n<1).
Hint Resolve Uexp_lt_one.

Lemma Uexp_lt_antimon: ∀ p n m,
    (n<m)%nat→ 0 < p → p < 1 → p^m < p^n.
Hint Resolve Uexp_lt_antimon.

Properties of division

Lemma Udiv_mult : ∀ x y, ¬ 0 ≈ y → x ≤ y → (x/y) * y ≈ x.
Hint Resolve Udiv_mult.

Lemma Umult_div_le : ∀ x y, y * (x / y) ≤ x.
Hint Resolve Umult_div_le.

Lemma Udiv_mult_le : ∀ x y, (x/y) * y ≤ x.
Hint Resolve Udiv_mult_le.

Lemma Udiv_le_compat_left : ∀ x y z, x ≤ y → x/z ≤ y/z.
Hint Resolve Udiv_le_compat_left.

Lemma Udiv_eq_compat_left : ∀ x y z, x ≈ y → x/z ≈ y/z.
Hint Resolve Udiv_eq_compat_left.

Lemma Umult_div_le_left : ∀ x y z, ¬ 0 ≈ y → x*y ≤ z → x ≤ z/y.

Lemma Udiv_le_compat_right : ∀ x y z, ¬ 0 ≈ y → y ≤ z → x/z ≤ x/y.
Hint Resolve Udiv_le_compat_right.

Lemma Udiv_eq_compat_right : ∀ x y z, y ≈ z → x/z ≈ x/y.
Hint Resolve Udiv_eq_compat_right.

Add Morphism Udiv with signature Oeq ⇾ Oeq ⇾ Oeq as Udiv_eq_compat.
Save.

Add Morphism Udiv with signature Ole ++> Oeq ⇾ Ole as Udiv_le_compat.
Save.

Lemma Umult_div_eq : ∀ x y z, ¬ 0 ≈ y → x*y ≈ z → x ≈ z/y.

Lemma Umult_div_le_right : ∀ x y z, x ≤ y*z → x/z ≤ y.

Lemma Udiv_le : ∀ x y, ¬ 0 ≈ y → x ≤ x/y.

Lemma Udiv_zero : ∀ x, 0/x ≈ 0.
Hint Resolve Udiv_zero.

Lemma Udiv_zero_eq : ∀ x y, 0 ≈ x → x/y ≈ 0.
Hint Resolve Udiv_zero_eq.

Lemma Udiv_one : ∀ x, ¬ 0 ≈ x → x/1 ≈ x.
Hint Resolve Udiv_one.

Lemma Udiv_refl : ∀ x, ¬ 0 ≈ x → x/x ≈ 1.
Hint Resolve Udiv_refl.

Lemma Umult_div_assoc : ∀ x y z, y ≤ z→ (x*y) / z ≈ x * (y/z).

Lemma Udiv_mult_assoc : ∀ x y z, x ≤ y*z → x/(y*z) ≈ (x/y)/z.

Lemma Udiv_inv : ∀ x y, ¬ 0 ≈ y → [1-](x/y) ≤ ([1-]x)/y.

Lemma Uplus_div_inv : ∀ x y z, x+y ≤ z → x ≤ [1-]y → x/z ≤ [1-](y/z).
Hint Resolve Uplus_div_inv.

Lemma Udiv_plus_le : ∀ x y z, x/z + y/z ≤ (x+y)/z.
Hint Resolve Udiv_plus_le.

Lemma Udiv_plus : ∀ x y z, (x+y)/z ≈ x/z + y/z.
Hint Resolve Udiv_plus.

Instance Udiv_mon : ∀ k, monotonic (fun x ⇒ (x/k)).
Save.

Definition UDiv (k:U) : U -m > U := mon (fun x ⇒ (x/k)).

Lemma UDiv_simpl : ∀ (k:U) x, UDiv k x = x/k.

Definition and properties of x & y

A conjonction operation which coincides with min and mult on 0 and 1, see Morgan & McIver

Definition Uesp (x y:U) := [1-] ([1-] x + [1-] y).

Infix "&" := Uesp (left associativity, at level 40) : U_scope.

Lemma Uinv_plus_esp : ∀ x y, [1-] (x + y) ≈ [1-] x & [1-] y.
Hint Resolve Uinv_plus_esp.

Lemma Uinv_esp_plus : ∀ x y, [1-] (x & y) ≈ [1-] x + [1-] y.
Hint Resolve Uinv_esp_plus.

Lemma Uesp_sym : ∀ x y : U, x & y ≈ y & x.

Lemma Uesp_one_right : ∀ x : U, x & 1 ≈ x.

Lemma Uesp_one_left : ∀ x : U, 1 & x ≈ x.

Lemma Uesp_zero : ∀ x y, x ≤ [1-] y → x & y ≈ 0.

Hint Resolve Uesp_sym Uesp_one_right Uesp_one_left Uesp_zero.

Lemma Uesp_zero_right : ∀ x : U, x & 0 ≈ 0.

Lemma Uesp_zero_left : ∀ x : U, 0 & x ≈ 0.

Hint Resolve Uesp_zero_right Uesp_zero_left.

Add Morphism Uesp with signature Oeq ⇾ Oeq ⇾ Oeq as Uesp_eq_compat.
Save.

Lemma Uesp_le_compat : ∀ x y z t, x ≤ y → z ≤ t → x&z ≤ y&t.

Hint Immediate Uesp_le_compat Uesp_eq_compat.

Lemma Uesp_zero_one_mult_left : ∀ x y, orc (x ≈ 0) (x ≈ 1) → x & y ≈ x * y.

Lemma Uesp_zero_one_mult_right : ∀ x y, orc (y ≈ 0) (y ≈ 1) → x & y ≈ x * y.

Hint Resolve Uesp_zero_one_mult_left Uesp_zero_one_mult_right.

Instance Uesp_mon : monotonic2 Uesp.
Save.

Definition UEsp : U -m > U -m > U := mon2 Uesp.

Lemma UEsp_simpl : ∀ x y, UEsp x y = x & y.

Lemma Uesp_le_left : ∀ x y, x & y ≤ x.

Lemma Uesp_le_right : ∀ x y, x & y ≤ y.

Hint Resolve Uesp_le_left Uesp_le_right.

Lemma Uesp_plus_inv : ∀ x y, [1-] y ≤ x → x ≈ x & y + [1-] y.
Hint Resolve Uesp_plus_inv.

Lemma Uesp_le_plus_inv : ∀ x y, x ≤ x & y + [1-] y.
Hint Resolve Uesp_le_plus_inv.

Lemma Uplus_inv_le_esp : ∀ x y z, x ≤ y + ([1-] z) → x & z ≤ y.
Hint Immediate Uplus_inv_le_esp.

Definition and properties of x - y

Definition Uminus (x y:U) := [1-] ([1-] x + y).

Infix "-" := Uminus : U_scope.

Lemma Uminus_le_compat_left : ∀ x y z, x ≤ y → x - z ≤ y - z.

Lemma Uminus_le_compat_right : ∀ x y z, y ≤ z → x - z ≤ x - y.

Hint Resolve Uminus_le_compat_left Uminus_le_compat_right.

Lemma Uminus_le_compat : ∀ x y z t, x ≤ y → t ≤ z → x - z ≤ y - t.

Hint Immediate Uminus_le_compat.

Add Morphism Uminus with signature Oeq ⇾ Oeq ⇾ Oeq as Uminus_eq_compat.
Save.
Hint Immediate Uminus_eq_compat.

Lemma Uminus_zero_right : ∀ x, x - 0 ≈ x.

Lemma Uminus_one_left : ∀ x, 1 - x ≈ [1-] x.

Lemma Uminus_le_zero : ∀ x y, x ≤ y → x - y ≈ 0.

Hint Resolve Uminus_zero_right Uminus_one_left Uminus_le_zero.

Lemma Uminus_zero_left : ∀ x, 0 - x ≈ 0.
Hint Resolve Uminus_zero_left.

Lemma Uminus_one_right : ∀ x, x - 1 ≈ 0.
Hint Resolve Uminus_one_right.

Lemma Uminus_eq : ∀ x, x - x ≈ 0.
Hint Resolve Uminus_eq.

Lemma Uminus_le_left : ∀ x y, x - y ≤ x.

Hint Resolve Uminus_le_left.

Lemma Uminus_le_inv : ∀ x y, x - y ≤ [1-]y.
Hint Resolve Uminus_le_inv.

Lemma Uminus_plus_simpl : ∀ x y, y ≤ x → (x - y) + y ≈ x.

Lemma Uminus_plus_zero : ∀ x y, x ≤ y → (x - y) + y ≈ y.

Hint Resolve Uminus_plus_simpl Uminus_plus_zero.

Lemma Uminus_plus_le : ∀ x y, x ≤ (x - y) + y.

Hint Resolve Uminus_plus_le.

Lemma Uesp_minus_distr_left : ∀ x y z, (x & y) - z ≈ (x - z) & y.

Lemma Uesp_minus_distr_right : ∀ x y z, (x & y) - z ≈ x & (y - z).

Hint Resolve Uesp_minus_distr_left Uesp_minus_distr_right.

Lemma Uesp_minus_distr : ∀ x y z t, (x & y) - (z + t) ≈ (x - z) & (y - t).
Hint Resolve Uesp_minus_distr.

Lemma Uminus_esp_simpl_left : ∀ x y, [1-]x ≤ y → x - (x & y) ≈ [1-]y.

Lemma Uplus_esp_simpl : ∀ x y, (x - (x & y))+y ≈ x+y.
Hint Resolve Uminus_esp_simpl_left Uplus_esp_simpl.

Lemma Uminus_esp_le_inv : ∀ x y, x - (x & y) ≤ [1-]y.

Hint Resolve Uminus_esp_le_inv.

Lemma Uplus_esp_inv_simpl : ∀ x y, x ≤ [1-]y → (x + y) & [1-]y ≈ x.
Hint Resolve Uplus_esp_inv_simpl.

Lemma Uplus_inv_esp_simpl : ∀ x y, x ≤ y → (x + [1-]y) & y ≈ x.
Hint Resolve Uplus_inv_esp_simpl.

Definition and properties of max

Definition max (x y : U) : U := (x - y) + y.

Lemma max_eq_right : ∀ x y : U, y ≤ x → max x y ≈ x.

Lemma max_eq_left : ∀ x y : U, x ≤ y → max x y ≈ y.

Hint Resolve max_eq_right max_eq_left.

Lemma max_eq_case : ∀ x y : U, orc (max x y ≈ x) (max x y ≈ y).

Add Morphism max with signature Oeq ⇾ Oeq ⇾ Oeq as max_eq_compat.
Save.

Lemma max_le_right : ∀ x y : U, x ≤ max x y.

Lemma max_le_left : ∀ x y : U, y ≤ max x y.

Hint Resolve max_le_right max_le_left.

Lemma max_le : ∀ x y z : U, x ≤ z → y ≤ z → max x y ≤ z.

Lemma max_le_compat : ∀ x y z t: U, x ≤ y → z ≤ t → max x z ≤ max y t.
Hint Immediate max_le_compat.

Lemma max_idem : ∀ x, max x x ≈ x.
Hint Resolve max_idem.

Lemma max_sym_le : ∀ x y, max x y ≤ max y x.
Hint Resolve max_sym_le.

Lemma max_sym : ∀ x y, max x y ≈ max y x.
Hint Resolve max_sym.

Lemma max_assoc : ∀ x y z, max x (max y z) ≈ max (max x y) z.
Hint Resolve max_assoc.

Lemma max_0 : ∀ x, max 0 x ≈ x.
Hint Resolve max_0.

Instance max_mon : monotonic2 max.
Save.

Definition Max : U -m > U -m > U := mon2 max.

Lemma max_eq_mult : ∀ k x y, max (k*x) (k*y) ≈ k * max x y.

Lemma max_eq_plus_cte_right : ∀ x y k, max (x+k) (y+k) ≈ (max x y) + k.

Hint Resolve max_eq_mult max_eq_plus_cte_right.

Definition and properties of min

Definition min (x y : U) : U := [1-] ((y - x) + [1-]y).

Lemma min_eq_right : ∀ x y : U, x ≤ y → min x y ≈ x.

Lemma min_eq_left : ∀ x y : U, y ≤ x → min x y ≈ y.

Hint Resolve min_eq_right min_eq_left.

Lemma min_eq_case : ∀ x y : U, orc (min x y ≈ x) (min x y ≈ y).

Add Morphism min with signature Oeq ⇾ Oeq ⇾ Oeq as min_eq_compat.
Save.
Hint Immediate min_eq_compat.

Lemma min_le_right : ∀ x y : U, min x y ≤ x.

Lemma min_le_left : ∀ x y : U, min x y ≤ y.

Hint Resolve min_le_right min_le_left.

Lemma min_le : ∀ x y z : U, z ≤ x → z ≤ y → z ≤ min x y.

Lemma Uinv_min_max : ∀ x y, [1-](min x y) ≈ max ([1-]x) ([1-]y).

Lemma Uinv_max_min : ∀ x y, [1-](max x y) ≈ min ([1-]x) ([1-]y).

Lemma min_idem : ∀ x, min x x ≈ x.

Lemma min_mult : ∀ x y k,
    min (k * x) (k * y) ≈ k * (min x y).
Hint Resolve min_mult.

Lemma min_plus : ∀ x1 x2 y1 y2,
    (min x1 x2) + (min y1 y2) ≤ min (x1+y1) (x2+y2).
Hint Resolve min_plus.

Lemma min_plus_cte : ∀ x y k, min (x + k) (y + k) ≈ (min x y) + k.
Hint Resolve min_plus_cte.

Lemma min_le_compat : ∀ x1 y1 x2 y2,
      x1 ≤ y1 → x2 ≤ y2 → min x1 x2 ≤ min y1 y2.
Hint Immediate min_le_compat.

Lemma min_sym_le : ∀ x y, min x y ≤ min y x.
Hint Resolve min_sym_le.

Lemma min_sym : ∀ x y, min x y ≈ min y x.
Hint Resolve min_sym.

Lemma min_assoc : ∀ x y z, min x (min y z) ≈ min (min x y) z.
Hint Resolve min_assoc.

Lemma min_0 : ∀ x, min 0 x ≈ 0.
Hint Resolve min_0.

Instance min_mon2 : monotonic2 min.
Save.

Definition Min : U -m > U -m > U := mon2 min.

Lemma Min_simpl : ∀ x y, Min x y = min x y.

Lemma incr_decomp_aux : ∀ f g : nat -m > U,
     ∀ n1 n2, (∀ m, ¬ ((n1 ≤ m)%nat ∧ f n1 ≤ g m))
           → (∀ m, ~((n2 ≤ m)%nat ∧ g n2 ≤ f m)) → (n1 ≤ n2)%nat → False.

Lemma incr_decomp : ∀ f g: nat -m > U,
     orc (∀ n, exc (fun m ⇒ (n ≤ m)%nat ∧ f n ≤ g m))
           (∀ n, exc (fun m ⇒ (n ≤ m)%nat ∧ g n ≤ f m)).

Other properties

Lemma Uplus_minus_simpl_right : ∀ x y, y ≤ [1-] x → (x + y) - y ≈ x.
Hint Resolve Uplus_minus_simpl_right.

Lemma Uplus_minus_simpl_left : ∀ x y, y ≤ [1-] x → (x + y) - x ≈ y.

Lemma Uminus_assoc_left : ∀ x y z, (x - y) - z ≈ x - (y + z).

Hint Resolve Uminus_assoc_left.

Lemma Uminus_perm : ∀ x y z, (x - y) - z ≈ (x - z) - y.
Hint Resolve Uminus_perm.

Lemma Uminus_le_perm_left : ∀ x y z, y ≤ x → x - y ≤ z → x ≤ z + y.

Lemma Uplus_le_perm_left : ∀ x y z, x ≤ y + z → x - y ≤ z.

Lemma Uminus_eq_perm_left : ∀ x y z, y ≤ x → x - y ≈ z → x ≈ z + y.

Lemma Uplus_eq_perm_left : ∀ x y z, y ≤ [1-] z → x ≈ y + z → x - y ≈ z.

Hint Resolve Uminus_le_perm_left Uminus_eq_perm_left.
Hint Resolve Uplus_le_perm_left Uplus_eq_perm_left.

Lemma Uminus_le_perm_right : ∀ x y z, z ≤ y → x ≤ y - z → x + z ≤ y.

Lemma Uplus_le_perm_right : ∀ x y z, z ≤ [1-] x → x + z ≤ y → x ≤ y - z.
Hint Resolve Uminus_le_perm_right Uplus_le_perm_right.

Lemma Uminus_le_perm : ∀ x y z, z ≤ y → x ≤ [1-] z → x ≤ y - z → z ≤ y - x.
Hint Resolve Uminus_le_perm.

Lemma Uminus_eq_perm_right : ∀ x y z, z ≤ y → x ≈ y - z → x + z ≈ y.
Hint Resolve Uminus_eq_perm_right.

Lemma Uminus_plus_perm : ∀ x y z, y ≤ x → z ≤ [1-]x → (x - y) + z ≈ (x + z) - y.

Lemma Uminus_zero_le : ∀ x y, x - y ≈ 0 → x ≤ y.

Lemma Uminus_lt_non_zero : ∀ x y, x < y → ¬0 ≈ y - x.
Hint Immediate Uminus_zero_le Uminus_lt_non_zero.

Lemma Ult_le_nth_minus : ∀ x y, x < y → exc (fun n ⇒ x ≤ y - [1/]1+n).

Lemma Ult_le_nth_plus : ∀ x y, x < y → exc (fun n : nat ⇒ x + [1/]1+n ≤ y).

Lemma Uminus_distr_left : ∀ x y z, (x - y) * z ≈ (x * z) - (y * z).

Hint Resolve Uminus_distr_left.

Lemma Uminus_distr_right : ∀ x y z, x * (y - z) ≈ (x * y) - (x * z).

Hint Resolve Uminus_distr_right.

Lemma Uminus_assoc_right : ∀ x y z, y ≤ x → z ≤ y → x - (y - z) ≈ (x - y) + z.

Lemma Uplus_minus_assoc_right : ∀ x y z, y ≤ [1-]x → z ≤ y → x + (y - z) ≈ (x + y) - z.

Lemma Udiv_minus : ∀ x y z, ¬0 ≈ z → x ≤ z → (x - y) / z ≈ x/z - y/z.

Lemma Umult_inv_minus : ∀ x y, x * [1-]y ≈ x - x * y.
Hint Resolve Umult_inv_minus.

Lemma Uinv_mult_minus : ∀ x y, ([1-]x) * y ≈ y - x * y.
Hint Resolve Uinv_mult_minus.

Lemma Uminus_plus_perm_right : ∀ x y z, y ≤ x → y ≤ z → (x - y) + z ≈ x + (z - y).
Hint Resolve Uminus_plus_perm_right.

triangular inequality

Lemma Uminus_triangular : ∀ x y z, x - y ≤ (x - z) + (z - y).
Hint Resolve Uminus_triangular.

Definition and properties of generalized sums

Definition sigma : (nat → U) → nat -m > U.
Defined.

Lemma sigma_0 : ∀ (f : nat → U), sigma f O ≈ 0.

Lemma sigma_S : ∀ (f :nat → U) (n:nat), sigma f (S n) = (f n) + (sigma f n).

Lemma sigma_1 : ∀ (f : nat → U), sigma f (S 0) ≈ f O.

Lemma sigma_incr : ∀ (f : nat → U) (n m:nat), (n ≤ m)%nat → sigma f n ≤ sigma f m.

Hint Resolve sigma_incr.

Lemma sigma_eq_compat : ∀ (f g: nat → U) (n:nat),
(∀ k, (k < n)%nat → f k ≈ g k) → sigma f n ≈ sigma g n.

Lemma sigma_le_compat : ∀ (f g: nat → U) (n:nat),
(∀ k, (k < n)%nat → f k ≤ g k) → sigma f n ≤ sigma g n.

Lemma sigma_S_lift : ∀ (f :nat → U) (n:nat),
          sigma f (S n) ≈ (f O ) + (sigma (fun k ⇒ f (S k)) n).

Lemma sigma_plus_lift : ∀ (f :nat → U) (n m:nat),
          sigma f (n+m)%nat ≈ sigma f n + sigma (fun k ⇒ f (n+k)%nat) m.

Lemma sigma_zero : ∀ f n,
  (∀ k, (k<n)%nat → f k ≈ 0) → sigma f n ≈ 0.

Lemma sigma_not_zero : ∀ f n k, (k<n)%nat → 0 < f k → 0 < sigma f n.

Lemma sigma_zero_elim : ∀ f n,
  (sigma f n) ≈ 0 → ∀ k, (k<n)%nat → f k ≈ 0.

Hint Resolve sigma_eq_compat sigma_le_compat sigma_zero.

Lemma sigma_le : ∀ f n k, (k<n)%nat → f k ≤ sigma f n.
Hint Resolve sigma_le.

Lemma sigma_minus_decr : ∀ f n, (∀ k, f (S k) ≤ f k) →
         sigma (fun k ⇒ f k - f (S k)) n ≈ f O - f n.

Lemma sigma_minus_incr : ∀ f n, (∀ k, f k ≤ f (S k)) →
         sigma (fun k ⇒ f (S k) - f k) n ≈ f n - f O.

Definition and properties of generalized products

Definition prod (alpha : nat → U) (n:nat) := compn Umult 1 alpha n.

Lemma prod_0 : ∀ (f : nat → U), prod f 0 = 1.

Lemma prod_S : ∀ (f :nat → U) (n:nat), prod f (S n) = (f n) * (prod f n).

Lemma prod_1 : ∀ (f : nat → U), prod f (S 0) ≈ f O.

Lemma prod_S_lift : ∀ (f :nat → U) (n:nat),
          prod f (S n) ≈ (f O ) * (prod (fun k ⇒ f (S k)) n).

Lemma prod_decr : ∀ (f : nat → U) (n m:nat), (n ≤ m)%nat → prod f m ≤ prod f n.

Hint Resolve prod_decr.

Lemma prod_eq_compat : ∀ (f g: nat → U) (n:nat),
(∀ k, (k < n)%nat → f k ≈ g k) → (prod f n) ≈ (prod g n).

Lemma prod_le_compat : ∀ (f g: nat → U) (n:nat),
(∀ k, (k < n)%nat → f k ≤ g k) → prod f n ≤ prod g n.

Lemma prod_zero : ∀ f n k, (k<n)%nat → f k ≈ 0 → prod f n ≈ 0.

Lemma prod_not_zero : ∀ f n,
  (∀ k, (k<n)%nat → 0 < f k) → 0 < prod f n.

Lemma prod_zero_elim : ∀ f n,
  prod f n ≈ 0 → exc (fun k ⇒ (k<n)%nat ∧ f k ≈ 0).

Hint Resolve prod_eq_compat prod_le_compat prod_not_zero.

Lemma prod_le : ∀ f n k, (k<n)%nat → prod f n ≤ f k.

Lemma prod_minus : ∀ f n, prod f n - prod f (S n) ≈ ([1-]f n) * prod f n.

Definition Prod : (nat → U) → nat -m → U.
Defined.

Lemma Prod_simpl : ∀ f n, Prod f n = prod f n.
Hint Resolve Prod_simpl.

Properties of Unth

Lemma Unth_zero : [1/]1+0 ≈ 1.

Notation "½" := (Unth 1).

Lemma Unth_one : ½ ≈ [1-] ½.

Hint Resolve Unth_zero Unth_one.

Lemma Unth_one_plus : ½ + ½ ≈ 1.
Hint Resolve Unth_one_plus.

Lemma Unth_one_refl : ∀ t, ½ * t + ½ * t ≈ t.

Lemma Unth_not_null : ∀ n, ¬ (0 ≈ [1/]1+n).
Hint Resolve Unth_not_null.

Lemma Unth_lt_zero : ∀ n, 0 < [1/]1+n.
Hint Resolve Unth_lt_zero.

Lemma Unth_inv_lt_one : ∀ n, [1-][1/]1+n<1.
Hint Resolve Unth_inv_lt_one.

Lemma Unth_not_one : ∀ n, ¬ (1 ≈ [1-][1/]1+n).
Hint Resolve Unth_not_one.

Lemma Unth_prop_sigma : ∀ n, [1/]1+n ≈ [1-] (sigma (fun k ⇒ [1/]1+n) n).
Hint Resolve Unth_prop_sigma.

Lemma Unth_sigma_n : ∀ n : nat, ¬ (1 ≈ sigma (fun k ⇒ [1/]1+n) n).

Lemma Unth_sigma_Sn : ∀ n : nat, 1 ≈ sigma (fun k ⇒ [1/]1+n) (S n).

Hint Resolve Unth_sigma_n Unth_sigma_Sn.

Lemma Unth_decr : ∀ n, [1/]1+(S n) < [1/]1+n.
Hint Resolve Unth_decr.

Lemma Unth_anti_mon :
∀ n m, (n ≤ m)%nat → [1/]1+m ≤ [1/]1+n.
Hint Resolve Unth_anti_mon.

Lemma Unth_le_half : ∀ n, [1/]1+(S n) ≤ ½.
Hint Resolve Unth_le_half.

Mean of two numbers : ½ x + ½ y

Definition mean (x y:U) := ½ * x + ½ * y.

Lemma mean_eq : ∀ x:U, mean x x ≈ x.

Lemma mean_le_compat_right : ∀ x y z, y ≤ z → mean x y ≤ mean x z.

Lemma mean_le_compat_left : ∀ x y z, x ≤ y → mean x z ≤ mean y z.

Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right.

Lemma mean_lt_compat_right : ∀ x y z, y < z → mean x y < mean x z.

Lemma mean_lt_compat_left : ∀ x y z, x < y → mean x z < mean y z.

Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right.
Hint Resolve mean_lt_compat_left mean_lt_compat_right.

Lemma mean_le_up : ∀ x y, x ≤ y → mean x y ≤ y.

Lemma mean_le_down : ∀ x y, x ≤ y → x ≤ mean x y.

Lemma mean_lt_up : ∀ x y, x < y → mean x y < y.

Lemma mean_lt_down : ∀ x y, x < y → x < mean x y.

Hint Resolve mean_le_up mean_le_down mean_lt_up mean_lt_down.

Properties of ½

Lemma le_half_inv : ∀ x, x ≤ ½ → x ≤ [1-] x.

Hint Immediate le_half_inv.

Lemma ge_half_inv : ∀ x, ½ ≤ x → [1-] x ≤ x.

Hint Immediate ge_half_inv.

Lemma Uinv_le_half_left : ∀ x, x ≤ ½ → ½ ≤ [1-] x.

Lemma Uinv_le_half_right : ∀ x, ½ ≤ x → [1-] x ≤ ½.

Hint Resolve Uinv_le_half_left Uinv_le_half_right.

Lemma half_twice : ∀ x, x ≤ ½ → ½ * (x + x) ≈ x.

Lemma half_twice_le : ∀ x, ½ * (x + x) ≤ x.

Lemma Uinv_half : ∀ x, ½ * ([1-] x) + ½ ≈ [1-] ( ½ * x ).

Lemma Uinv_half_plus : ∀ x, [1-]x + ½ * x ≈ [1-] ( ½ * x ).

Lemma half_esp :
∀ x, (½ ≤ x) → (½ ) * (x & x) + ½ ≈ x.

Lemma half_esp_le : ∀ x, x ≤ ½ * (x & x) + ½.
Hint Resolve half_esp_le.

Lemma half_le : ∀ x y, y ≤ [1-] y → x ≤ y + y → (½ ) * x ≤ y.

Lemma half_Unth: ∀ n, (½ )*([1/]1+n) ≤ [1/]1+(S n).
Hint Resolve half_le half_Unth.

Lemma half_exp : ∀ n, ½ ^n ≈ ½ ^(S n) + ½ ^(S n).

Diff function : | x - y |

Definition diff (x y:U) := (x - y) + (y - x).

Lemma diff_eq : ∀ x, diff x x ≈ 0.
Hint Resolve diff_eq.

Lemma diff_sym : ∀ x y, diff x y ≈ diff y x.
Hint Resolve diff_sym.

Lemma diff_zero : ∀ x, diff x 0 ≈ x.
Hint Resolve diff_zero.

Add Morphism diff with signature Oeq ⇾ Oeq ⇾ Oeq as diff_eq_compat.
Qed.
Hint Immediate diff_eq_compat.

Lemma diff_plus_ok : ∀ x y, x - y ≤ [1-](y - x).
Hint Resolve diff_plus_ok.

Lemma diff_Uminus : ∀ x y, x ≤ y → diff x y ≈ y - x.

Lemma diff_Uplus_le : ∀ x y, x ≤ diff x y + y.
Hint Resolve diff_Uplus_le.

Lemma diff_triangular : ∀ x y z, diff x y ≤ diff x z + diff y z.
Hint Resolve diff_triangular.

Density

Lemma Ule_lt_lim : ∀ x y, (∀ t, t < x → t ≤ y) → x ≤ y.

Lemma Ule_nth_lim : ∀ x y, (∀ p, x ≤ y + [1/]1+p) → x ≤ y.

Properties of least upper bounds

Lemma lub_un : mlub (cte nat 1) ≈ 1.
Hint Resolve lub_un.

Lemma UPlusk_eq : ∀ k, UPlus k ≈ mon (Uplus k).

Lemma UMultk_eq : ∀ k, UMult k ≈ mon (Umult k).

Lemma UPlus_continuous_right : ∀ k, continuous (UPlus k).
Hint Resolve UPlus_continuous_right.

Lemma UPlus_continuous_left : continuous UPlus.
Hint Resolve UPlus_continuous_left.

Lemma UMult_continuous_right : ∀ k, continuous (UMult k).
Hint Resolve UMult_continuous_right.

Lemma UMult_continuous_left : continuous UMult.
Hint Resolve UMult_continuous_left.

Lemma lub_eq_plus_cte_left : ∀ (f:nat -m > U) (k:U), lub ((UPlus k) @ f) ≈ k + lub f.
Hint Resolve lub_eq_plus_cte_left.

Lemma lub_eq_mult : ∀ (k:U) (f:nat -m > U), lub ((UMult k) @ f) ≈ k * lub f.
Hint Resolve lub_eq_mult.

Lemma lub_eq_plus_cte_right : ∀ (f : nat -m > U) (k:U),
           lub ((mshift UPlus k) @ f) ≈ lub f + k.
Hint Resolve lub_eq_plus_cte_right.

Lemma min_lub_le : ∀ f g : nat -m > U,
         lub ((Min @² f) g) ≤ min (lub f) (lub g).

Lemma min_lub_le_incr_aux : ∀ f g : nat -m > U,
         (∀ n, exc (fun m ⇒ (n ≤ m)%nat ∧ f n ≤ g m))
         → min (lub f) (lub g) ≤ lub ((Min @² f) g).

Lemma min_lub_le_incr : ∀ f g : nat -m > U,
         min (lub f) (lub g) ≤ lub ((Min @² f) g).

Lemma min_continuous2 : continuous2 Min.
Hint Resolve min_continuous2.

Lemma lub_eq_esp_right :
  ∀ (f : nat -m > U) (k : U), lub ((mshift UEsp k) @ f) ≈ lub f & k.
Hint Resolve lub_eq_esp_right.

Lemma Udiv_continuous : ∀ (k:U), continuous (UDiv k).
Hint Resolve Udiv_continuous.

Greatest lower bounds

Definition glb (f:nat -m → U) := [1-](lub (UInv @ f)).

Lemma glb_le: ∀ (f : nat -m → U) (n : nat), glb f ≤ (f n).

Lemma le_glb: ∀ (f : nat -m → U) (x:U),
      (∀ n : nat, x ≤ f n) → x ≤ glb f.
Hint Resolve glb_le le_glb.

Definition Uopp : cpo (o:=Iord U) U.
Defined.

Lemma Uopp_lub_simpl
   : ∀ h : nat -m → U, lub (cpo:=Uopp) h = glb h.

Lemma Uopp_mon_seq : ∀ f:nat -m → U,
   ∀ n m:nat, (n ≤ m)%nat → f m ≤ f n.
Hint Resolve Uopp_mon_seq.

Infinite product: Π(i=0..∞) f i

Definition prod_inf (f : nat → U) : U := glb (Prod f).

Properties of glb

Lemma glb_le_compat:
  ∀ f g : nat -m → U, (∀ x, f x ≤ g x) → glb f ≤ glb g.
Hint Resolve glb_le_compat.

Lemma glb_eq_compat:
  ∀ f g : nat -m → U, f ≈ g → glb f ≈ glb g.
Hint Resolve glb_eq_compat.

Lemma glb_cte: ∀ c : U, glb (mon (cte nat (o1:=(Iord U)) c)) ≈ c.
Hint Resolve glb_cte.

Lemma glb_eq_plus_cte_right:
  ∀ (f : nat -m → U) (k : U), glb (Imon (mshift UPlus k) @ f) ≈ glb f + k.
Hint Resolve glb_eq_plus_cte_right.

Lemma glb_eq_plus_cte_left:
  ∀ (f : nat -m → U) (k : U), glb (Imon (UPlus k) @ f) ≈ k + glb f.
Hint Resolve glb_eq_plus_cte_left.

Lemma glb_eq_mult:
  ∀ (k : U) (f : nat -m → U), glb (Imon (UMult k) @ f) ≈ k * glb f.

Lemma Imon2_plus_continuous
       : continuous2 (c1:=Uopp) (c2:=Uopp) (c3:=Uopp) (imon2 Uplus).

Hint Resolve Imon2_plus_continuous.

Lemma Uinv_continuous : continuous (c1:=Uopp) UInv.

Lemma Uinv_lub_eq : ∀ f : nat -m → U, [1-](lub (cpo:=Uopp) f) ≈ lub (UInv@f).

Lemma Uinvopp_mon : monotonic (o2:= Iord U) Uinv.
Hint Resolve Uinvopp_mon.

Definition UInvopp : U -m → U
   := mon (o2:= Iord U) Uinv (fmonotonic:=Uinvopp_mon).

Lemma UInvopp_simpl : ∀ x, UInvopp x = [1-]x.

Lemma Uinvopp_continuous : continuous (c2:=Uopp) UInvopp.

Lemma Uinvopp_lub_eq
   : ∀ f : nat -m > U, [1-](lub f) ≈ lub (cpo:=Uopp) (UInvopp@f).

Hint Resolve Uinv_continuous Uinvopp_continuous.

Instance Uminus_mon2 : monotonic2 (o2:=Iord U) Uminus.
Save.

Definition UMinus : U -m > U --m > U := mon2 Uminus.

Lemma UMinus_simpl : ∀ x y, UMinus x y = x - y.

Lemma Uminus_continuous2 : continuous2 (c2:=Uopp) UMinus.
Hint Resolve Uminus_continuous2.

Lemma glb_le_esp : ∀ f g :nat -m → U, (glb f) & (glb g) ≤ glb ((imon2 Uesp @² f) g).
Hint Resolve glb_le_esp.

Lemma Uesp_min : ∀ a1 a2 b1 b2, min a1 b1 & min a2 b2 ≤ min (a1 & a2) (b1 & b2).

Defining lubs of arbitrary sequences

Fixpoint seq_max (f:nat → U) (n:nat) : U := match n with
             O ⇒ f O | S p ⇒ max (seq_max f p) (f (S p)) end.

Lemma seq_max_incr : ∀ f n, seq_max f n ≤ seq_max f (S n).
Hint Resolve seq_max_incr.

Lemma seq_max_le : ∀ f n, f n ≤ seq_max f n.
Hint Resolve seq_max_le.

Instance seq_max_mon : ∀ (f:nat → U), monotonic (seq_max f).
Save.

Definition sMax (f:nat → U) : nat -m > U := mon (seq_max f).

Lemma sMax_mult : ∀ k (f:nat→U), sMax (fun n ⇒ k * f n) ≈ UMult k @ sMax f.

Lemma sMax_plus_cte_right : ∀ k (f:nat→ U),
    sMax (fun n ⇒ f n + k) ≈ mshift UPlus k @ sMax f.

Definition Ulub (f:nat → U) := lub (sMax f).

Lemma le_Ulub : ∀ f n, f n ≤ Ulub f.

Lemma Ulub_le : ∀ f x, (∀ n, f n ≤ x) → Ulub f ≤ x.

Hint Resolve le_Ulub Ulub_le.

Lemma Ulub_le_compat : ∀ f g : nat→U, f ≤ g → Ulub f ≤ Ulub g.
Hint Resolve Ulub_le_compat.

Add Morphism Ulub with signature Oeq ⇾ Oeq as Ulub_eq_compat.
Save.
Hint Resolve Ulub_eq_compat.

Lemma Ulub_eq_mult : ∀ k (f:nat→U), Ulub (fun n ⇒ k * f n) ≈ k * Ulub f.

Lemma Ulub_eq_plus_cte_right : ∀ (f:nat→U) k, Ulub (fun n ⇒ f n + k) ≈ Ulub f + k.

Hint Resolve Ulub_eq_mult Ulub_eq_plus_cte_right.

Lemma Ulub_eq_esp_right :
  ∀ (f : nat → U) (k : U), Ulub (fun n ⇒ f n & k) ≈ Ulub f & k.
Hint Resolve lub_eq_esp_right.

Lemma Ulub_le_plus : ∀ f g, Ulub (fun n ⇒ f n + g n) ≤ Ulub f + Ulub g.
Hint Resolve Ulub_le_plus.

Definition Uglb (f:nat → U) :U := [1-]Ulub (fun n ⇒ [1-](f n)).

Lemma Uglb_le: ∀ (f : nat → U) (n : nat), Uglb f ≤ f n.

Lemma le_Uglb: ∀ (f : nat → U) (x:U),
  (∀ n : nat, x ≤ f n) → x ≤ Uglb f.
Hint Resolve Uglb_le le_Uglb.

Lemma Uglb_le_compat : ∀ f g : nat → U, f ≤ g → Uglb f ≤ Uglb g.
Hint Resolve Uglb_le_compat.

Add Morphism Uglb with signature Oeq ⇾ Oeq as Uglb_eq_compat.
Save.
Hint Resolve Uglb_eq_compat.

Lemma Uglb_eq_plus_cte_right:
  ∀ (f : nat → U) (k : U), Uglb (fun n ⇒ f n + k) ≈ Uglb f + k.
Hint Resolve Uglb_eq_plus_cte_right.

Lemma Uglb_eq_mult:
  ∀ (k : U) (f : nat → U), Uglb (fun n ⇒ k * f n) ≈ k * Uglb f.
Hint Resolve Uglb_eq_mult Uglb_eq_plus_cte_right.

Lemma Uglb_le_plus : ∀ f g, Uglb f + Uglb g ≤ Uglb (fun n ⇒ f n + g n).
Hint Resolve Uglb_le_plus.

Lemma Ulub_lub : ∀ f:nat -m > U, Ulub f ≈ lub f.
Hint Resolve Ulub_lub.

Lemma Uglb_glb : ∀ f:nat -m → U, Uglb f ≈ glb f.
Hint Resolve Uglb_glb.

Lemma lub_le_plus : ∀ (f g : nat -m > U), lub ((UPlus @² f) g) ≤ lub f + lub g.
Hint Resolve lub_le_plus.

Lemma glb_le_plus : ∀ (f g:nat -m → U) , glb f + glb g ≤ glb ((Imon2 UPlus @² f) g).
Hint Resolve glb_le_plus.

Lemma lub_eq_plus : ∀ f g : nat -m > U, lub ((UPlus @² f) g) ≈ lub f + lub g.
Hint Resolve lub_eq_plus.

Lemma glb_mon : ∀ f : nat -m > U, Uglb f ≈ f O.

Lemma lub_inv : ∀ (f g : nat -m > U), (∀ n, f n ≤ [1-] g n) → lub f ≤ [1-] (lub g).

Lemma glb_lift_left : ∀ (f:nat -m → U) n,
     glb f ≈ glb (mon (seq_lift_left f n)).
Hint Resolve glb_lift_left.

Lemma Ulub_mon : ∀ f : nat -m → U, Ulub f ≈ f O.

Lemma lub_glb_le : ∀ (f:nat -m > U) (g:nat -m → U),
      (∀ n, f n ≤ g n) → lub f ≤ glb g.

Lemma lub_lub_inv_le : ∀ f g :nat -m > U,
      (∀ n, f n ≤ [1-]g n) → lub f ≤ [1-] lub g.

Lemma Uplus_opp_continuous_right :
     ∀ k, continuous (c1:=Uopp) (c2:=Uopp) (Imon (UPlus k)).

Lemma Uplus_opp_continuous_left :
     continuous (c1:=Uopp) (c2:=fmon_cpo (o:=Iord U) (c:=Uopp))(Imon2 UPlus).

Hint Resolve Uplus_opp_continuous_right Uplus_opp_continuous_left.

Instance Uplusopp_continuous2 : continuous2 (c1:=Uopp) (c2:=Uopp) (c3:=Uopp) (Imon2 UPlus).
Save.

Lemma Uplusopp_lub_eq : ∀ (f g : nat -m → U),
    lub (cpo:=Uopp) f + lub (cpo:=Uopp) g ≈ lub (cpo:=Uopp) ((Imon2 UPlus @² f) g).

Lemma glb_eq_plus : ∀ (f g : nat -m → U), glb ((Imon2 UPlus @² f) g) ≈ glb f + glb g.
Hint Resolve glb_eq_plus.

Instance UEsp_continuous2 : continuous2 UEsp.
Save.

Lemma Uesp_lub_eq : ∀ f g : nat -m > U, lub f & lub g ≈ lub ((UEsp @² f) g).

Instance sigma_mon :monotonic sigma.
Save.

Definition Sigma : (nat → U ) -m > nat -m > U
    := mon sigma (fmonotonic:=sigma_mon).

Lemma Sigma_simpl : ∀ f, Sigma f = sigma f.

Lemma sigma_continuous1 : continuous Sigma.

Lemma sigma_lub1 : ∀ (f : nat -m > (nat → U )) n,
       sigma (lub f) n ≈ lub ((mshift Sigma n) @ f).

Definition MF (A:Type) : Type := A → U.

Lemma MFcpo (A:Type) : cpo (MF A).

Definition MFopp (A:Type) : cpo (o:=Iord (A → U)) (MF A).
Defined.

Lemma MFopp_lub_eq : ∀ (A:Type) (h:nat -m → MF A),
      lub (cpo:=MFopp A) h ≈ fun x ⇒ glb (Iord_app x @ h).

Lemma fle_intro : ∀ (A:Type) (f g : MF A), (∀ x, f x ≤ g x) → f ≤ g.
Hint Resolve fle_intro.

Lemma feq_intro : ∀ (A:Type) (f g : MF A), (∀ x, f x ≈ g x) → f ≈ g.
Hint Resolve feq_intro.

Definition fplus (A:Type) (f g : MF A) : MF A :=
               fun x ⇒ f x + g x.

Definition fmult (A:Type) (k:U) (f : MF A) : MF A :=
               fun x ⇒ k * f x.

Definition finv (A:Type) (f : MF A) : MF A :=
               fun x ⇒ [1-] f x.

Definition fzero (A:Type) : MF A :=
               fun x ⇒ 0.

Definition fdiv (A:Type) (k:U) (f : MF A) : MF A :=
               fun x ⇒ (f x) / k.

Definition flub (A:Type) (f : nat -m > MF A) : MF A := lub f.

Lemma fplus_simpl : ∀ (A:Type)(f g : MF A) (x : A),
                             fplus f g x = f x + g x.

Lemma fplus_def : ∀ (A:Type)(f g : MF A),
                             fplus f g = fun x ⇒ f x + g x.

Lemma fmult_simpl : ∀ (A:Type)(k:U) (f : MF A) (x : A),
                             fmult k f x = k * f x.

Lemma fmult_def : ∀ (A:Type)(k:U) (f : MF A),
                             fmult k f = fun x ⇒ k * f x.

Lemma fdiv_simpl : ∀ (A:Type)(k:U) (f : MF A) (x : A),
                             fdiv k f x = f x / k.

Lemma fdiv_def : ∀ (A:Type)(k:U) (f : MF A),
                             fdiv k f = fun x ⇒ f x / k.

Implicit Arguments fzero [].

Lemma fzero_simpl : ∀ (A:Type)(x : A), fzero A x = 0.

Lemma fzero_def : ∀ (A:Type), fzero A = fun x:A ⇒ 0.

Lemma finv_simpl : ∀ (A:Type)(f : MF A) (x : A), finv f x = [1-]f x.

Lemma finv_def : ∀ (A:Type)(f : MF A), finv f = fun x ⇒ [1-](f x).

Lemma flub_simpl : ∀ (A:Type)(f:nat -m > MF A) (x:A),
                           (flub f) x = lub (f <o > x).

Lemma flub_def : ∀ (A:Type)(f:nat -m > MF A),
                           (flub f) = fun x ⇒ lub (f <o > x).

Hint Resolve fplus_simpl fmult_simpl fzero_simpl finv_simpl flub_simpl.

Definition fone (A:Type) : MF A := fun x ⇒ 1.
Implicit Arguments fone [].

Lemma fone_simpl : ∀ (A:Type) (x:A), fone A x = 1.

Lemma fone_def : ∀ (A:Type), fone A = fun (x:A) ⇒ 1.

Definition fcte (A:Type) (k:U): MF A := fun x ⇒ k.
Implicit Arguments fcte [].

Lemma fcte_simpl : ∀ (A:Type) (k:U) (x:A), fcte A k x = k.

Lemma fcte_def : ∀ (A:Type) (k:U), fcte A k = fun (x:A) ⇒ k.

Definition fminus (A:Type) (f g :MF A) : MF A := fun x ⇒ f x - g x.

Lemma fminus_simpl : ∀ (A:Type) (f g: MF A) (x:A), fminus f g x = f x - g x.

Lemma fminus_def : ∀ (A:Type) (f g: MF A), fminus f g = fun x ⇒ f x - g x.

Definition fesp (A:Type) (f g :MF A) : MF A := fun x ⇒ f x & g x.

Lemma fesp_simpl : ∀ (A:Type) (f g: MF A) (x:A), fesp f g x = f x & g x.

Lemma fesp_def : ∀ (A:Type) (f g: MF A) , fesp f g = fun x ⇒ f x & g x.

Definition fconj (A:Type)(f g:MF A) : MF A := fun x ⇒ f x * g x.

Lemma fconj_simpl : ∀ (A:Type) (f g: MF A) (x:A), fconj f g x = f x * g x.

Lemma fconj_def : ∀ (A:Type) (f g: MF A), fconj f g = fun x ⇒ f x * g x.

Lemma MF_lub_simpl : ∀ (A:Type) (f : nat -m > MF A) (x:A),
             lub f x = lub (f <o >x).
Hint Resolve MF_lub_simpl.

Lemma MF_lub_def : ∀ (A:Type) (f : nat -m > MF A),
             lub f = fun x ⇒ lub (f <o >x).

Defining morphisms

Lemma fplus_eq_compat : ∀ A (f1 f2 g1 g2:MF A),
          f1 ≈ f2 → g1 ≈ g2 → fplus f1 g1 ≈ fplus f2 g2.

Add Parametric Morphism (A:Type) : (@fplus A)
    with signature Oeq ⇾ Oeq ⇾ Oeq
    as fplus_feq_compat_morph.
Save.

Instance fplus_mon2 : ∀ A, monotonic2 (fplus (A:=A)).
Save.
Hint Resolve fplus_mon2.

Lemma fplus_le_compat : ∀ A (f1 f2 g1 g2:MF A),
          f1 ≤ f2 → g1 ≤ g2 → fplus f1 g1 ≤ fplus f2 g2.

Add Parametric Morphism A : (@fplus A) with signature Ole ++> Ole ++> Ole
    as fplus_fle_compat_morph.
Save.

Lemma finv_eq_compat : ∀ A (f g:MF A), f ≈ g → finv f ≈ finv g.

Add Parametric Morphism A : (@finv A) with signature Oeq ⇾ Oeq
    as finv_feq_compat_morph.
Save.

Instance finv_mon : ∀ A, monotonic (o2:=Iord (MF A)) (finv (A:=A)).
Save.
Hint Resolve finv_mon.

Lemma finv_le_compat : ∀ A (f g:MF A), f ≤ g → finv g ≤ finv f.

Add Parametric Morphism A: (@finv A)
   with signature Ole --> Ole as finv_fle_compat_morph.
Save.

Lemma fmult_eq_compat : ∀ A k1 k2 (f1 f2:MF A),
          k1 ≈ k2 → f1 ≈ f2 → fmult k1 f1 ≈ fmult k2 f2.

Add Parametric Morphism A : (@fmult A)
   with signature Oeq ⇾ Oeq ⇾ Oeq as fmult_feq_compat_morph.
Save.

Instance fmult_mon2 : ∀ A, monotonic2 (fmult (A:=A)).
Save.
Hint Resolve fmult_mon2.

Lemma fmult_le_compat : ∀ A k1 k2 (f1 f2:MF A),
          k1 ≤ k2 → f1 ≤ f2 → fmult k1 f1 ≤ fmult k2 f2.

Add Parametric Morphism A : (@fmult A)
    with signature Ole ++> Ole ++> Ole as fmult_fle_compat_morph.
Save.

Lemma fminus_eq_compat : ∀ A (f1 f2 g1 g2:MF A),
          f1 ≈ f2 → g1 ≈ g2 → fminus f1 g1 ≈ fminus f2 g2.

Add Parametric Morphism A : (@fminus A)
    with signature Oeq ⇾ Oeq ⇾ Oeq as fminus_feq_compat_morph.
Save.

Instance fminus_mon2 : ∀ A, monotonic2 (o2:=Iord (MF A)) (fminus (A:=A)).
Save.
Hint Resolve fminus_mon2.

Lemma fminus_le_compat : ∀ A (f1 f2 g1 g2:MF A),
          f1 ≤ f2 → g2 ≤ g1 → fminus f1 g1 ≤ fminus f2 g2.

Add Parametric Morphism A : (@fminus A)
    with signature Ole ++> Ole --> Ole as fminus_fle_compat_morph.
Save.

Lemma fesp_eq_compat : ∀ A (f1 f2 g1 g2:MF A),
          f1 ≈ f2 → g1 ≈ g2 → fesp f1 g1 ≈ fesp f2 g2.

Add Parametric Morphism A : (@fesp A) with signature Oeq ⇾ Oeq ⇾ Oeq as fesp_feq_compat_morph.
Save.

Instance fesp_mon2 : ∀ A, monotonic2 (fesp (A:=A)).
Save.
Hint Resolve fesp_mon2.

Lemma fesp_le_compat : ∀ A (f1 f2 g1 g2:MF A),
          f1 ≤ f2 → g1 ≤ g2 → fesp f1 g1 ≤ fesp f2 g2.

Add Parametric Morphism A : (@fesp A)
   with signature Ole ++> Ole ++> Ole as fesp_fle_compat_morph.
Save.

Lemma fconj_eq_compat : ∀ A (f1 f2 g1 g2:MF A),
           f1 ≈ f2 → g1 ≈ g2 → fconj f1 g1 ≈ fconj f2 g2.

Add Parametric Morphism A : (@fconj A)
   with signature Oeq ⇾ Oeq ⇾ Oeq
as fconj_feq_compat_morph.
Save.

Instance fconj_mon2 : ∀ A, monotonic2 (fconj (A:=A)).
Save.
Hint Resolve fconj_mon2.

Lemma fconj_le_compat : ∀ A (f1 f2 g1 g2:MF A),
           f1 ≤ f2 → g1 ≤ g2 → fconj f1 g1 ≤ fconj f2 g2.

Add Parametric Morphism A : (@fconj A) with signature Ole ++> Ole ++> Ole
as fconj_fle_compat_morph.
Save.

Hint Immediate fplus_le_compat fplus_eq_compat fesp_le_compat fesp_eq_compat
fmult_le_compat fmult_eq_compat fminus_le_compat fminus_eq_compat
fconj_eq_compat.

Hint Resolve finv_eq_compat.

Elementary properties

Lemma fle_fplus_left : ∀ (A:Type) (f g : MF A), f ≤ fplus f g.

Lemma fle_fplus_right : ∀ (A:Type) (f g : MF A), g ≤ fplus f g.

Lemma fle_fmult : ∀ (A:Type) (k:U)(f : MF A), fmult k f ≤ f.

Lemma fle_zero : ∀ (A:Type) (f : MF A), fzero A ≤ f.

Lemma fle_one : ∀ (A:Type) (f : MF A), f ≤ fone A.

Lemma feq_finv_finv : ∀ (A:Type) (f : MF A), finv (finv f) ≈ f.

Lemma fle_fesp_left : ∀ (A:Type) (f g : MF A), fesp f g ≤ f.

Lemma fle_fesp_right : ∀ (A:Type) (f g : MF A), fesp f g ≤ g.

Lemma fle_fconj_left : ∀ (A:Type) (f g : MF A), fconj f g ≤ f.

Lemma fle_fconj_right : ∀ (A:Type) (f g : MF A), fconj f g ≤ g.

Lemma fconj_decomp : ∀ A (f g : MF A),
f ≈ fplus (fconj f g) (fconj f (finv g)).
Hint Resolve fconj_decomp.

Compatibility of addition of two functions

Definition fplusok (A:Type) (f g : MF A) := f ≤ finv g.
Hint Unfold fplusok.

Lemma fplusok_sym : ∀ (A:Type) (f g : MF A) , fplusok f g → fplusok g f.
Hint Immediate fplusok_sym.

Lemma fplusok_inv : ∀ (A:Type) (f : MF A) , fplusok f (finv f).
Hint Resolve fplusok_inv.

Lemma fplusok_le_compat : ∀ (A:Type)(f1 f2 g1 g2:MF A),
      fplusok f2 g2 → f1 ≤ f2 → g1 ≤ g2 → fplusok f1 g1.

Hint Resolve fle_fplus_left fle_fplus_right fle_zero fle_one feq_finv_finv finv_le_compat
fle_fmult fle_fesp_left fle_fesp_right fle_fconj_left fle_fconj_right.

Lemma fconj_fplusok : ∀ (A:Type)(f g h:MF A),
            fplusok g h → fplusok (fconj f g) (fconj f h).
Hint Resolve fconj_fplusok.

Definition Fconj A : MF A -m > MF A -m > MF A := mon2 (fconj (A:=A)).

Lemma Fconj_simpl : ∀ A f g, Fconj A f g = fconj f g.

Lemma fconj_sym : ∀ A (f g : MF A), fconj f g ≈ fconj g f.
Hint Resolve fconj_sym.

Lemma Fconj_sym : ∀ A (f g : MF A), Fconj A f g ≈ Fconj A g f.
Hint Resolve Fconj_sym.

Lemma lub_MF_simpl : ∀ A (h : nat -m > MF A) (x:A), lub h x = lub (h <o > x).

Instance fconj_continuous2 A : continuous2 (Fconj A).
Save.

Definition Fmult A : U -m > MF A -m > MF A := mon2 (fmult (A:=A)).

Lemma Fmult_simpl : ∀ A k f, Fmult A k f = fmult k f.

Lemma fmult_continuous2 : ∀ A, continuous2 (Fmult A).

Lemma Umult_sym_cst:
  ∀ A : Type,
  ∀ (k : U) (f : MF A), (fun x : A ⇒ f x * k) ≈ (fun x : A ⇒ k * f x).

Fixpoints of functions of type A → U

Section FixDef.
Variable A :Type.

Variable F : MF A -m > MF A.

Definition mufix : MF A := fixp F.

Definition G : MF A --m → MF A := Imon F.

Definition nufix : MF A := fixp (c:=MFopp A) G.

Lemma mufix_inv : ∀ f : MF A, F f ≤ f → mufix ≤ f.
Hint Resolve mufix_inv.

Lemma nufix_inv : ∀ f :MF A, f ≤ F f → f ≤ nufix.
Hint Resolve nufix_inv.

Lemma mufix_le : mufix ≤ F mufix.
Hint Resolve mufix_le.

Lemma nufix_sup : F nufix ≤ nufix.
Hint Resolve nufix_sup.

Lemma mufix_eq : continuous F → mufix ≈ F mufix.
Hint Resolve mufix_eq.

Lemma nufix_eq : continuous (c1:=MFopp A) (c2:=MFopp A) G → nufix ≈ F nufix.
Hint Resolve nufix_eq.

End FixDef.
Hint Resolve mufix_le mufix_eq nufix_sup nufix_eq.

Definition Fcte (A:Type) (f:MF A) : MF A -m > MF A := mon (cte (MF A) f).

Lemma mufix_cte : ∀ (A:Type) (f:MF A), mufix (Fcte f) ≈ f.

Lemma nufix_cte : ∀ (A:Type) (f:MF A), nufix (Fcte f) ≈ f.

Hint Resolve mufix_cte nufix_cte.

Properties of (pseudo-)barycenter of two points

Lemma Uinv_bary :
   ∀ a b x y : U, a ≤ [1-]b →
      [1-] (a * x + b * y) ≈ a * [1-] x + b * [1-] y + [1-] (a + b).
Hint Resolve Uinv_bary.

Lemma Uinv_bary_le :
   ∀ a b x y : U, a ≤ [1-]b → a * [1-] x + b * [1-] y ≤ [1-] (a * x + b * y).
Hint Resolve Uinv_bary_le.

Lemma Uinv_bary_eq : ∀ a b x y : U, a ≈ [1-]b →
      [1-] (a * x + b * y) ≈ a * [1-] x + b * [1-] y.
Hint Resolve Uinv_bary_eq.

Lemma bary_refl_eq : ∀ a b x, a ≈ [1-]b → a * x + b * x ≈ x.
Hint Resolve bary_refl_eq.

Lemma bary_refl_feq : ∀ A a b (f:A → U) ,
      a ≈ [1-]b → (fun x ⇒ a * f x + b * f x) ≈ f.
Hint Resolve bary_refl_feq.

Lemma bary_le_left : ∀ a b x y, [1-]b ≤ a → x ≤ y → x ≤ a * x + b * y.

Lemma bary_le_right : ∀ a b x y, a ≤ [1-]b → x ≤ y → a * x + b * y ≤ y.

Hint Resolve bary_le_left bary_le_right.

Lemma bary_up_eq : ∀ a b x y : U, a ≈ [1-]b → x ≤ y → a * x + b * y ≈ x + b * (y - x).

Lemma bary_up_le : ∀ a b x y : U, a ≤ [1-]b → a * x + b * y ≤ x + b * (y - x).

Lemma bary_anti_mon : ∀ a b a' b' x y : U,
  a ≈ [1-]b → a' ≈ [1-]b' → a ≤ a' → x ≤ y → a' * x + b' * y ≤ a * x + b * y.
Hint Resolve bary_anti_mon.

Lemma bary_Uminus_left :
   ∀ a b x y : U, a ≤ [1-]b → (a * x + b * y) - x ≤ b * (y - x).

Lemma bary_Uminus_left_eq :
    ∀ a b x y : U, a ≈ [1-]b → x ≤ y → (a * x + b * y) - x ≈ b * (y - x).

Lemma Uminus_bary_left
   : ∀ a b x y : U, [1-]a ≤ b → x - (a * x + b * y) ≤ b * (x - y).

Lemma Uminus_bary_left_eq
   : ∀ a b x y : U, a ≈ [1-]b → y ≤ x → x - (a * x + b * y) ≈ b * (x - y).

Hint Resolve bary_up_eq bary_up_le bary_Uminus_left Uminus_bary_left bary_Uminus_left_eq Uminus_bary_left_eq.

Lemma bary_le_simpl_right
     : ∀ a b x y : U, a ≈ [1-]b → ¬ 0 ≈ a → a * x + b * y ≤ y → x ≤ y.

Lemma bary_le_simpl_left
     : ∀ a b x y : U, a ≈ [1-]b → ¬ 0 ≈ b → x ≤ a * x + b * y → x ≤ y.

Lemma diff_bary_left_eq
   : ∀ a b x y : U, a ≈ [1-]b → diff x (a * x + b * y) ≈ b * diff x y.
Hint Resolve diff_bary_left_eq.

Lemma Uinv_half_bary :
   ∀ x y : U, [1-] (½ * x + ½ * y) ≈ ½ * [1-] x + ½ * [1-] y.
Hint Resolve Uinv_half_bary.

Properties of generalized sums sigma

Lemma sigma_plus : ∀ (f g : nat → U) (n:nat),
   sigma (fun k ⇒ (f k) + (g k)) n ≈ sigma f n + sigma g n.

Definition retract (f : nat → U) (n : nat) := ∀ k, (k < n)%nat → f k ≤ [1-] (sigma f k).

Lemma retract0 : ∀ (f : nat → U), retract f 0.

Lemma retract_pred : ∀ (f : nat → U) (n : nat), retract f (S n) → retract f n.

Lemma retractS: ∀ (f : nat → U) (n : nat), retract f (S n) → f n ≤ [1-] (sigma f n).

Hint Immediate retract_pred retractS.

Lemma retractS_inv :
     ∀ (f : nat → U) (n : nat), retract f (S n) → sigma f n ≤ [1-] f n.
Hint Immediate retractS_inv.

Lemma retractS_intro: ∀ (f : nat → U) (n : nat),
   retract f n → f n ≤ [1-] (sigma f n) → retract f (S n).

Hint Resolve retract0 retractS_intro.

Lemma retract_lt : ∀ (f : nat → U) (n : nat), sigma f n < 1 → retract f n.

Lemma retract_unif :
    ∀ (f : nat → U) (n : nat),
             (∀ k, (k ≤ n)%nat → f k ≤ [1/]1+n) → retract f (S n).

Hint Resolve retract_unif.

Lemma sigma_mult :
  ∀ (f : nat → U) n c, retract f n → sigma (fun k ⇒ c * (f k)) n ≈ c * (sigma f n).
Hint Resolve sigma_mult.

Lemma sigma_prod_maj : ∀ (f g : nat → U) n,
   sigma (fun k ⇒ (f k) * (g k)) n ≤ sigma f n.

Hint Resolve sigma_prod_maj.

Lemma sigma_prod_le : ∀ (f g : nat → U) (c:U), (∀ k, (f k) ≤ c)
   → ∀ n, retract g n → sigma (fun k ⇒ (f k) * (g k)) n ≤ c * (sigma g n).

Lemma sigma_prod_ge : ∀ (f g : nat → U) (c:U), (∀ k, c ≤ (f k))
   → ∀ n, (retract g n) → c * (sigma g n) ≤ (sigma (fun k ⇒ (f k) * (g k)) n).

Hint Resolve sigma_prod_maj sigma_prod_le sigma_prod_ge.

Lemma sigma_inv : ∀ (f g : nat → U) (n:nat), (retract f n) →
  [1-] (sigma (fun k ⇒ f k * g k) n) ≈ (sigma (fun k ⇒ f k * [1-] (g k)) n) + [1-] (sigma f n).

Product by an integer

Definition of Nmult n x written n */ x

Fixpoint Nmult (n: nat) (x : U) {struct n} : U :=
match n with O ⇒ 0 | (S O) ⇒ x | S p ⇒ x + (Nmult p x) end.

Condition for n */ x to be exact : n = 0 or x ≤ 1/n

Definition Nmult_def (n: nat) (x : U) :=
match n with O ⇒ True | S p ⇒ x ≤ [1/]1+p end.

Lemma Nmult_def_O : ∀ x, Nmult_def O x.
Hint Resolve Nmult_def_O.

Lemma Nmult_def_1 : ∀ x, Nmult_def (S O) x.
Hint Resolve Nmult_def_1.

Lemma Nmult_def_intro : ∀ n x , x ≤ [1/]1+n → Nmult_def (S n) x.
Hint Resolve Nmult_def_intro.

Lemma Nmult_def_Unth: ∀ n , Nmult_def (S n) ([1/]1+n).
Hint Resolve Nmult_def_Unth.

Lemma Nmult_def_pred : ∀ n x, Nmult_def (S n) x → Nmult_def n x.

Hint Immediate Nmult_def_pred.

Lemma Nmult_defS : ∀ n x, Nmult_def (S n) x → x ≤ [1/]1+n.
Hint Immediate Nmult_defS.

Lemma Nmult_def_class : ∀ n p, class (Nmult_def n p).
Hint Resolve Nmult_def_class.

Infix "*/" := Nmult (at level 60) : U_scope.

Add Morphism Nmult_def with signature eq ⇾ Oeq ⇾ iff as Nmult_def_eq_compat.
Save.

Lemma Nmult_def_zero : ∀ n, Nmult_def n 0.
Hint Resolve Nmult_def_zero.

Properties of n */ x

Lemma Nmult_0 : ∀ (x:U), O */x = 0.

Lemma Nmult_1 : ∀ (x:U), (S O )*/x = x.

Lemma Nmult_zero : ∀ n, n */ 0 ≈ 0.

Lemma Nmult_SS : ∀ (n:nat) (x:U), S (S n) */x = x + (S n */ x).

Lemma Nmult_2 : ∀ (x:U), 2*/x = x + x.

Lemma Nmult_S : ∀ (n:nat) (x:U), S n */ x ≈ x + (n*/x).

Hint Resolve Nmult_1 Nmult_SS Nmult_2 Nmult_S.

Add Morphism Nmult with signature eq ⇾ Oeq ⇾ Oeq as Nmult_eq_compat.
Save.
Hint Immediate Nmult_eq_compat.

Lemma Nmult_eq_compat_left : ∀ (n:nat) (x y:U), x ≈ y → n */ x ≈ n */ y.

Lemma Nmult_eq_compat_right : ∀ (n m:nat) (x:U), (n = m)%nat → n */ x ≈ m */ x.
Hint Resolve Nmult_eq_compat_right.

Lemma Nmult_le_compat_right : ∀ n x y, x ≤ y → n */ x ≤ n */ y.

Lemma Nmult_le_compat_left : ∀ n m x, (n ≤ m)%nat → n */ x ≤ m */ x.

Hint Resolve Nmult_eq_compat_right Nmult_le_compat_right Nmult_le_compat_left.

Lemma Nmult_le_compat : ∀ (n m:nat) x y, n ≤ m → x ≤ y → n */ x ≤ m */ y.
Hint Immediate Nmult_le_compat.

Instance Nmult_mon2 : monotonic2 Nmult.
Save.

Definition NMult : nat -m > U -m > U :=mon2 Nmult.

Lemma Nmult_sigma : ∀ (n:nat) (x:U), n */ x ≈ sigma (fun k ⇒ x) n.

Hint Resolve Nmult_sigma.

Lemma Nmult_Unth_prop : ∀ n:nat, [1/]1+n ≈ [1-] (n*/ ([1/]1+n)).
Hint Resolve Nmult_Unth_prop.

Lemma Nmult_n_Unth: ∀ n:nat, n */ [1/]1+n ≈ [1-] ([1/]1+n).

Lemma Nmult_Sn_Unth: ∀ n:nat, S n */ [1/]1+n ≈ 1.

Hint Resolve Nmult_n_Unth Nmult_Sn_Unth.

Lemma Nmult_ge_Sn_Unth: ∀ n k, (S n ≤ k)%nat → k */ [1/]1+n ≈ 1.

Lemma Nmult_le_n_Unth: ∀ n k, (k ≤ n)%nat → k */ [1/]1+n ≤ [1-] ([1/]1+n).

Hint Resolve Nmult_ge_Sn_Unth Nmult_le_n_Unth.

Lemma Nmult_Umult_assoc_left : ∀ n x y, Nmult_def n x → n*/(x*y) ≈ (n*/x)*y.

Hint Resolve Nmult_Umult_assoc_left.

Lemma Nmult_Umult_assoc_right : ∀ n x y, Nmult_def n y → n*/(x*y) ≈ x*(n*/y).

Hint Resolve Nmult_Umult_assoc_right.

Lemma plus_Nmult_distr : ∀ n m x, (n + m) */ x ≈ (n */ x) + (m */ x).

Lemma Nmult_Uplus_distr : ∀ n x y, n */ (x + y) ≈ (n */ x) + (n */ y).

Lemma Nmult_mult_assoc : ∀ n m x, (n * m) */ x ≈ n */ (m */ x).

Lemma Nmult_Unth_simpl_left : ∀ n x, (S n) */ ([1/]1+n * x) ≈ x.

Lemma Nmult_Unth_simpl_right : ∀ n x, (S n) */ (x * [1/]1+n) ≈ x.

Hint Resolve Nmult_Umult_assoc_right plus_Nmult_distr Nmult_Uplus_distr
Nmult_mult_assoc Nmult_Unth_simpl_left Nmult_Unth_simpl_right.

Lemma Uinv_Nmult : ∀ k n, [1-] (k */ [1/]1+n) ≈ ((S n) - k) */ [1/]1+n.

Lemma Nmult_neq_zero : ∀ n x, ¬0 ≈ x → ¬0 ≈ S n */ x.
Hint Resolve Nmult_neq_zero.

Lemma Nmult_le_simpl : ∀ (n:nat) (x y:U),
   Nmult_def (S n) x → Nmult_def (S n) y → (S n */ x) ≤ (S n */ y) → x ≤ y.

Lemma Nmult_Unth_le : ∀ (n1 n2 m1 m2:nat),
   (n2 * S n1 ≤ m2 * S m1)%nat → n2 */ [1/]1+m1 ≤ m2 */ [1/]1+n1.

Lemma Nmult_Unth_eq :
   ∀ (n1 n2 m1 m2:nat),
   (n2 * S n1= m2 * S m1)%nat → n2 */ [1/]1+m1 ≈ m2 */ [1/]1+n1.

Hint Resolve Nmult_Unth_le Nmult_Unth_eq.

Lemma Nmult_Unth_factor :
   ∀ (n m1 m2:nat),
   (n * S m2= S m1)%nat → n */ [1/]1+m1 ≈ [1/]1+m2.
Hint Resolve Nmult_Unth_factor.

Lemma Nmult_def_lt : ∀ n x, n */ x <1 → Nmult_def n x.

Hint Immediate Nmult_def_lt.

Conversion from booleans to U

Definition B2U :MF bool := fun (b:bool) ⇒ if b then 1 else 0.

Definition NB2U :MF bool := fun (b:bool) ⇒ if b then 0 else 1.

Lemma B2Uinv : NB2U ≈ finv B2U.

Lemma NB2Uinv : B2U ≈ finv NB2U.

Hint Resolve B2Uinv NB2Uinv.

Particular sequences

pmin p n = p - ½ ^ n

Definition pmin (p:U) (n:nat) := p - ( ½ ^ n ).

Add Morphism pmin with signature Oeq ⇾ eq ⇾ Oeq as pmin_eq_compat.
Save.

Properties of pmin

Lemma pmin_esp_S : ∀ p n, pmin (p & p) n ≈ pmin p (S n) & pmin p (S n).

Lemma pmin_esp_le : ∀ p n, pmin p (S n) ≤ ½ * (pmin (p & p) n) + ½.

Lemma pmin_plus_eq : ∀ p n, p ≤ ½ → pmin p (S n) ≈ ½ * (pmin (p + p) n).

Lemma pmin_0 : ∀ p:U, pmin p O ≈ 0.

Lemma pmin_le : ∀ (p:U) (n:nat), p - ([1/]1+n) ≤ pmin p n.

Hint Resolve pmin_0 pmin_le.

Lemma pmin_le_compat : ∀ p (n m : nat), n ≤ m → pmin p n ≤ pmin p m.
Hint Resolve pmin_le_compat.

Instance pmin_mon : ∀ p, monotonic (pmin p).
Save.

Definition Pmin (p:U) :nat -m > U := mon (pmin p).

Lemma le_p_lim_pmin : ∀ p, p ≤ lub (Pmin p).

Lemma le_lim_pmin_p : ∀ p, lub (Pmin p) ≤ p.
Hint Resolve le_p_lim_pmin le_lim_pmin_p.

Lemma eq_lim_pmin_p : ∀ p, lub (Pmin p) ≈ p.

Hint Resolve eq_lim_pmin_p.

Particular case where p = 1

Definition U1min := Pmin 1.

Lemma eq_lim_U1min : lub U1min ≈ 1.

Lemma U1min_S : ∀ n, U1min (S n) ≈ ½ *(U1min n) + ½.

Lemma U1min_0 : U1min O ≈ 0.

Hint Resolve eq_lim_U1min U1min_S U1min_0.

Lemma glb_half_exp : glb (UExp ½) ≈ 0.
Hint Resolve glb_half_exp.

Lemma Ule_lt_half_exp : ∀ x y, (∀ p, x ≤ y + ½ ^p) → x ≤ y.

Lemma half_exp_le_half : ∀ p, ½ ^(S p) ≤ ½.
Hint Resolve half_exp_le_half.

Lemma twice_half_exp : ∀ p, ½ ^(S p) + ½ ^(S p) ≈ ½ ^p.
Hint Resolve twice_half_exp.

Dyadic numbers

Fixpoint exp2 (n:nat) : nat :=
match n with O ⇒ (1%nat) | S p ⇒ (2 * (exp2 p))%nat end.

Lemma exp2_pos : ∀ n, (O < exp2 n)%nat.
Hint Resolve exp2_pos.

Lemma S_pred_exp2 : ∀ n, S (pred (exp2 n))=exp2 n.
Hint Resolve S_pred_exp2.

Notation "k /2^ p" := (k */ (½ )^p) (at level 35, no associativity).

Lemma Unth_eq : ∀ n p, n*/ p ≈ [1-]p → p ≈ [1/]1+n.

Lemma Unth_half : ∀ n, (O <n)%nat → [1/]1+(pred (n+n)) ≈ ½ * [1/]1+pred n.

Lemma Unth_exp2 : ∀ p, ½ ^p ≈ [1/]1+pred (exp2 p).

Hint Resolve Unth_exp2.

Lemma Nmult_exp2 : ∀ p, (exp2 p)/2^p ≈ 1.
Hint Resolve Nmult_exp2.

Section Sequence.
Variable k : U.
Hypothesis kless1 : k < 1.

Lemma Ult_one_inv_zero : ¬ 0 ≈ [1-]k.
Hint Resolve Ult_one_inv_zero.

Lemma Umult_simpl_zero : ∀ x, x ≤ k * x → x ≈ 0.

Lemma Umult_simpl_one : ∀ x, k * x + [1-]k ≤ x → x ≈ 1.

Lemma bary_le_compat : ∀ k' x y, x ≤ y → k ≤ k' → k' * x + [1-]k' * y ≤ k * x + [1-]k * y.

Lemma bary_one_le_compat : ∀ k' x, k ≤ k' → k' * x + [1-]k' ≤ k * x + [1-]k.

Lemma glb_exp_0 : glb (UExp k) ≈ 0.

Instance Uinvexp_mon : monotonic (fun n ⇒ [1-]k ^ n).
Save.

Lemma lub_inv_exp_1 : mlub (fun n ⇒ [1-]k ^ n) ≈ 1.

End Sequence.
Hint Resolve glb_exp_0 lub_inv_exp_1 bary_one_le_compat bary_le_compat.

Tactic for simplification of goals

Ltac Usimpl := match goal with
    |- context [(Uplus 0 ?x)] ⇒ setoid_rewrite (Uplus_zero_left x)
| |- context [(Uplus ?x 0)] ⇒ setoid_rewrite (Uplus_zero_right x)
| |- context [(Uplus 1 ?x)] ⇒ setoid_rewrite (Uplus_one_left x)
| |- context [(Uplus ?x 1)] ⇒ setoid_rewrite (Uplus_one_right x)
| |- context [(Umult 0 ?x)] ⇒ setoid_rewrite (Umult_zero_left x)
| |- context [(Umult ?x 0)] ⇒ setoid_rewrite (Umult_zero_right x)
| |- context [(Umult 1 ?x)] ⇒ setoid_rewrite (Umult_one_left x)
| |- context [(Umult ?x 1)] ⇒ setoid_rewrite (Umult_one_right x)
| |- context [(Uesp 0 ?x)] ⇒ setoid_rewrite (Uesp_zero_left x)
| |- context [(Uesp ?x 0)] ⇒ setoid_rewrite (Uesp_zero_right x)
| |- context [(Uesp 1 ?x)] ⇒ setoid_rewrite (Uesp_one_left x)
| |- context [(Uesp ?x 1)] ⇒ setoid_rewrite (Uesp_one_right x)
| |- context [(Uminus 0 ?x)] ⇒ setoid_rewrite (Uminus_zero_left x)
| |- context [(Uminus ?x 0)] ⇒ setoid_rewrite (Uminus_zero_right x)
| |- context [(Uminus ?x 1)] ⇒ setoid_rewrite (Uminus_one_right x)
| |- context [([1-] ([1-] ?x))] ⇒ setoid_rewrite (Uinv_inv x)
| |- context [ ?x + ([1-] ?x)] ⇒ setoid_rewrite (Uinv_opp_right x)
| |- context [ ([1-]?x) + ?x ] ⇒ setoid_rewrite (Uinv_opp_left x)
| |- context [([1-] 1)] ⇒ setoid_rewrite Uinv_one
| |- context [([1-] 0)] ⇒ setoid_rewrite Uinv_zero
| |- context [([1/]1+O)] ⇒ setoid_rewrite Unth_zero
| |- context [?x^O] ⇒ setoid_rewrite (Uexp_0 x)
| |- context [?x^(S O )] ⇒ setoid_rewrite (Uexp_1 x)
| |- context [0^(?n)] ⇒ setoid_rewrite Uexp_zero; [idtac|omega]
| |- context [U1 ^(?n)] ⇒ setoid_rewrite Uexp_one
| |- context [(Nmult 0 ?x)] ⇒ setoid_rewrite (Nmult_0 x)
| |- context [(Nmult 1 ?x)] ⇒ setoid_rewrite (Nmult_1 x)
| |- context [(Nmult ?n 0)] ⇒ setoid_rewrite (Nmult_zero n)
| |- context [(sigma ?f O)] ⇒ setoid_rewrite (sigma_0 f)
| |- context [(sigma ?f (S O))] ⇒ setoid_rewrite (sigma_1 f)
| |- (Ole (Uplus ?x ?y) (Uplus ?x ?z)) ⇒ apply Uplus_le_compat_right
| |- (Ole (Uplus ?x ?z) (Uplus ?y ?z)) ⇒ apply Uplus_le_compat_left
| |- (Ole (Uplus ?x ?z) (Uplus ?z ?y)) ⇒ setoid_rewrite (Uplus_sym z y);
                                              apply Uplus_le_compat_left
| |- (Ole (Uplus ?x ?y) (Uplus ?z ?x)) ⇒ setoid_rewrite (Uplus_sym x y);
                                              apply Uplus_le_compat_left
| |- (Ole (Uinv ?y) (Uinv ?x)) ⇒ apply Uinv_le_compat
| |- (Ole (Uminus ?x ?y) (Uplus ?x ?z)) ⇒ apply Uminus_le_compat_right
| |- (Ole (Uminus ?x ?z) (Uplus ?y ?z)) ⇒ apply Uminus_le_compat_left
| |- ((Uinv ?x) ≈ (Uinv ?y)) ⇒ apply Uinv_eq_compat
| |- ((Uplus ?x ?y) ≈ (Uplus ?x ?z)) ⇒ apply Uplus_eq_compat_right
| |- ((Uplus ?x ?z) ≈ (Uplus ?y ?z)) ⇒ apply Uplus_eq_compat_left
| |- ((Uplus ?x ?z) ≈ (Uplus ?z ?y)) ⇒ setoid_rewrite (Uplus_sym z y);
                                             apply Uplus_eq_compat_left
| |- ((Uplus ?x ?y) ≈ (Uplus ?z ?x)) ⇒ setoid_rewrite (Uplus_sym x y);
                                             apply Uplus_eq_compat_left
| |- ((Uminus ?x ?y) ≈ (Uplus ?x ?z)) ⇒ apply Uminus_eq_compat;[apply Oeq_refl|idtac]
| |- ((Uminus ?x ?z) ≈ (Uplus ?y ?z)) ⇒ apply Uminus_eq_compat;[idtac|apply Oeq_refl]
| |- (Ole (Umult ?x ?y) (Umult ?x ?z)) ⇒ apply Umult_le_compat_right
| |- (Ole (Umult ?x ?z) (Umult ?y ?z)) ⇒ apply Umult_le_compat_left
| |- (Ole (Umult ?x ?z) (Umult ?z ?y)) ⇒ setoid_rewrite (Umult_sym z y);
                                             apply Umult_le_compat_left
| |- (Ole (Umult ?x ?y) (Umult ?z ?x)) ⇒ setoid_rewrite (Umult_sym x y);
                                             apply Umult_le_compat_left
| |- ((Umult ?x ?y) ≈ (Umult ?x ?z)) ⇒ apply Umult_eq_compat_right
| |- ((Umult ?x ?z) ≈ (Umult ?y ?z)) ⇒ apply Umult_eq_compat_left
| |- ((Umult ?x ?z) ≈ (Umult ?z ?y)) ⇒ setoid_rewrite (Umult_sym z y);
                                             apply Umult_eq_compat_left
| |- ((Umult ?x ?y) ≈ (Umult ?z ?x)) ⇒ setoid_rewrite (Umult_sym x y);
                                             apply Umult_eq_compat_left
end.

Ltac Ucompute :=
first [setoid_rewrite Uplus_zero_left |
        setoid_rewrite Uplus_zero_right |
        setoid_rewrite Uplus_one_left |
        setoid_rewrite Uplus_one_right |
        setoid_rewrite Umult_zero_left |
        setoid_rewrite Umult_zero_right |
        setoid_rewrite Umult_one_left |
        setoid_rewrite Umult_one_right |
        setoid_rewrite Uesp_zero_left |
        setoid_rewrite Uesp_zero_right |
        setoid_rewrite Uesp_one_left |
        setoid_rewrite Uesp_one_right |
        setoid_rewrite Uminus_zero_left |
        setoid_rewrite Uminus_zero_right |
        setoid_rewrite Uminus_one_right |
        setoid_rewrite Uinv_inv |
        setoid_rewrite Uinv_opp_right |
        setoid_rewrite Uinv_opp_left |
        setoid_rewrite Uinv_one |
        setoid_rewrite Uinv_zero |
        setoid_rewrite Unth_zero |
        setoid_rewrite Uexp_0 |
        setoid_rewrite Uexp_1 |
        (setoid_rewrite Uexp_zero; [idtac|omega]) |
        setoid_rewrite Uexp_one |
        setoid_rewrite Nmult_0 |
        setoid_rewrite Nmult_1 |
        setoid_rewrite Nmult_zero |
        setoid_rewrite sigma_0 |
        setoid_rewrite sigma_1
].

Properties of current values

Notation "[1/3]" := (Unth 2%nat).
Notation "¼" := (Unth 3%nat).
Notation "[1/8]" := (Unth 7).
Notation "¾" := (Uinv ¼).

Lemma half_square : ½ *½ ≈ ¼.

Lemma half_cube : ½ *½ *½ ≈ [1/8].

Lemma three_quarter_decomp : ¾ ≈ ½ +¼.

Equality is not true, even for monotonic sequences fot instance n/m

Lemma Ulub_Uglb_exch_le : ∀ f : nat → nat → U,
Ulub (fun n ⇒ Uglb (fun m ⇒ f n m)) ≤ Uglb (fun m ⇒ Ulub (fun n ⇒ f n m)).

Intervals

Definition

Record IU : Type := mk_IU {low:U; up:U; proper:low ≤ up}.

Hint Resolve proper.

the all set : [0,1]

Definition full := mk_IU 0 1 (Upos 1).

singleton : [x]

Definition singl (x:U) := mk_IU x x (Ole_refl x).

down segment : [0,x]

Definition inf (x:U) := mk_IU 0 x (Upos x).

up segment : [x,1]

Definition sup (x:U) := mk_IU x 1 (Unit x).

Relations

Definition Iin (x:U) (I:IU) := low I ≤ x ∧ x ≤ up I.

Definition Iincl I J := low J ≤ low I ∧ up I ≤ up J.

Definition Ieq I J := low I ≈ low J ∧ up I ≈ up J.
Hint Unfold Iin Iincl Ieq.

Properties

Lemma Iin_low : ∀ I, Iin (low I) I.

Lemma Iin_up : ∀ I, Iin (up I) I.

Hint Resolve Iin_low Iin_up.

Lemma Iin_singl_elim : ∀ x y, Iin x (singl y) → x ≈ y.

Lemma Iin_inf_elim : ∀ x y, Iin x (inf y) → x ≤ y.

Lemma Iin_sup_elim : ∀ x y, Iin x (sup y) → y ≤ x.

Lemma Iin_singl_intro : ∀ x y, x ≈ y → Iin x (singl y).

Lemma Iin_inf_intro : ∀ x y, x ≤ y → Iin x (inf y).

Lemma Iin_sup_intro : ∀ x y, y ≤ x → Iin x (sup y).

Hint Immediate Iin_inf_elim Iin_sup_elim Iin_singl_elim.
Hint Resolve Iin_inf_intro Iin_sup_intro Iin_singl_intro.

Lemma Iin_class : ∀ I x, class (Iin x I).

Lemma Iincl_class : ∀ I J, class (Iincl I J).

Lemma Ieq_class : ∀ I J, class (Ieq I J).
Hint Resolve Iin_class Iincl_class Ieq_class.

Lemma Iincl_in : ∀ I J, Iincl I J → ∀ x, Iin x I → Iin x J.

Lemma Iincl_low : ∀ I J, Iincl I J → low J ≤ low I.

Lemma Iincl_up : ∀ I J, Iincl I J → up I ≤ up J.

Hint Immediate Iincl_low Iincl_up.

Lemma Iincl_refl : ∀ I, Iincl I I.
Hint Resolve Iincl_refl.

Lemma Iincl_trans : ∀ I J K, Iincl I J → Iincl J K → Iincl I K.

Instance IUord : ord IU := {Oeq := fun I J ⇒ Ieq I J; Ole := fun I J ⇒ Iincl J I}.
Defined.

Lemma low_le_compat : ∀ I J:IU, I ≤ J → low I ≤ low J.

Lemma up_le_compat : ∀ I J : IU, I ≤ J → up J ≤ up I.

Instance low_mon : monotonic low.
Save.

Definition Low : IU -m > U := mon low.

Instance up_mon : monotonic (o2:=Iord U) up.
Save.

Definition Up : IU -m → U := mon (o2:=Iord U) up.

Lemma Ieq_incl : ∀ I J, Ieq I J → Iincl I J.

Lemma Ieq_incl_sym : ∀ I J, Ieq I J → Iincl J I.
Hint Immediate Ieq_incl Ieq_incl_sym.

Lemma lincl_eq_compat : ∀ I J K L,
     Ieq I J → Iincl J K → Ieq K L → Iincl I L.

Lemma lincl_eq_trans : ∀ I J K,
     Iincl I J → Ieq J K → Iincl I K.

Lemma Ieq_incl_trans : ∀ I J K,
     Ieq I J → Iincl J K → Iincl I K.

Lemma Iincl_antisym : ∀ I J, Iincl I J → Iincl J I → Ieq I J.
Hint Immediate Iincl_antisym.

Lemma Ieq_refl : ∀ I, Ieq I I.
Hint Resolve Ieq_refl.

Lemma Ieq_sym : ∀ I J, Ieq I J → Ieq J I.
Hint Immediate Ieq_sym.

Lemma Ieq_trans : ∀ I J K, Ieq I J → Ieq J K → Ieq I K.

Lemma Isingl_eq : ∀ x y, Iincl (singl x) (singl y) → x ≈ y.
Hint Immediate Isingl_eq.

Lemma Iincl_full : ∀ I, Iincl I full.
Hint Resolve Iincl_full.

Operations on intervals

Definition Iplus I J := mk_IU (low I + low J) (up I + up J)
                                           (Uplus_le_compat _ _ _ _ (proper I) (proper J)).

Lemma low_Iplus : ∀ I J, low (Iplus I J)=low I + low J.

Lemma up_Iplus : ∀ I J, up (Iplus I J)=up I + up J.

Lemma Iplus_in : ∀ I J x y, Iin x I → Iin y J → Iin (x+y) (Iplus I J).

Lemma lplus_in_elim :
∀ I J z, low I ≤ [1-]up J → Iin z (Iplus I J)
                → exc (fun x ⇒ Iin x I ∧
                                                   exc (fun y ⇒ Iin y J ∧ z ≈ x+y)).

Definition Imult I J := mk_IU (low I * low J) (up I * up J)
                                            (Umult_le_compat _ _ _ _ (proper I) (proper J)).

Lemma low_Imult : ∀ I J, low (Imult I J) = low I * low J.

Lemma up_Imult : ∀ I J, up (Imult I J) = up I * up J.

Definition Imultk p I := mk_IU (p * low I) (p * up I) (Umult_le_compat_right p _ _ (proper I)).

Lemma low_Imultk : ∀ p I, low (Imultk p I) = p * low I.

Lemma up_Imultk : ∀ p I, up (Imultk p I) = p * up I.

Lemma Imult_in : ∀ I J x y, Iin x I → Iin y J → Iin (x*y) (Imult I J).

Lemma Imultk_in : ∀ p I x , Iin x I → Iin (p*x) (Imultk p I).

Limits of intervals

Definition Ilim : ∀ I: nat -m > IU, IU.
Defined.

Lemma low_lim : ∀ (I:nat -m > IU), low (Ilim I) = lub (Low @ I).

Lemma up_lim : ∀ (I:nat -m > IU), up (Ilim I) = glb (Up @ I).

Lemma lim_Iincl : ∀ (I:nat -m > IU) n, Iincl (Ilim I) (I n).
Hint Resolve lim_Iincl.

Lemma Iincl_lim : ∀ J (I:nat -m >IU), (∀ n, Iincl J (I n)) → Iincl J (Ilim I).

Lemma IIim_incl_stable : ∀ (I J:nat -m > IU), (∀ n, Iincl (I n) (J n)) → Iincl (Ilim I) (Ilim J).
Hint Resolve IIim_incl_stable.

Instance IUcpo : cpo IU := {D0:=full; lub:=Ilim}.
Defined.

Limits inf and sup

Definition fsup (f:nat→U) (n:nat) := Ulub (fun k ⇒ f (n+k)%nat).

Definition finf (f:nat→U) (n:nat) := Uglb (fun k ⇒ f (n+k)%nat).

Lemma fsup_incr : ∀ (f:nat→U) n, fsup f (S n) ≤ fsup f n.
Hint Resolve fsup_incr.

Lemma finf_incr : ∀ (f:nat→U) n, finf f n ≤ finf f (S n).

Hint Resolve finf_incr.

Instance fsup_mon : ∀ f, monotonic (o2:=Iord U) (fsup f).
Save.

Instance finf_mon : ∀ f, monotonic (finf f).
Save.

Definition Fsup (f:nat→U) : nat -m → U := mon (fsup f).
Definition Finf (f:nat→U) : nat -m > U := mon (finf f).

Lemma fn_fsup : ∀ f n, f n ≤ fsup f n.
Hint Resolve fn_fsup.

Lemma finf_fn : ∀ f n, finf f n ≤ f n.
Hint Resolve finf_fn.

Definition limsup f := glb (Fsup f).
Definition liminf f := lub (Finf f).

Lemma le_liminf_sup : ∀ f, liminf f ≤ limsup f.

Hint Resolve le_liminf_sup.

Definition has_lim f := limsup f ≤ liminf f.

Lemma eq_liminf_sup : ∀ f, has_lim f→ liminf f ≈ limsup f.

Definition cauchy f := ∀ (p:nat), exc (fun M:nat ⇒ ∀ n m,
          (M ≤ n)%nat → (M ≤ m)%nat → f n ≤ f m + ½ ^p).

Definition is_limit f (l:U) := ∀ (p:nat), exc (fun M:nat ⇒ ∀ n,
          (M ≤ n)%nat → f n ≤ l + ½ ^p ∧ l ≤ f n + ½ ^p).

Lemma cauchy_lim : ∀ f, cauchy f → is_limit f (limsup f).

Lemma has_limit_cauchy : ∀ f l, is_limit f l → cauchy f.

Lemma limit_le_unique : ∀ f l1 l2, is_limit f l1 → is_limit f l2 → l1 ≤ l2.

Lemma limit_unique : ∀ f l1 l2, is_limit f l1 → is_limit f l2 → l1 ≈ l2.
Hint Resolve limit_unique.

Lemma has_limit_compute : ∀ f l, is_limit f l → is_limit f (limsup f).

Lemma limsup_eq_mult : ∀ k (f : nat → U),
        limsup (fun n ⇒ k * f n) ≈ k * limsup f.

Lemma liminf_eq_mult : ∀ k (f : nat → U),
        liminf (fun n ⇒ k * f n) ≈ k * liminf f.

Lemma limsup_eq_plus_cte_right : ∀ k (f : nat → U),
                 limsup (fun n ⇒ (f n) + k) ≈ limsup f + k.

Lemma liminf_eq_plus_cte_right : ∀ k (f : nat → U),
                 liminf (fun n ⇒ (f n) + k) ≈ liminf f + k.

Lemma limsup_le_plus : ∀ (f g: nat → U),
                 limsup (fun x ⇒ f x + g x) ≤ limsup f + limsup g.

Lemma liminf_le_plus : ∀ (f g: nat → U),
                 liminf f + liminf g ≤ liminf (fun x ⇒ f x + g x).

Hint Resolve liminf_le_plus limsup_le_plus.

Lemma limsup_le_compat : ∀ f g : nat → U, f ≤ g → limsup f ≤ limsup g.

Lemma liminf_le_compat : ∀ f g : nat → U, f ≤ g → liminf f ≤ liminf g.

Hint Resolve limsup_le_compat liminf_le_compat.

Lemma limsup_eq_compat : ∀ f g : nat → U, f ≈ g → limsup f ≈ limsup g.

Lemma liminf_eq_compat : ∀ f g : nat → U, f ≈ g → liminf f ≈ liminf g.

Hint Resolve liminf_eq_compat limsup_eq_compat.

Lemma limsup_inv : ∀ f : nat → U, limsup (fun x ⇒ [1-]f x) ≈ [1-] liminf f.

Lemma liminf_inv : ∀ f : nat → U, liminf (fun x ⇒ [1-]f x) ≈ [1-] limsup f.

Hint Resolve limsup_inv liminf_inv.

Limits of arbitrary sequences

Lemma liminf_incr : ∀ f:nat -m > U, liminf f ≈ lub f.

Lemma limsup_incr : ∀ f:nat -m > U, limsup f ≈ lub f.

Lemma has_limit_incr : ∀ f:nat -m > U, has_lim f.

Lemma liminf_decr : ∀ f:nat -m → U, liminf f ≈ glb f.

Lemma limsup_decr : ∀ f:nat -m →U, limsup f ≈ glb f.

Lemma has_limit_decr : ∀ f:nat -m → U, has_lim f.

Lemma has_limit_sum : ∀ f g: nat → U, has_lim f → has_lim g → has_lim (fun x ⇒ f x + g x).

Lemma has_limit_inv : ∀ f : nat → U, has_lim f → has_lim (fun x ⇒ [1-]f x).

Lemma has_limit_cte : ∀ c, has_lim (fun n ⇒ c).

Definition and properties of series : infinite sums

Definition serie (f : nat → U) : U := lub (sigma f).

Lemma serie_le_compat : ∀ (f g: nat → U),
(∀ k, f k ≤ g k) → serie f ≤ serie g.

Lemma serie_eq_compat : ∀ (f g: nat → U),
(∀ k, f k ≈ g k) → serie f ≈ serie g.

Lemma serie_sigma_lift : ∀ (f :nat → U) (n:nat),
          serie f ≈ sigma f n + serie (fun k ⇒ f (n + k)%nat).

Lemma serie_S_lift : ∀ (f :nat → U),
          serie f ≈ f O + serie (fun k ⇒ f (S k)).

Lemma serie_zero : ∀ f, (∀ k, f k ≈ 0) → serie f ≈ 0.

Lemma serie_not_zero : ∀ f k, 0 < f k → 0 < serie f.

Lemma serie_zero_elim : ∀ f, serie f ≈ 0 → ∀ k, f k ≈ 0.

Hint Resolve serie_eq_compat serie_le_compat serie_zero.

Lemma serie_le : ∀ f k, f k ≤ serie f.

Lemma serie_minus_incr : ∀ f :nat -m > U, serie (fun k ⇒ f (S k) - f k) ≈ lub f - f O.

Lemma serie_minus_decr : ∀ f : nat -m → U,
         serie (fun k ⇒ f k - f (S k)) ≈ f O - glb f.

Lemma serie_plus : ∀ (f g : nat → U),
   serie (fun k ⇒ (f k) + (g k)) ≈ serie f + serie g.

Definition wretract (f : nat → U) := ∀ k, f k ≤ [1-] (sigma f k).

Lemma retract_wretract : ∀ f, (∀ n, retract f n) → wretract f.

Lemma wretract_retract : ∀ f, wretract f → ∀ n, retract f n.

Hint Resolve wretract_retract.

Lemma wretract_lt : ∀ (f : nat → U), (∀ (n : nat), sigma f n < 1) → wretract f.

Lemma retract_zero_wretract :
       ∀ f n, retract f n → (∀ k, (n ≤ k)%nat → f k ≈ 0) → wretract f.

Lemma wretract_le : ∀ f g : nat→U, f ≤ g → wretract g → wretract f.

Lemma serie_mult :
  ∀ (f : nat → U) c, wretract f → serie (fun k ⇒ c * f k) ≈ c * serie f.
Hint Resolve serie_mult.

Lemma serie_prod_maj : ∀ (f g : nat → U),
   serie (fun k ⇒ f k * g k) ≤ serie f.

Hint Resolve serie_prod_maj.

Lemma serie_prod_le : ∀ (f g : nat → U) (c:U), (∀ k, f k ≤ c)
   → wretract g → serie (fun k ⇒ f k * g k) ≤ c * serie g.

Lemma serie_prod_ge : ∀ (f g : nat → U) (c:U), (∀ k, c ≤ (f k))
   → wretract g → c * serie g ≤ serie (fun k ⇒ f k * g k).

Hint Resolve serie_prod_le serie_prod_ge.

Lemma serie_inv_le : ∀ (f g : nat → U), wretract f →
  serie (fun k ⇒ f k * [1-] (g k)) ≤ [1-] (serie (fun k ⇒ f k * g k)).

Definition Serie : (nat → U ) -m > U.
Defined.

Lemma Serie_simpl : ∀ f, Serie f = serie f.

Lemma serie_continuous : continuous Serie.