Library Coquelicot.Hierarchy

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2017 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

From Coq Require Import Reals Psatz ssreflect.

Require Import Rcomplements Rbar Markov Iter Lub.

This file first describes Filters that are predicates of type (T Prop) Prop used for limits and neighborhoods. Then the algebraic hierarchy of the Coquelicot library is given: from the AbelianMonoid to the CompleteNormedModule. Topologies on R and R×R are also given.

More documentation details can be found in Coquelicot.html.

Open Scope R_scope.

Filters

Definitions


Class Filter {T : Type} (F : (T Prop) Prop) := {
  filter_true : F (fun _True) ;
  filter_and : P Q : T Prop, F P F Q F (fun xP x Q x) ;
  filter_imp : P Q : T Prop, ( x, P x Q x) F P F Q
}.


Class ProperFilter' {T : Type} (F : (T Prop) Prop) := {
  filter_not_empty : not (F (fun _False)) ;
  filter_filter' : Filter F
}.
#[global] Existing Instance filter_filter'.

Class ProperFilter {T : Type} (F : (T Prop) Prop) := {
  filter_ex : P, F P x, P x ;
  filter_filter : Filter F
}.
#[global] Existing Instance filter_filter.

Global Instance Proper_StrongProper :
   {T : Type} (F : (T Prop) Prop),
  ProperFilter F ProperFilter' F.

Lemma filter_forall :
   {T : Type} {F} {FF: @Filter T F} (P : T Prop),
  ( x, P x) F P.

Lemma filter_const :
   {T : Type} {F} {FF: @ProperFilter T F} (P : Prop),
  F (fun _P) P.

Limits expressed with filters


Definition filter_le {T : Type} (F G : (T Prop) Prop) :=
   P, G P F P.

Lemma filter_le_refl :
   T F, @filter_le T F F.

Lemma filter_le_trans :
   T F G H, @filter_le T F G filter_le G H filter_le F H.

Definition filtermap {T U : Type} (f : T U) (F : (T Prop) Prop) :=
  fun PF (fun xP (f x)).

Global Instance filtermap_filter :
   T U (f : T U) (F : (T Prop) Prop),
  Filter F Filter (filtermap f F).

Global Instance filtermap_proper_filter' :
   T U (f : T U) (F : (T Prop) Prop),
  ProperFilter' F ProperFilter' (filtermap f F).

Global Instance filtermap_proper_filter :
   T U (f : T U) (F : (T Prop) Prop),
  ProperFilter F ProperFilter (filtermap f F).

Definition filtermapi {T U : Type} (f : T U Prop) (F : (T Prop) Prop) :=
  fun P : U PropF (fun x y, f x y P y).

Global Instance filtermapi_filter :
   T U (f : T U Prop) (F : (T Prop) Prop),
  F (fun x( y, f x y) y1 y2, f x y1 f x y2 y1 = y2)
  Filter F Filter (filtermapi f F).

Global Instance filtermapi_proper_filter' :
   T U (f : T U Prop) (F : (T Prop) Prop),
  F (fun x( y, f x y) y1 y2, f x y1 f x y2 y1 = y2)
  ProperFilter' F ProperFilter' (filtermapi f F).

Global Instance filtermapi_proper_filter :
   T U (f : T U Prop) (F : (T Prop) Prop),
  F (fun x( y, f x y) y1 y2, f x y1 f x y2 y1 = y2)
  ProperFilter F ProperFilter (filtermapi f F).

Definition filterlim {T U : Type} (f : T U) F G :=
  filter_le (filtermap f F) G.

Lemma filterlim_id :
   T (F : (T Prop) Prop), filterlim (fun xx) F F.

Lemma filterlim_comp :
   T U V (f : T U) (g : U V) F G H,
  filterlim f F G filterlim g G H
  filterlim (fun xg (f x)) F H.

Lemma filterlim_ext_loc :
   {T U F G} {FF : Filter F} (f g : T U),
  F (fun xf x = g x)
  filterlim f F G
  filterlim g F G.

Lemma filterlim_ext :
   {T U F G} {FF : Filter F} (f g : T U),
  ( x, f x = g x)
  filterlim f F G
  filterlim g F G.

Lemma filterlim_filter_le_1 :
   {T U F G H} (f : T U),
  filter_le G F
  filterlim f F H
  filterlim f G H.

Lemma filterlim_filter_le_2 :
   {T U F G H} (f : T U),
  filter_le G H
  filterlim f F G
  filterlim f F H.

Definition filterlimi {T U : Type} (f : T U Prop) F G :=
  filter_le (filtermapi f F) G.

Lemma filterlimi_comp :
   T U V (f : T U) (g : U V Prop) F G H,
  filterlim f F G filterlimi g G H
  filterlimi (fun xg (f x)) F H.

Lemma filterlimi_ext_loc :
   {T U F G} {FF : Filter F} (f g : T U Prop),
  F (fun x y, f x y g x y)
  filterlimi f F G
  filterlimi g F G.

Lemma filterlimi_ext :
   {T U F G} {FF : Filter F} (f g : T U Prop),
  ( x y, f x y g x y)
  filterlimi f F G
  filterlimi g F G.

Lemma filterlimi_lim_ext_loc :
   {T U F G} {FF : Filter F} (f : T U) (g : T U Prop),
  F (fun xg x (f x))
  filterlim f F G
  filterlimi g F G.

Lemma filterlimi_lim_ext :
   {T U F G} {FF : Filter F} (f : T U) (g : T U Prop),
  ( x, g x (f x))
  filterlim f F G
  filterlimi g F G.

Lemma filterlimi_filter_le_1 :
   {T U F G H} (f : T U Prop),
  filter_le G F
  filterlimi f F H
  filterlimi f G H.

Lemma filterlimi_filter_le_2 :
   {T U F G H} (f : T U Prop),
  filter_le G H
  filterlimi f F G
  filterlimi f F H.

Specific filters

Filters for pairs

Inductive filter_prod {T U : Type} (F G : _ Prop) (P : T × U Prop) : Prop :=
  Filter_prod (Q : T Prop) (R : U Prop) :
    F Q G R ( x y, Q x R y P (x, y)) filter_prod F G P.

Global Instance filter_prod_filter :
   T U (F : (T Prop) Prop) (G : (U Prop) Prop),
  Filter F Filter G Filter (filter_prod F G).

Global Instance filter_prod_proper' {T1 T2 : Type}
  {F : (T1 Prop) Prop} {G : (T2 Prop) Prop}
  {FF : ProperFilter' F} {FG : ProperFilter' G} :
  ProperFilter' (filter_prod F G).

Global Instance filter_prod_proper {T1 T2 : Type}
  {F : (T1 Prop) Prop} {G : (T2 Prop) Prop}
  {FF : ProperFilter F} {FG : ProperFilter G} :
  ProperFilter (filter_prod F G).

Lemma filterlim_fst :
   {T U F G} {FG : Filter G},
  filterlim (@fst T U) (filter_prod F G) F.

Lemma filterlim_snd :
   {T U F G} {FF : Filter F},
  filterlim (@snd T U) (filter_prod F G) G.

Lemma filterlim_pair :
   {T U V F G H} {FF : Filter F},
   (f : T U) (g : T V),
  filterlim f F G
  filterlim g F H
  filterlim (fun x(f x, g x)) F (filter_prod G H).

Lemma filterlim_comp_2 :
   {T U V W F G H I} {FF : Filter F},
   (f : T U) (g : T V) (h : U V W),
  filterlim f F G
  filterlim g F H
  filterlim (fun xh (fst x) (snd x)) (filter_prod G H) I
  filterlim (fun xh (f x) (g x)) F I.

Lemma filterlimi_comp_2 :
   {T U V W F G H I} {FF : Filter F},
   (f : T U) (g : T V) (h : U V W Prop),
  filterlim f F G
  filterlim g F H
  filterlimi (fun xh (fst x) (snd x)) (filter_prod G H) I
  filterlimi (fun xh (f x) (g x)) F I.

Lemma prod_filtermap_le {T1 T2 U1 U2 F G} {FF : Filter F} {FG : Filter G}
    (f1 : T1 U1) (f2 : T2 U2) :
  filter_le (filter_prod (filtermap f1 F) (filtermap f2 G))
    (filtermap (fun x(f1 (fst x), f2 (snd x))) (filter_prod F G)).

Lemma filtermap_prod_le {T1 T2 U1 U2 F G} {FF : Filter F} {FG : Filter G}
    (f1 : T1 U1) (f2 : T2 U2) :
  filter_le (filtermap (fun x(f1 (fst x), f2 (snd x))) (filter_prod F G))
   (filter_prod (filtermap f1 F) (filtermap f2 G)).

Lemma filterlim_prod {E} {T} {U} {F : (T Prop) Prop} {FF : Filter F} (g : E U U Prop) (f : T U) :
  filterlim (fun x(f (fst x), f (snd x))) (filter_prod F F) (fun P e, u v, g e u v P (u, v))
  ( e, P, F P u v : T, P u P v g e (f u) (f v)).

Restriction of a filter to a domain

Definition within {T : Type} D (F : (T Prop) Prop) (P : T Prop) :=
  F (fun xD x P x).

Global Instance within_filter :
   T D F, Filter F Filter (@within T D F).

Lemma filter_le_within :
   {T} {F : (T Prop) Prop} {FF : Filter F} D,
  filter_le (within D F) F.

Lemma filterlim_within_ext :
   {T U F G} {FF : Filter F} D (f g : T U),
  ( x, D x f x = g x)
  filterlim f (within D F) G
  filterlim g (within D F) G.

Definition subset_filter {T} (F : (T Prop) Prop) (dom : T Prop) (P : {x|dom x} Prop) : Prop :=
  F (fun x H : dom x, P (exist _ x H)).

Global Instance subset_filter_filter :
   T F (dom : T Prop),
  Filter F
  Filter (subset_filter F dom).

Lemma subset_filter_proper' :
   {T F} {FF : Filter F} (dom : T Prop),
  ( P, F P ¬ ¬ x, dom x P x)
  ProperFilter' (subset_filter F dom).

Lemma subset_filter_proper :
   {T F} {FF : Filter F} (dom : T Prop),
  ( P, F P x, dom x P x)
  ProperFilter (subset_filter F dom).

Algebraic spaces

Abelian monoids


Module AbelianMonoid.

Record mixin_of (G : Type) := Mixin {
  plus : G G G ;
  zero : G ;
  ax1 : x y, plus x y = plus y x ;
  ax2 : x y z, plus x (plus y z) = plus (plus x y) z ;
  ax3 : x, plus x zero = x ;
}.

Notation class_of := mixin_of (only parsing).

Section ClassDef.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Definition class (cT : type) := let: Pack _ c _ := cT return class_of cT in c.

End ClassDef.

Module Exports.

Coercion sort : type >-> Sortclass.
Notation AbelianMonoid := type.

End Exports.

End AbelianMonoid.

Export AbelianMonoid.Exports.

Arithmetic operations

Section AbelianMonoid1.

Context {G : AbelianMonoid}.

Definition zero := AbelianMonoid.zero _ (AbelianMonoid.class G).
Definition plus := AbelianMonoid.plus _ (AbelianMonoid.class G).

Lemma plus_comm :
   x y : G,
  plus x y = plus y x.

Lemma plus_assoc :
   x y z : G,
  plus x (plus y z) = plus (plus x y) z.

Lemma plus_zero_r :
   x : G,
  plus x zero = x.

Lemma plus_zero_l :
   x : G,
  plus zero x = x.

End AbelianMonoid1.

Sum

Section Sums1.

Context {G : AbelianMonoid}.

Definition sum_n_m (a : nat G) n m :=
  iter_nat plus zero a n m.
Definition sum_n (a : nat G) n :=
  sum_n_m a O n.

Lemma sum_n_m_Chasles (a : nat G) (n m k : nat) :
  (n S m)%nat (m k)%nat
     sum_n_m a n k = plus (sum_n_m a n m) (sum_n_m a (S m) k).

Lemma sum_n_n (a : nat G) (n : nat) :
  sum_n_m a n n = a n.

Lemma sum_O (a : nat G) : sum_n a 0 = a O.

Lemma sum_n_Sm (a : nat G) (n m : nat) :
  (n S m)%nat sum_n_m a n (S m) = plus (sum_n_m a n m) (a (S m)).

Lemma sum_Sn_m (a : nat G) (n m : nat) :
  (n m)%nat sum_n_m a n m = plus (a n) (sum_n_m a (S n) m).

Lemma sum_n_m_S (a : nat G) (n m : nat) :
  sum_n_m (fun na (S n)) n m = sum_n_m a (S n) (S m).

Lemma sum_Sn (a : nat G) (n : nat) :
  sum_n a (S n) = plus (sum_n a n) (a (S n)).

Lemma sum_n_m_zero (a : nat G) (n m : nat) :
  (m < n)%nat sum_n_m a n m = zero.

Lemma sum_n_m_const_zero (n m : nat) :
  sum_n_m (fun _zero) n m = zero.

Lemma sum_n_m_ext_loc (a b : nat G) (n m : nat) :
  ( k, (n k m)%nat a k = b k)
  sum_n_m a n m = sum_n_m b n m.
Lemma sum_n_m_ext (a b : nat G) n m :
  ( n, a n = b n)
  sum_n_m a n m = sum_n_m b n m.

Lemma sum_n_ext_loc :
   (a b : nat G) N,
  ( n, (n N)%nat a n = b n)
  sum_n a N = sum_n b N.

Lemma sum_n_ext :
   (a b : nat G) N,
  ( n, a n = b n)
  sum_n a N = sum_n b N.

Lemma sum_n_m_plus :
   (u v : nat G) (n m : nat),
  sum_n_m (fun kplus (u k) (v k)) n m = plus (sum_n_m u n m) (sum_n_m v n m).

Lemma sum_n_plus :
   (u v : nat G) (n : nat),
  sum_n (fun kplus (u k) (v k)) n = plus (sum_n u n) (sum_n v n).

Lemma sum_n_switch :
   (u : nat nat G) (m n : nat),
  sum_n (fun isum_n (u i) n) m = sum_n (fun jsum_n (fun iu i j) m) n.

End Sums1.

Abelian groups


Module AbelianGroup.

Record mixin_of (G : AbelianMonoid) := Mixin {
  opp : G G ;
  ax1 : x, plus x (opp x) = zero
}.

Section ClassDef.

Record class_of (G : Type) := Class {
  base : AbelianMonoid.class_of G ;
  mixin : mixin_of (AbelianMonoid.Pack _ base G)
}.
Local Coercion base : class_of >-> AbelianMonoid.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> AbelianMonoid.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Notation AbelianGroup := type.

End Exports.

End AbelianGroup.

Export AbelianGroup.Exports.

Arithmetic operations

Section AbelianGroup1.

Context {G : AbelianGroup}.

Definition opp := AbelianGroup.opp _ (AbelianGroup.class G).
Definition minus x y := (plus x (opp y)).

Lemma plus_opp_r :
   x : G,
  plus x (opp x) = zero.

Lemma plus_opp_l :
   x : G,
  plus (opp x) x = zero.

Lemma opp_zero :
  opp zero = zero.

Lemma minus_zero_r :
   x : G,
  minus x zero = x.

Lemma minus_eq_zero (x : G) :
  minus x x = zero.

Lemma plus_reg_l :
   r x y : G,
  plus r x = plus r y x = y.

Lemma plus_reg_r :
   r x y : G,
  plus x r = plus y r x = y.

Lemma opp_opp :
   x : G,
  opp (opp x) = x.

Lemma opp_plus :
   x y : G,
  opp (plus x y) = plus (opp x) (opp y).

Lemma opp_minus (x y : G) :
  opp (minus x y) = minus y x.

Lemma minus_trans (r x y : G) :
  minus x y = plus (minus x r) (minus r y).

End AbelianGroup1.

Sum

Section Sums2.

Context {G : AbelianGroup}.

Lemma sum_n_m_sum_n (a:nat G) (n m : nat) :
  (n m)%nat sum_n_m a (S n) m = minus (sum_n a m) (sum_n a n).

End Sums2.

Noncommutative rings


Module Ring.

Record mixin_of (K : AbelianGroup) := Mixin {
  mult : K K K ;
  one : K ;
  ax1 : x y z, mult x (mult y z) = mult (mult x y) z ;
  ax2 : x, mult x one = x ;
  ax3 : x, mult one x = x ;
  ax4 : x y z, mult (plus x y) z = plus (mult x z) (mult y z) ;
  ax5 : x y z, mult x (plus y z) = plus (mult x y) (mult x z)
}.

Section ClassDef.

Record class_of (K : Type) := Class {
  base : AbelianGroup.class_of K ;
  mixin : mixin_of (AbelianGroup.Pack _ base K)
}.
Local Coercion base : class_of >-> AbelianGroup.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> AbelianGroup.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Notation Ring := type.

End Exports.

End Ring.

Export Ring.Exports.

Arithmetic operations

Section Ring1.

Context {K : Ring}.

Definition mult : K K K := Ring.mult _ (Ring.class K).
Definition one : K := Ring.one _ (Ring.class K).

Lemma mult_assoc :
   x y z : K,
  mult x (mult y z) = mult (mult x y) z.

Lemma mult_one_r :
   x : K,
  mult x one = x.

Lemma mult_one_l :
   x : K,
  mult one x = x.

Lemma mult_distr_r :
   x y z : K,
  mult (plus x y) z = plus (mult x z) (mult y z).

Lemma mult_distr_l :
   x y z : K,
  mult x (plus y z) = plus (mult x y) (mult x z).

Lemma mult_zero_r :
   x : K,
  mult x zero = zero.

Lemma mult_zero_l :
   x : K,
  mult zero x = zero.

Lemma opp_mult_r :
   x y : K,
  opp (mult x y) = mult x (opp y).

Lemma opp_mult_l :
   x y : K,
  opp (mult x y) = mult (opp x) y.

Lemma opp_mult_m1 :
   x : K,
  opp x = mult (opp one) x.

Lemma sum_n_m_mult_r :
  (a : K) (u : nat K) (n m : nat),
  sum_n_m (fun kmult (u k) a) n m = mult (sum_n_m u n m) a.

Lemma sum_n_m_mult_l :
  (a : K) (u : nat K) (n m : nat),
  sum_n_m (fun kmult a (u k)) n m = mult a (sum_n_m u n m).

Lemma sum_n_mult_r :
  (a : K) (u : nat K) (n : nat),
  sum_n (fun kmult (u k) a) n = mult (sum_n u n) a.

Lemma sum_n_mult_l :
  (a : K) (u : nat K) (n : nat),
  sum_n (fun kmult a (u k)) n = mult a (sum_n u n).

pow_n

Fixpoint pow_n (x : K) (N : nat) {struct N} : K :=
  match N with
   | 0%natone
   | S imult x (pow_n x i)
  end.

Lemma pow_n_plus :
   (x : K) (n m : nat), pow_n x (n+m) = mult (pow_n x n) (pow_n x m).

Lemma pow_n_comm_1 :
   (x : K) (n : nat), mult (pow_n x n) x = mult x (pow_n x n).

Lemma pow_n_comm :
   (x : K) n m, mult (pow_n x n) (pow_n x m) = mult (pow_n x m) (pow_n x n).

End Ring1.

Rings with absolute value


Module AbsRing.

Record mixin_of (K : Ring) := Mixin {
  abs : K R ;
  ax1 : abs zero = 0 ;
  ax2 : abs (opp one) = 1 ;
  ax3 : x y : K, abs (plus x y) abs x + abs y ;
  ax4 : x y : K, abs (mult x y) abs x × abs y ;
  ax5 : x : K, abs x = 0 x = zero
}.

Section ClassDef.

Record class_of (K : Type) := Class {
  base : Ring.class_of K ;
  mixin : mixin_of (Ring.Pack _ base K)
}.
Local Coercion base : class_of >-> Ring.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition Ring := Ring.Pack cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> Ring.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion Ring : type >-> Ring.type.
Canonical Ring.
Notation AbsRing := type.

End Exports.

End AbsRing.

Export AbsRing.Exports.

Usual properties

Section AbsRing1.

Context {K : AbsRing}.

Definition abs : K R := AbsRing.abs _ (AbsRing.class K).

Lemma abs_zero :
  abs zero = 0.

Lemma abs_opp_one :
  abs (opp one) = 1.

Lemma abs_triangle :
   x y : K,
  abs (plus x y) abs x + abs y.

Lemma abs_mult :
   x y : K,
  abs (mult x y) abs x × abs y.

Lemma abs_eq_zero :
   x : K,
  abs x = 0 x = zero.

Lemma abs_opp :
   x, abs (opp x) = abs x.

Lemma abs_minus :
   x y : K, abs (minus x y) = abs (minus y x).

Lemma abs_one :
  abs one = 1.

Lemma abs_ge_0 :
   x, 0 abs x.

Lemma abs_gt_0 :
   x : K,
  x zero 0 < abs x.

Lemma abs_minus_gt_0 :
   x y : K,
  x y 0 < abs (minus x y).

Lemma abs_pow_n :
   (x : K) n,
  abs (pow_n x n) (abs x)^n.

End AbsRing1.

Uniform spaces defined using balls


Module UniformSpace.

Record mixin_of (M : Type) := Mixin {
  point_of : M ;
  ball : M R M Prop ;
  ax1 : x (e : posreal), ball x e x ;
  ax2 : x y e, ball x e y ball y e x ;
  ax3 : x y z e1 e2, ball x e1 y ball y e2 z ball x (e1 + e2) z
}.

Notation class_of := mixin_of (only parsing).

Section ClassDef.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Definition class (cT : type) := let: Pack _ c _ := cT return class_of cT in c.

End ClassDef.

Module Exports.

Coercion sort : type >-> Sortclass.
Notation UniformSpace := type.

End Exports.

End UniformSpace.

Export UniformSpace.Exports.

Section UniformSpace1.

Context {M : UniformSpace}.

Definition point_of := UniformSpace.point_of _ (UniformSpace.class M).

Definition ball := UniformSpace.ball _ (UniformSpace.class M).

Lemma ball_center :
   (x : M) (e : posreal),
  ball x e x.

Lemma ball_sym :
   (x y : M) (e : R),
  ball x e y ball y e x.

Lemma ball_triangle :
   (x y z : M) (e1 e2 : R),
  ball x e1 y ball y e2 z ball x (e1 + e2) z.

Lemma ball_le :
   (x : M) (e1 e2 : R), e1 e2
   (y : M), ball x e1 y ball x e2 y.

Definition close (x y : M) : Prop := eps : posreal, ball x eps y.

Lemma close_refl (x : M) : close x x.

Lemma close_sym (x y : M) : close x y close y x.

Lemma close_trans (x y z : M) : close x y close y z close x z.

End UniformSpace1.

Specific uniform spaces

Rings with absolute value
Functional metric spaces

Section fct_UniformSpace.

Variable (T : Type) (U : UniformSpace).

Definition fct_ball (x : T U) (eps : R) (y : T U) :=
   t : T, ball (x t) eps (y t).

Lemma fct_ball_center :
   (x : T U) (e : posreal),
  fct_ball x e x.

Lemma fct_ball_sym :
   (x y : T U) (e : R),
  fct_ball x e y fct_ball y e x.

Lemma fct_ball_triangle :
   (x y z : T U) (e1 e2 : R),
  fct_ball x e1 y fct_ball y e2 z fct_ball x (e1 + e2) z.

Definition fct_UniformSpace_mixin :=
  UniformSpace.Mixin _ (fun _point_of) _ fct_ball_center fct_ball_sym fct_ball_triangle.

Canonical fct_UniformSpace :=
  UniformSpace.Pack (T U) fct_UniformSpace_mixin (T U).

End fct_UniformSpace.

Local predicates

locally_dist

Definition locally_dist {T : Type} (d : T R) (P : T Prop) :=
   delta : posreal, y, d y < delta P y.

Global Instance locally_dist_filter :
   T (d : T R), Filter (locally_dist d).

locally

Section Locally.

Context {T : UniformSpace}.

Definition locally (x : T) (P : T Prop) :=
   eps : posreal, y, ball x eps y P y.

Global Instance locally_filter :
   x : T, ProperFilter (locally x).

Lemma locally_locally :
   (x : T) (P : T Prop),
  locally x P locally x (fun ylocally y P).

Lemma locally_singleton :
   (x : T) (P : T Prop),
  locally x P P x.

Lemma locally_ball :
   (x : T) (eps : posreal), locally x (ball x eps).

Lemma locally_not' :
   (x : T) (P : T Prop),
  not ( eps : posreal, not ( y, ball x eps y not (P y)))
  {d : posreal | y, ball x d y not (P y)}.

Lemma locally_not :
   (x : T) (P : T Prop),
  not ( eps : posreal, not ( y, ball x eps y not (P y)))
  locally x (fun ynot (P y)).

Lemma locally_ex_not :
   (x : T) (P : T Prop),
  locally x (fun ynot (P y))
  {d : posreal | y, ball x d y not (P y)}.

Lemma locally_ex_dec :
   (x : T) (P : T Prop),
  ( x, P x ¬P x)
  locally x P
  {d : posreal | y, ball x d y P y}.

Definition is_filter_lim (F : (T Prop) Prop) (x : T) :=
   P, locally x P F P.

Lemma is_filter_lim_filter_le :
   {F G} (x : T),
  filter_le G F
  is_filter_lim F x is_filter_lim G x.

Lemma is_filter_lim_close {F} {FF : ProperFilter F} (x y : T) :
  is_filter_lim F x is_filter_lim F y close x y.

Lemma is_filter_lim_locally_close (x y : T) :
  is_filter_lim (locally x) y close x y.

End Locally.

Lemma filterlim_const :
   {T} {U : UniformSpace} {F : (T Prop) Prop} {FF : Filter F},
   a : U, filterlim (fun _a) F (locally a).

Section Locally_fct.

Context {T : Type} {U : UniformSpace}.

Lemma filterlim_locally :
   {F} {FF : Filter F} (f : T U) y,
  filterlim f F (locally y)
   eps : posreal, F (fun xball y eps (f x)).

Lemma filterlimi_locally :
   {F} {FF : Filter F} (f : T U Prop) y,
  filterlimi f F (locally y)
   eps : posreal, F (fun x z, f x z ball y eps z).

Lemma filterlim_locally_close :
   {F} {FF: ProperFilter F} (f : T U) l l',
  filterlim f F (locally l) filterlim f F (locally l')
  close l l'.

Lemma filterlimi_locally_close :
   {F} {FF: ProperFilter F} (f : T U Prop) l l',
  F (fun x y1 y2, f x y1 f x y2 y1 = y2)
  filterlimi f F (locally l) filterlimi f F (locally l')
  close l l'.

End Locally_fct.

Lemma is_filter_lim_filtermap {T: UniformSpace} {U : UniformSpace} :
F x (f : T U),
  filterlim f (locally x) (locally (f x))
   is_filter_lim F x
   is_filter_lim (filtermap f F) (f x).

locally'

Definition locally' {T : UniformSpace} (x : T) :=
  within (fun yy x) (locally x).

Global Instance locally'_filter :
   {T : UniformSpace} (x : T), Filter (locally' x).

closely

Section closely.

Context {T : UniformSpace}.

Definition closely (P : T × T Prop) :=
   eps : posreal, u v : T, ball u eps v P (u, v).

Global Instance closely_filter :
  ProperFilter closely.

End closely.

Lemma filterlim_closely {T} {U : UniformSpace} {F : (T Prop) Prop} {FF : Filter F} (f : T U) :
  filterlim (fun x(f (fst x), f (snd x))) (filter_prod F F) closely
  ( eps : posreal, P, F P u v : T, P u P v ball (f u) eps (f v)).

Pointed filter

Section at_point.

Context {T : UniformSpace}.

Definition at_point (a : T) (P : T Prop) : Prop := P a.

Global Instance at_point_filter (a : T) :
  ProperFilter (at_point a).

End at_point.

Open sets in uniform spaces


Section Open.

Context {T : UniformSpace}.

Definition open (D : T Prop) :=
   x, D x locally x D.

Lemma locally_open :
   (D E : T Prop),
  open D
  ( x : T, D x E x)
   x : T, D x
  locally x E.

Lemma open_ext :
   D E : T Prop,
  ( x, D x E x)
  open D open E.

Lemma open_and :
   D E : T Prop,
  open D open E
  open (fun xD x E x).

Lemma open_or :
   D E : T Prop,
  open D open E
  open (fun xD x E x).

Lemma open_true :
  open (fun x : TTrue).

Lemma open_false :
  open (fun x : TFalse).

End Open.

Lemma open_comp :
   {T U : UniformSpace} (f : T U) (D : U Prop),
  ( x, D (f x) filterlim f (locally x) (locally (f x)))
  open D open (fun x : TD (f x)).

Closed sets in uniform spaces


Section Closed.

Context {T : UniformSpace}.

Definition closed (D : T Prop) :=
   x, not (locally x (fun x : Tnot (D x))) D x.

Lemma open_not :
   D : T Prop,
  closed D open (fun xnot (D x)).

Lemma closed_not :
   D : T Prop,
  open D closed (fun xnot (D x)).

Lemma closed_ext :
   D E : T Prop,
  ( x, D x E x)
  closed D closed E.

Lemma closed_and :
   D E : T Prop,
  closed D closed E
  closed (fun xD x E x).


Lemma closed_true :
  closed (fun x : TTrue).

Lemma closed_false :
  closed (fun x : TFalse).

End Closed.

Lemma closed_comp :
   {T U : UniformSpace} (f : T U) (D : U Prop),
  ( x, filterlim f (locally x) (locally (f x)))
  closed D closed (fun x : TD (f x)).

Lemma closed_filterlim_loc :
   {T} {U : UniformSpace} {F} {FF : ProperFilter' F} (f : T U) (D : U Prop),
   y, filterlim f F (locally y)
  F (fun xD (f x))
  closed D D y.

Lemma closed_filterlim :
   {T} {U : UniformSpace} {F} {FF : ProperFilter' F} (f : T U) (D : U Prop),
   y, filterlim f F (locally y)
  ( x, D (f x))
  closed D D y.

Complete uniform spaces


Definition cauchy {T : UniformSpace} (F : (T Prop) Prop) :=
   eps : posreal, x, F (ball x eps).

Module CompleteSpace.

Record mixin_of (T : UniformSpace) := Mixin {
  lim : ((T Prop) Prop) T ;
  ax1 : F, ProperFilter F cauchy F eps : posreal, F (ball (lim F) eps) ;
  ax2 : F1 F2, filter_le F1 F2 filter_le F2 F1 close (lim F1) (lim F2)
}.

Section ClassDef.

Record class_of (T : Type) := Class {
  base : UniformSpace.class_of T ;
  mixin : mixin_of (UniformSpace.Pack _ base T)
}.
Local Coercion base : class_of >-> UniformSpace.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition UniformSpace := UniformSpace.Pack cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> UniformSpace.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Notation CompleteSpace := type.

End Exports.

End CompleteSpace.

Export CompleteSpace.Exports.

Section CompleteSpace1.

Context {T : CompleteSpace}.

Definition lim : ((T Prop) Prop) T := CompleteSpace.lim _ (CompleteSpace.class T).

Lemma complete_cauchy :
   F : (T Prop) Prop,
  ProperFilter F cauchy F
   eps : posreal,
  F (ball (lim F) eps).

Lemma close_lim :
   F1 F2 : (T Prop) Prop,
  filter_le F1 F2 filter_le F2 F1
  close (lim F1) (lim F2).

Definition iota (P : T Prop) := lim (fun A ⇒ ( x, P x A x)).

Lemma iota_correct_weak :
   P : T Prop,
  ( x y, P x P y close x y)
   x, P x close (iota P) x.

Lemma close_iota :
   P Q : T Prop,
  ( x, P x Q x)
  close (iota P) (iota Q).

End CompleteSpace1.

Lemma cauchy_distance' :
   {T : UniformSpace} {F} {FF : ProperFilter F},
  cauchy F filter_le (filter_prod F F) (@closely T).

Lemma cauchy_distance :
   {T : UniformSpace} {F} {FF : ProperFilter F},
  cauchy F
  ( eps : posreal, P, F P u v : T, P u P v ball u eps v).

Section fct_CompleteSpace.

Context {T : Type} {U : CompleteSpace}.

Lemma filterlim_locally_closely :
   {F} {FF : ProperFilter F} (f : T U),
  filterlim (fun x(f (fst x), f (snd x))) (filter_prod F F) closely
   y, filterlim f F (locally y).

Lemma filterlim_locally_cauchy :
   {F} {FF : ProperFilter F} (f : T U),
  ( eps : posreal, P, F P u v : T, P u P v ball (f u) eps (f v))
   y, filterlim f F (locally y).

Lemma filterlimi_locally_cauchy :
   {F} {FF : ProperFilter F} (f : T U Prop),
  F (fun x( y, f x y)
    ( y1 y2, f x y1 f x y2 y1 = y2))
  (( eps : posreal, P, F P
    u v : T, P u P v u' v': U, f u u' f v v' ball u' eps v')
   y, filterlimi f F (locally y)).

Definition lim_fct (F : ((T U) Prop) Prop) (t : T) :=
  lim (fun PF (fun gP (g t))).

Lemma complete_cauchy_fct :
   (F : ((T U) Prop) Prop),
  ProperFilter F
  ( eps : posreal, f : T U, F (ball f eps))
   eps : posreal, F (ball (lim_fct F) eps).

Lemma close_lim_fct :
   F1 F2 : ((T U) Prop) Prop,
  filter_le F1 F2 filter_le F2 F1
  close (lim_fct F1) (lim_fct F2).

Definition fct_CompleteSpace_mixin :=
  CompleteSpace.Mixin _ lim_fct complete_cauchy_fct close_lim_fct.

Canonical fct_CompleteSpace :=
  CompleteSpace.Pack (T U) (CompleteSpace.Class _ _ fct_CompleteSpace_mixin) (T U).

End fct_CompleteSpace.

Limit switching


Section Filterlim_switch.

Context {T1 T2 : Type}.

Lemma filterlim_switch_1 {U : UniformSpace}
  F1 (FF1 : ProperFilter F1) F2 (FF2 : Filter F2) (f : T1 T2 U) g h (l : U) :
  filterlim f F1 (locally g)
  ( x, filterlim (f x) F2 (locally (h x)))
  filterlim h F1 (locally l) filterlim g F2 (locally l).

Lemma filterlim_switch_2 {U : CompleteSpace}
  F1 (FF1 : ProperFilter F1) F2 (FF2 : ProperFilter F2) (f : T1 T2 U) g h :
  filterlim f F1 (locally g)
  ( x, filterlim (f x) F2 (locally (h x)))
   l : U, filterlim h F1 (locally l).

Lemma filterlim_switch {U : CompleteSpace}
  F1 (FF1 : ProperFilter F1) F2 (FF2 : ProperFilter F2) (f : T1 T2 U) g h :
  filterlim f F1 (locally g)
  ( x, filterlim (f x) F2 (locally (h x)))
   l : U, filterlim h F1 (locally l) filterlim g F2 (locally l).

End Filterlim_switch.

Lemma filterlim_switch_dom {T1 T2 : Type} {U : CompleteSpace}
  F1 (FF1 : ProperFilter F1) F2 (FF2 : Filter F2)
  (dom : T2 Prop) (HF2 : P, F2 P x, dom x P x)
  (f : T1 T2 U) g h :
  filterlim (fun x (y : {z : T2 | dom z}) ⇒ f x (proj1_sig y)) F1 (locally (T := fct_UniformSpace _ _) (fun y : {z : T2 | dom z}g (proj1_sig y)))
  ( x, filterlim (f x) (within dom F2) (locally (h x)))
   l : U, filterlim h F1 (locally l) filterlim g (within dom F2) (locally l).

Modules


Module ModuleSpace.

Record mixin_of (K : Ring) (V : AbelianGroup) := Mixin {
  scal : K V V ;
  ax1 : x y u, scal x (scal y u) = scal (mult x y) u ;
  ax2 : u, scal one u = u ;
  ax3 : x u v, scal x (plus u v) = plus (scal x u) (scal x v) ;
  ax4 : x y u, scal (plus x y) u = plus (scal x u) (scal y u)
}.

Section ClassDef.

Variable K : Ring.

Record class_of (V : Type) := Class {
  base : AbelianGroup.class_of V ;
  mixin : mixin_of K (AbelianGroup.Pack _ base V)
}.
Local Coercion base : class_of >-> AbelianGroup.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> AbelianGroup.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Notation ModuleSpace := type.

End Exports.

End ModuleSpace.

Export ModuleSpace.Exports.

Section ModuleSpace1.

Context {K : Ring} {V : ModuleSpace K}.

Definition scal : K V V := ModuleSpace.scal _ _ (ModuleSpace.class K V).

Lemma scal_assoc :
   (x y : K) (u : V),
  scal x (scal y u) = scal (mult x y) u.

Lemma scal_one :
   (u : V), scal one u = u.

Lemma scal_distr_l :
   (x : K) (u v : V),
  scal x (plus u v) = plus (scal x u) (scal x v).

Lemma scal_distr_r :
   (x y : K) (u : V),
  scal (plus x y) u = plus (scal x u) (scal y u).

Lemma scal_zero_r :
   x : K,
  scal x zero = zero.

Lemma scal_zero_l :
   u : V,
  scal zero u = zero.

Lemma scal_opp_l :
   (x : K) (u : V),
  scal (opp x) u = opp (scal x u).

Lemma scal_opp_r :
   (x : K) (u : V),
  scal x (opp u) = opp (scal x u).

Lemma scal_opp_one :
   u : V,
  scal (opp one) u = opp u.

Lemma scal_minus_distr_l (x : K) (u v : V) :
   scal x (minus u v) = minus (scal x u) (scal x v).
Lemma scal_minus_distr_r (x y : K) (u : V) :
   scal (minus x y) u = minus (scal x u) (scal y u).

Lemma sum_n_m_scal_l :
   (a : K) (u : nat V) (n m : nat),
  sum_n_m (fun kscal a (u k)) n m = scal a (sum_n_m u n m).

Lemma sum_n_scal_l :
   (a : K) (u : nat V) (n : nat),
  sum_n (fun kscal a (u k)) n = scal a (sum_n u n).

End ModuleSpace1.

Rings are modules

Modules with a norm


Module NormedModuleAux.

Section ClassDef.

Variable K : AbsRing.

Record class_of (T : Type) := Class {
  base : ModuleSpace.class_of K T ;
  mixin : UniformSpace.mixin_of T
}.
Local Coercion base : class_of >-> ModuleSpace.class_of.
Local Coercion mixin : class_of >-> UniformSpace.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition ModuleSpace := ModuleSpace.Pack _ cT xclass xT.
Definition UniformSpace := UniformSpace.Pack cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> ModuleSpace.class_of.
Coercion mixin : class_of >-> UniformSpace.class_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion ModuleSpace : type >-> ModuleSpace.type.
Canonical ModuleSpace.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Notation NormedModuleAux := type.

End Exports.

End NormedModuleAux.

Export NormedModuleAux.Exports.

Module NormedModule.

Record mixin_of (K : AbsRing) (V : NormedModuleAux K) := Mixin {
  norm : V R ;
  norm_factor : R ;
  ax1 : (x y : V), norm (plus x y) norm x + norm y ;
  ax2 : (l : K) (x : V), norm (scal l x) abs l × norm x ;
  ax3 : (x y : V) (eps : R), norm (minus y x) < eps ball x eps y ;
  ax4 : (x y : V) (eps : posreal), ball x eps y norm (minus y x) < norm_factor × eps ;
  ax5 : x : V, norm x = 0 x = zero
}.

Section ClassDef.

Variable K : AbsRing.

Record class_of (T : Type) := Class {
  base : NormedModuleAux.class_of K T ;
  mixin : mixin_of K (NormedModuleAux.Pack K T base T)
}.
Local Coercion base : class_of >-> NormedModuleAux.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition ModuleSpace := ModuleSpace.Pack _ cT xclass xT.
Definition UniformSpace := UniformSpace.Pack cT xclass xT.
Definition NormedModuleAux := NormedModuleAux.Pack _ cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> NormedModuleAux.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion ModuleSpace : type >-> ModuleSpace.type.
Canonical ModuleSpace.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Coercion NormedModuleAux : type >-> NormedModuleAux.type.
Canonical NormedModuleAux.
Notation NormedModule := type.

End Exports.

End NormedModule.

Export NormedModule.Exports.

Section NormedModule1.

Context {K : AbsRing} {V : NormedModule K}.

Definition norm : V R := NormedModule.norm K _ (NormedModule.class K V).

Definition norm_factor : R := NormedModule.norm_factor K _ (NormedModule.class K V).

Lemma norm_triangle :
   x y : V,
  norm (plus x y) norm x + norm y.

Lemma norm_scal :
   (l : K) (x : V),
  norm (scal l x) abs l × norm x.

Lemma norm_compat1 :
   (x y : V) (eps : R),
  norm (minus y x) < eps ball x eps y.

Lemma norm_compat2 :
   (x y : V) (eps : posreal), ball x eps y norm (minus y x) < norm_factor × eps.

Lemma norm_eq_zero :
   x : V, norm x = 0 x = zero.

Lemma norm_zero :
  norm zero = 0.

Lemma norm_factor_gt_0 :
  0 < norm_factor.

Lemma norm_opp :
   x : V,
  norm (opp x) = norm x.

Lemma norm_ge_0 :
   x : V,
  0 norm x.

Lemma norm_gt_0 :
   x : V,
  x zero 0 < norm x.

Lemma norm_minus_gt_0 :
   x y : V,
  x y 0 < norm (minus x y).

Lemma norm_triangle_inv :
   x y : V,
  Rabs (norm x - norm y) norm (minus x y).

Lemma eq_dec :
   x y : V,
  { x = y } + { x y }.

Lemma eq_close :
   x y : V,
  close x y x = y.

Definition ball_norm (x : V) (eps : R) (y : V) := norm (minus y x) < eps.

Definition locally_norm (x : V) (P : V Prop) :=
   eps : posreal, y, ball_norm x eps y P y.

Lemma locally_le_locally_norm :
   x, filter_le (locally x) (locally_norm x).

Lemma locally_norm_le_locally :
   x, filter_le (locally_norm x) (locally x).

Lemma locally_norm_ball_norm :
   (x : V) (eps : posreal),
  locally_norm x (ball_norm x eps).

Lemma locally_norm_ball :
   (x : V) (eps : posreal),
  locally_norm x (ball x eps).

Lemma locally_ball_norm :
   (x : V) (eps : posreal),
  locally x (ball_norm x eps).

Lemma ball_norm_triangle (x y z : V) (e1 e2 : R) :
  ball_norm x e1 y ball_norm y e2 z ball_norm x (e1 + e2) z.

Lemma ball_norm_center (x : V) (e : posreal) :
  ball_norm x e x.

Lemma ball_norm_dec : (x y : V) (eps : posreal),
  {ball_norm x eps y} + {¬ ball_norm x eps y}.

Lemma ball_norm_sym :
   (x y : V) (eps : posreal), ball_norm x eps y ball_norm y eps x.

Lemma ball_norm_le :
   (x : V) (e1 e2 : posreal), e1 e2
   y, ball_norm x e1 y ball_norm x e2 y.

Lemma ball_norm_eq :
   x y : V,
  ( eps : posreal, ball_norm x eps y) x = y.

Lemma is_filter_lim_unique :
   {F} {FF : ProperFilter' F} (x y : V),
  is_filter_lim F x is_filter_lim F y x = y.

Lemma is_filter_lim_locally_unique :
   (x y : V),
  is_filter_lim (locally x) y x = y.

Definition closely_norm (P : V × V Prop) :=
   eps : posreal, x y, ball_norm x eps y P (x, y).

Lemma closely_le_closely_norm :
  filter_le closely closely_norm.

Lemma closely_norm_le_closely :
  filter_le closely_norm closely.

End NormedModule1.

Section NormedModule2.

Context {T : Type} {K : AbsRing} {V : NormedModule K}.

Lemma filterlim_closely_norm {F : (T Prop) Prop} {FF : Filter F} (f : T V) :
  filterlim (fun x(f (fst x), f (snd x))) (filter_prod F F) closely_norm
  ( eps : posreal, P, F P u v : T, P u P v ball_norm (f u) eps (f v)).

Lemma filterlim_locally_unique :
   {F} {FF : ProperFilter' F} (f : T V) (x y : V),
  filterlim f F (locally x) filterlim f F (locally y)
  x = y.

Lemma filterlimi_locally_unique :
   {F} {FF : ProperFilter' F} (f : T V Prop) (x y : V),
  F (fun x y1 y2, f x y1 f x y2 y1 = y2)
  filterlimi f F (locally x) filterlimi f F (locally y)
  x = y.

End NormedModule2.

Rings with absolute values are normed modules
Normed vector spaces have some continuous functions

Section NVS_continuity.

Context {K : AbsRing} {V : NormedModule K}.

Lemma filterlim_plus :
   x y : V,
  filterlim (fun z : V × Vplus (fst z) (snd z)) (filter_prod (locally x) (locally y)) (locally (plus x y)).

Lemma filterlim_scal (k : K) (x : V) :
  filterlim (fun zscal (fst z) (snd z)) (filter_prod (locally k) (locally x)) (locally (scal k x)).
Lemma filterlim_scal_r (k : K) (x : V) :
  filterlim (fun z : Vscal k z) (locally x) (locally (scal k x)).
Lemma filterlim_scal_l (k : K) (x : V) :
  filterlim (fun zscal z x) (locally k) (locally (scal k x)).

Lemma filterlim_opp :
   x : V,
  filterlim opp (locally x) (locally (opp x)).

End NVS_continuity.

Lemma filterlim_mult {K : AbsRing} (x y : K) :
  filterlim (fun zmult (fst z) (snd z)) (filter_prod (locally x) (locally y)) (locally (mult x y)).

Lemma filterlim_locally_ball_norm :
   {K : AbsRing} {T} {U : NormedModule K} {F : (T Prop) Prop} {FF : Filter F} (f : T U) (y : U),
  filterlim f F (locally y) eps : posreal, F (fun xball_norm y eps (f x)).

Complete Normed Modules


Module CompleteNormedModule.

Section ClassDef.

Variable K : AbsRing.

Record class_of (T : Type) := Class {
  base : NormedModule.class_of K T ;
  mixin : CompleteSpace.mixin_of (UniformSpace.Pack T base T)
}.
Local Coercion base : class_of >-> NormedModule.class_of.
Definition base2 T (cT : class_of T) : CompleteSpace.class_of T :=
  CompleteSpace.Class _ (base T cT) (mixin T cT).
Local Coercion base2 : class_of >-> CompleteSpace.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition ModuleSpace := ModuleSpace.Pack _ cT xclass xT.
Definition NormedModuleAux := NormedModuleAux.Pack _ cT xclass xT.
Definition NormedModule := NormedModule.Pack _ cT xclass xT.
Definition UniformSpace := UniformSpace.Pack cT xclass xT.
Definition CompleteSpace := CompleteSpace.Pack cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> NormedModule.class_of.
Coercion mixin : class_of >-> CompleteSpace.mixin_of.
Coercion base2 : class_of >-> CompleteSpace.class_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion ModuleSpace : type >-> ModuleSpace.type.
Canonical ModuleSpace.
Coercion NormedModuleAux : type >-> NormedModuleAux.type.
Canonical NormedModuleAux.
Coercion NormedModule : type >-> NormedModule.type.
Canonical NormedModule.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Coercion CompleteSpace : type >-> CompleteSpace.type.
Canonical CompleteSpace.
Notation CompleteNormedModule := type.

End Exports.

End CompleteNormedModule.

Export CompleteNormedModule.Exports.

Section CompleteNormedModule1.

Context {K : AbsRing} {V : CompleteNormedModule K}.

Lemma iota_unique :
   (P : V Prop) (x : V),
  ( y, P y y = x)
  P x
  iota P = x.

Lemma iota_correct :
   P : V Prop,
  (! x : V, P x)
  P (iota P).

Lemma iota_is_filter_lim {F} {FF : ProperFilter' F} (l : V) :
  is_filter_lim F l
  iota (is_filter_lim F) = l.

Context {T : Type}.

Lemma iota_filterlim_locally {F} {FF : ProperFilter' F} (f : T V) l :
  filterlim f F (locally l)
  iota (fun xfilterlim f F (locally x)) = l.

Lemma iota_filterlimi_locally {F} {FF : ProperFilter' F} (f : T V Prop) l :
  F (fun x y1 y2, f x y1 f x y2 y1 = y2)
  filterlimi f F (locally l)
  iota (fun xfilterlimi f F (locally x)) = l.

End CompleteNormedModule1.

Extended Types

Pairs


Section prod_AbelianMonoid.

Context {U V : AbelianMonoid}.

Definition prod_plus (x y : U × V) :=
  (plus (fst x) (fst y), plus (snd x) (snd y)).

Definition prod_zero : U × V := (zero, zero).

Lemma prod_plus_comm :
   x y : U × V,
  prod_plus x y = prod_plus y x.

Lemma prod_plus_assoc :
   x y z : U × V,
  prod_plus x (prod_plus y z) = prod_plus (prod_plus x y) z.

Lemma prod_plus_zero_r :
   x : U × V,
  prod_plus x prod_zero = x.

End prod_AbelianMonoid.

Definition prod_AbelianMonoid_mixin (U V : AbelianMonoid) :=
  AbelianMonoid.Mixin (U × V) _ _ prod_plus_comm prod_plus_assoc prod_plus_zero_r.

Canonical prod_AbelianMonoid (U V : AbelianMonoid) :=
  AbelianMonoid.Pack (U × V) (prod_AbelianMonoid_mixin U V) (U × V).

Section prod_AbelianGroup.

Context {U V : AbelianGroup}.

Definition prod_opp (x : U × V) :=
  (opp (fst x), opp (snd x)).

Lemma prod_plus_opp_r :
   x : U × V,
  prod_plus x (prod_opp x) = prod_zero.

End prod_AbelianGroup.

Definition prod_AbelianGroup_mixin (U V : AbelianGroup) :=
  AbelianGroup.Mixin _ _ (@prod_plus_opp_r U V).

Canonical prod_AbelianGroup (U V : AbelianGroup) :=
  AbelianGroup.Pack (U × V) (AbelianGroup.Class _ _ (prod_AbelianGroup_mixin U V)) (U × V).

Section prod_UniformSpace.

Context {U V : UniformSpace}.

Definition prod_ball (x : U × V) (eps : R) (y : U × V) :=
  ball (fst x) eps (fst y) ball (snd x) eps (snd y).

Lemma prod_ball_center :
   (x : U × V) (eps : posreal),
  prod_ball x eps x.

Lemma prod_ball_sym :
   (x y : U × V) (eps : R),
  prod_ball x eps y prod_ball y eps x.

Lemma prod_ball_triangle :
   (x y z : U × V) (e1 e2 : R),
  prod_ball x e1 y prod_ball y e2 z
  prod_ball x (e1 + e2) z.

End prod_UniformSpace.

Definition prod_UniformSpace_mixin (U V : UniformSpace) :=
  UniformSpace.Mixin (U × V) (point_of, point_of) _ prod_ball_center prod_ball_sym prod_ball_triangle.

Canonical prod_UniformSpace (U V : UniformSpace) :=
  UniformSpace.Pack (U × V) (prod_UniformSpace_mixin U V) (U × V).

Section prod_ModuleSpace.

Context {K : Ring} {U V : ModuleSpace K}.

Definition prod_scal (x : K) (u : U × V) :=
  (scal x (fst u), scal x (snd u)).

Lemma prod_scal_assoc :
   (x y : K) (u : U × V),
  prod_scal x (prod_scal y u) = prod_scal (mult x y) u.

Lemma prod_scal_one :
   u : U × V,
  prod_scal one u = u.

Lemma prod_scal_distr_l :
   (x : K) (u v : U × V),
  prod_scal x (prod_plus u v) = prod_plus (prod_scal x u) (prod_scal x v).

Lemma prod_scal_distr_r :
   (x y : K) (u : U × V),
  prod_scal (plus x y) u = prod_plus (prod_scal x u) (prod_scal y u).

End prod_ModuleSpace.

Definition prod_ModuleSpace_mixin (K : Ring) (U V : ModuleSpace K) :=
  ModuleSpace.Mixin K _ _ (@prod_scal_assoc K U V) prod_scal_one prod_scal_distr_l prod_scal_distr_r.

Canonical prod_ModuleSpace (K : Ring) (U V : ModuleSpace K) :=
  ModuleSpace.Pack K (U × V) (ModuleSpace.Class _ _ _ (prod_ModuleSpace_mixin K U V)) (U × V).

Canonical prod_NormedModuleAux (K : AbsRing) (U V : NormedModuleAux K) :=
  NormedModuleAux.Pack K (U × V) (NormedModuleAux.Class _ _ (ModuleSpace.class K _) (UniformSpace.class (prod_UniformSpace U V))) (U × V).

Lemma sqrt_plus_sqr :
   x y : R, Rmax (Rabs x) (Rabs y) sqrt (x ^ 2 + y ^ 2) sqrt 2 × Rmax (Rabs x) (Rabs y).

Section prod_NormedModule.

Context {K : AbsRing} {U V : NormedModule K}.

Definition prod_norm (x : U × V) :=
  sqrt (norm (fst x) ^ 2 + norm (snd x) ^ 2).

Lemma prod_norm_triangle :
   x y : U × V,
  prod_norm (plus x y) prod_norm x + prod_norm y.

Lemma prod_norm_scal :
   (l : K) (x : U × V),
  prod_norm (scal l x) abs l × prod_norm x.

Lemma prod_norm_compat1 :
   (x y : U × V) (eps : R),
  prod_norm (minus y x) < eps ball x eps y.

Definition prod_norm_factor :=
  sqrt 2 × Rmax (@norm_factor K U) (@norm_factor K V).

Lemma prod_norm_compat2 :
   (x y : U × V) (eps : posreal),
  ball x eps y
  prod_norm (minus y x) < prod_norm_factor × eps.

Lemma prod_norm_eq_zero :
   x : U × V,
  prod_norm x = 0 x = zero.

End prod_NormedModule.

Definition prod_NormedModule_mixin (K : AbsRing) (U V : NormedModule K) :=
  NormedModule.Mixin K _ (@prod_norm K U V) prod_norm_factor prod_norm_triangle
  prod_norm_scal prod_norm_compat1 prod_norm_compat2 prod_norm_eq_zero.

Canonical prod_NormedModule (K : AbsRing) (U V : NormedModule K) :=
  NormedModule.Pack K (U × V) (NormedModule.Class K (U × V) _ (prod_NormedModule_mixin K U V)) (U × V).

Lemma norm_prod {K : AbsRing}
  {U : NormedModule K} {V : NormedModule K}
  (x : U) (y : V) :
  Rmax (norm x) (norm y) norm (x,y) sqrt 2 × Rmax (norm x) (norm y).

Iterated Products


Fixpoint Tn (n : nat) (T : Type) : Type :=
  match n with
  | Ounit
  | S nprod T (Tn n T)
  end.

Notation "[ x1 , .. , xn ]" := (pair x1 .. (pair xn tt) .. ).

Fixpoint mk_Tn {T} (n : nat) (u : nat T) : Tn n T :=
  match n with
    | O ⇒ (tt : Tn O T)
    | S n(u O, mk_Tn n (fun nu (S n)))
  end.
Fixpoint coeff_Tn {T} {n : nat} (x0 : T) : (Tn n T) nat T :=
  match n with
  | Ofun (_ : Tn O T) (_ : nat) ⇒ x0
  | S n'fun (v : Tn (S n') T) (i : nat) ⇒ match i with
           | Ofst v
           | S icoeff_Tn x0 (snd v) i
           end
  end.
Lemma mk_Tn_bij {T} {n : nat} (x0 : T) (v : Tn n T) :
  mk_Tn n (coeff_Tn x0 v) = v.
Lemma coeff_Tn_bij {T} {n : nat} (x0 : T) (u : nat T) :
   i, (i < n)%nat coeff_Tn x0 (mk_Tn n u) i = u i.
Lemma coeff_Tn_ext {T} {n : nat} (x1 x2 : T) (v1 v2 : Tn n T) :
  v1 = v2 i, (i < n)%nat coeff_Tn x1 v1 i = coeff_Tn x2 v2 i.
Lemma mk_Tn_ext {T} (n : nat) (u1 u2 : nat T) :
  ( i, (i < n)%nat (u1 i) = (u2 i))
     (mk_Tn n u1) = (mk_Tn n u2).



Fixpoint Fn (n : nat) (T U : Type) : Type :=
  match n with
  | OU
  | S nT Fn n T U
  end.


Matrices


Section Matrices.

Context {T : Type}.

Definition matrix (m n : nat) := Tn m (Tn n T).

Definition coeff_mat {m n : nat} (x0 : T) (A : matrix m n) (i j : nat) :=
  coeff_Tn x0 (coeff_Tn (mk_Tn _ (fun _x0)) A i) j.

Definition mk_matrix (m n : nat) (U : nat nat T) : matrix m n :=
  mk_Tn m (fun i ⇒ (mk_Tn n (U i))).

Lemma mk_matrix_bij {m n : nat} (x0 : T) (A : matrix m n) :
  mk_matrix m n (coeff_mat x0 A) = A.

Lemma coeff_mat_bij {m n : nat} (x0 : T) (u : nat nat T) :
   i j, (i < m)%nat (j < n)%nat coeff_mat x0 (mk_matrix m n u) i j = u i j.

Lemma coeff_mat_ext_aux {m n : nat} (x1 x2 : T) (v1 v2 : matrix m n) :
  v1 = v2 i j, (i < m)%nat (j < n)%nat (coeff_mat x1 v1 i j) = (coeff_mat x2 v2 i j).

Lemma coeff_mat_ext {m n : nat} (x0 : T) (v1 v2 : matrix m n) :
  v1 = v2 i j, (coeff_mat x0 v1 i j) = (coeff_mat x0 v2 i j).

Lemma mk_matrix_ext (m n : nat) (u1 u2 : nat nat T) :
  ( i j, (i < m)%nat (j < n)%nat (u1 i j) = (u2 i j))
     (mk_matrix m n u1) = (mk_matrix m n u2).

End Matrices.

Section MatrixMonoid.

Context {G : AbelianMonoid} {m n : nat}.

Definition Mzero := mk_matrix m n (fun i j ⇒ @zero G).

Definition Mplus (A B : @matrix G m n) :=
  mk_matrix m n (fun i jplus (coeff_mat zero A i j) (coeff_mat zero B i j)).

Lemma Mplus_comm :
   A B : @matrix G m n,
  Mplus A B = Mplus B A.

Lemma Mplus_assoc :
   A B C : @matrix G m n,
  Mplus A (Mplus B C) = Mplus (Mplus A B) C.

Lemma Mplus_zero_r :
   A : @matrix G m n,
  Mplus A Mzero = A.

Definition matrix_AbelianMonoid_mixin :=
  AbelianMonoid.Mixin _ _ _ Mplus_comm Mplus_assoc Mplus_zero_r.

Canonical matrix_AbelianMonoid :=