Library Coquelicot.Hierarchy

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/

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.

Require Import Reals mathcomp.ssreflect.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 AbelianGroup 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 x ⇒ P 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
}.

Class ProperFilter {T : Type} (F : (T → Prop) → Prop) := {
  filter_ex : ∀ P, F P → ∃ x, P x ;
  filter_filter :> Filter F
}.

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 P ⇒ F (fun x ⇒ P (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 → Prop ⇒ F (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 x ⇒ x) 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 x ⇒ g (f x)) F H.

Lemma filterlim_ext_loc :
  ∀ {T U F G} {FF : Filter F} (f g : T → U),
  F (fun x ⇒ f 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 x ⇒ g (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_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 x ⇒ h (fst x) (snd x)) (filter_prod G H) I →
  filterlim (fun x ⇒ h (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 x ⇒ h (fst x) (snd x)) (filter_prod G H) I →
  filterlimi (fun x ⇒ h (f x) (g x)) F I.

Restriction of a filter to a domain

Definition within {T : Type} D (F : (T → Prop) → Prop) (P : T → Prop) :=
  F (fun x ⇒ D 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 groups

Module AbelianGroup.

Record mixin_of (G : Type) := Mixin {
  plus : G → G → G ;
  opp : 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 ;
  ax4 : ∀ x, plus x (opp x) = zero
}.

Notation class_of := mixin_of (only parsing).

Section ClassDef.

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

End ClassDef.

Module Exports.

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

End Exports.

End AbelianGroup.

Export AbelianGroup.Exports.

Arithmetic operations

Section AbelianGroup1.

Context {G : AbelianGroup}.

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

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_opp_r :
  ∀ x : G,
  plus x (opp x) = zero.

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

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 Sums.

Context {G : AbelianGroup}.

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 n ⇒ a (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 k ⇒ plus (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 k ⇒ plus (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 i ⇒ sum_n (u i) n) m = sum_n (fun j ⇒ sum_n (fun i ⇒ u i j) m) n.

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 Sums.

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)
}.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.

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 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 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 k ⇒ mult (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 k ⇒ mult 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 k ⇒ mult (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 k ⇒ mult 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%nat ⇒ one
   | S i ⇒ mult 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)
}.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.

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 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 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_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 {
  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 }.
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 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

Section AbsRing_UniformSpace.

Variable K : AbsRing.

Definition AbsRing_ball (x : K) (eps : R) (y : K) := abs (minus y x) < eps.

Lemma AbsRing_ball_center :
  ∀ (x : K) (e : posreal),
  AbsRing_ball x e x.

Lemma AbsRing_ball_sym :
  ∀ (x y : K) (e : R),
  AbsRing_ball x e y → AbsRing_ball y e x.

Lemma AbsRing_ball_triangle :
  ∀ (x y z : K) (e1 e2 : R),
  AbsRing_ball x e1 y → AbsRing_ball y e2 z →
  AbsRing_ball x (e1 + e2) z.

Definition AbsRing_UniformSpace_mixin :=
  UniformSpace.Mixin _ _ AbsRing_ball_center AbsRing_ball_sym AbsRing_ball_triangle.

Canonical AbsRing_UniformSpace :=
  UniformSpace.Pack K AbsRing_UniformSpace_mixin K.

End AbsRing_UniformSpace.

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 _ _ 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 y ⇒ locally 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 y ⇒ not (P y)).

Lemma locally_ex_not :
  ∀ (x : T) (P : T → Prop),
  locally x (fun y ⇒ not (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 x ⇒ ball 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 y ⇒ y ≠ x) (locally x).

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

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 x ⇒ D x ∧ E x).

Lemma open_or :
  ∀ D E : T → Prop,
  open D → open E →
  open (fun x ⇒ D x ∨ E x).

Lemma open_true :
  open (fun x : T ⇒ True).

Lemma open_false :
  open (fun x : T ⇒ False).

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 : T ⇒ D (f x)).

Closed sets in uniform spaces

Section Closed.

Context {T : UniformSpace}.

Definition closed (D : T → Prop) :=
  ∀ x, not (locally x (fun x : T ⇒ not (D x))) → D x.

Lemma open_not :
  ∀ D : T → Prop,
  closed D → open (fun x ⇒ not (D x)).

Lemma closed_not :
  ∀ D : T → Prop,
  open D → closed (fun x ⇒ not (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 x ⇒ D x ∧ E x).

Lemma closed_true :
  closed (fun x : T ⇒ True).

Lemma closed_false :
  closed (fun x : T ⇒ False).

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 : T ⇒ D (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 x ⇒ D (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)
}.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.

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},
  (∀ eps : posreal, ∃ x, F (ball x eps)) ↔
  (∀ 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_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 P ⇒ F (fun g ⇒ P (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)
}.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.

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 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 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 k ⇒ scal 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 k ⇒ scal a (u k)) n = scal a (sum_n u n).

End ModuleSpace1.

Rings are modules

Section Ring_ModuleSpace.

Variable (K : Ring).

Definition Ring_ModuleSpace_mixin :=
  ModuleSpace.Mixin K _ _ mult_assoc mult_one_l mult_distr_l mult_distr_r.

Canonical Ring_ModuleSpace :=
  ModuleSpace.Pack K K (ModuleSpace.Class _ _ _ Ring_ModuleSpace_mixin) K.

End Ring_ModuleSpace.

Section AbsRing_ModuleSpace.

Variable (K : AbsRing).

Definition AbsRing_ModuleSpace_mixin :=
  ModuleSpace.Mixin K _ _ mult_assoc mult_one_l mult_distr_l mult_distr_r.

Canonical AbsRing_ModuleSpace :=
  ModuleSpace.Pack K K (ModuleSpace.Class _ _ _ AbsRing_ModuleSpace_mixin) K.

End AbsRing_ModuleSpace.

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
}.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.

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 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 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)
}.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.

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 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 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_triangle_inv :
  ∀ x y : V,
  Rabs (norm x - norm y) ≤ norm (minus 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.

End NormedModule1.

Section NormedModule2.

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

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

Section AbsRing_NormedModule.

Variable (K : AbsRing).

Canonical AbsRing_NormedModuleAux :=
  NormedModuleAux.Pack K K (NormedModuleAux.Class _ _ (ModuleSpace.class _ (AbsRing_ModuleSpace K)) (UniformSpace.class (AbsRing_UniformSpace K))) K.

Lemma AbsRing_norm_compat2 :
  ∀ (x y : AbsRing_NormedModuleAux) (eps : posreal),
  ball x eps y → abs (minus y x) < 1 × eps.

Definition AbsRing_NormedModule_mixin :=
  NormedModule.Mixin K _ abs 1 abs_triangle abs_mult (fun x y e H ⇒ H) AbsRing_norm_compat2 abs_eq_zero.

Canonical AbsRing_NormedModule :=
  NormedModule.Pack K _ (NormedModule.Class _ _ _ AbsRing_NormedModule_mixin) K.

End AbsRing_NormedModule.

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 × V ⇒ plus (fst z) (snd z)) (filter_prod (locally x) (locally y)) (locally (plus x y)).

Lemma filterlim_scal (k : K) (x : V) :
  filterlim (fun z ⇒ scal (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 : V ⇒ scal k z) (locally x) (locally (scal k x)).
Lemma filterlim_scal_l (k : K) (x : V) :
  filterlim (fun z ⇒ scal 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 z ⇒ mult (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 x ⇒ ball_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)
}.
Definition base2 T (cT : class_of T) : CompleteSpace.class_of T :=
  CompleteSpace.Class _ (base T cT) (mixin T cT).

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.

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 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 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 x ⇒ filterlim 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 x ⇒ filterlimi f F (locally x)) = l.

End CompleteNormedModule1.

Extended Types

Pairs

Section prod_AbelianGroup.

Context {U V : AbelianGroup}.

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

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

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.

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 (U × V) _ _ _ prod_plus_comm prod_plus_assoc prod_plus_zero_r prod_plus_opp_r.

Canonical prod_AbelianGroup (U V : AbelianGroup) :=
  AbelianGroup.Pack (U × V) (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) _ 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
  | O ⇒ unit
  | S n ⇒ prod 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 n ⇒ u (S n)))
  end.
Fixpoint coeff_Tn {T} {n : nat} (x0 : T) : (Tn n T ) → nat → T :=
  match n with
  | O ⇒ fun (_ : Tn O T) (_ : nat) ⇒ x0
  | S n' ⇒ fun (v : Tn (S n') T) (i : nat) ⇒ match i with
           | O ⇒ fst v
           | S i ⇒ coeff_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
  | O ⇒ U
  | S n ⇒ T → 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 MatrixGroup.

Context {G : AbelianGroup} {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 j ⇒ plus (coeff_mat zero A i j) (coeff_mat zero B i j)).

Definition Mopp (A : @matrix G m n) :=
  mk_matrix m n (fun i j ⇒ opp (coeff_mat zero A 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.

Lemma Mplus_opp_r :
  ∀ A : @matrix G m n,
  Mplus A (Mopp A) = Mzero.

Definition matrix_AbelianGroup_mixin :=
  AbelianGroup.Mixin _ _ _ _ Mplus_comm Mplus_assoc Mplus_zero_r Mplus_opp_r.

Canonical matrix_AbelianGroup :=
  AbelianGroup.Pack _ matrix_AbelianGroup_mixin (@matrix G m n).

End MatrixGroup.

Section MatrixRing.

Context {T : Ring}.

Fixpoint Mone_seq i j : T :=
  match i,j with
    | O, O ⇒ one
    | O, S _ | S _, O ⇒ zero
    | S i, S j ⇒ Mone_seq i j end.

Definition Mone {n} : matrix n n :=
  mk_matrix n n Mone_seq.

Lemma Mone_seq_diag :
  ∀ i j : nat, i = j → Mone_seq i j = @one T.
Lemma Mone_seq_not_diag :
  ∀ i j : nat, i ≠ j → Mone_seq i j = @zero T.

Definition Mmult {n m k} (A : @matrix T n m) (B : @matrix T m k) :=
  mk_matrix n k (fun i j ⇒ sum_n (fun l ⇒ mult (coeff_mat zero A i l) (coeff_mat zero B l j)) (pred m)).

Lemma Mmult_assoc {n m k l} :
  ∀ (A : matrix n m) (B : matrix m k) (C : matrix k l),
  Mmult A (Mmult B C) = Mmult (Mmult A B) C.

Lemma Mmult_one_r {m n} :
  ∀ x : matrix m n, Mmult x Mone = x.

Lemma Mmult_one_l {m n} :
  ∀ x : matrix m n, Mmult Mone x = x.

Lemma Mmult_distr_r {m n k} :
  ∀ (A B : @matrix T m n) (C : @matrix T n k),
  Mmult (Mplus A B) C = Mplus (Mmult A C) (Mmult B C).

Lemma Mmult_distr_l {m n k} :
  ∀ (A : @matrix T m n) (B C : @matrix T n k),
  Mmult A (Mplus B C) = Mplus (Mmult A B) (Mmult A C).

Definition matrix_Ring_mixin {n} :=
  Ring.Mixin _ _ _ (@Mmult_assoc n n n n) Mmult_one_r Mmult_one_l Mmult_distr_r Mmult_distr_l.

Canonical matrix_Ring {n} :=
  Ring.Pack (@matrix T n n) (Ring.Class _ _ matrix_Ring_mixin) (@matrix T n n).

Definition matrix_ModuleSpace_mixin {m n} :=
  ModuleSpace.Mixin (@matrix_Ring m) (@matrix_AbelianGroup T m n) Mmult
    Mmult_assoc Mmult_one_l Mmult_distr_l Mmult_distr_r.

Canonical matrix_ModuleSpace {m n} :=
  ModuleSpace.Pack _ (@matrix T m n) (ModuleSpace.Class _ _ _ matrix_ModuleSpace_mixin) (@matrix T m n).

End MatrixRing.

The topology on natural numbers

Definition eventually (P : nat → Prop) :=
∃ N : nat , ∀ n, (N ≤ n)%nat → P n.

Global Instance eventually_filter : ProperFilter eventually.

The topology on real numbers

Definition R_AbelianGroup_mixin :=
  AbelianGroup.Mixin _ _ _ _ Rplus_comm (fun x y z ⇒ sym_eq (Rplus_assoc x y z)) Rplus_0_r Rplus_opp_r.

Canonical R_AbelianGroup :=
  AbelianGroup.Pack _ R_AbelianGroup_mixin R.

Definition R_Ring_mixin :=
  Ring.Mixin _ _ _ (fun x y z ⇒ sym_eq (Rmult_assoc x y z)) Rmult_1_r Rmult_1_l Rmult_plus_distr_r Rmult_plus_distr_l.

Canonical R_Ring :=
  Ring.Pack R (Ring.Class _ _ R_Ring_mixin) R.

Lemma Rabs_m1 :
  Rabs (-1) = 1.

Definition R_AbsRing_mixin :=
  AbsRing.Mixin _ _ Rabs_R0 Rabs_m1 Rabs_triang (fun x y ⇒ Req_le _ _ (Rabs_mult x y)) Rabs_eq_0.

Canonical R_AbsRing :=
  AbsRing.Pack R (AbsRing.Class _ _ R_AbsRing_mixin) R.

Definition R_UniformSpace_mixin :=
  AbsRing_UniformSpace_mixin R_AbsRing.

Canonical R_UniformSpace :=
  UniformSpace.Pack R R_UniformSpace_mixin R.

Definition R_complete_lim (F : (R → Prop) → Prop) : R :=
  Lub_Rbar (fun x : R ⇒ F (ball (x + 1) (mkposreal _ Rlt_0_1))).

Lemma R_complete_ax1 :
  ∀ F : (R → Prop) → Prop,
  ProperFilter' F →
  (∀ eps : posreal, ∃ x : R , F (ball x eps)) →
  ∀ eps : posreal, F (ball (R_complete_lim F) eps).

Lemma R_complete :
  ∀ F : (R → Prop) → Prop,
  ProperFilter F →
  (∀ eps : posreal, ∃ x : R , F (ball x eps)) →
  ∀ eps : posreal, F (ball (R_complete_lim F) eps).

Lemma R_complete_ax2 :
  ∀ F1 F2 : (R → Prop) → Prop,
  filter_le F1 F2 → filter_le F2 F1 →
  R_complete_lim F1 = R_complete_lim F2.

Lemma R_complete_close :
  ∀ F1 F2 : (R → Prop) → Prop,
  filter_le F1 F2 → filter_le F2 F1 →
  close (R_complete_lim F1) (R_complete_lim F2).

Definition R_CompleteSpace_mixin :=
  CompleteSpace.Mixin _ R_complete_lim R_complete R_complete_close.

Canonical R_CompleteSpace :=
  CompleteSpace.Pack R (CompleteSpace.Class _ _ R_CompleteSpace_mixin) R.

Definition R_ModuleSpace_mixin :=
  AbsRing_ModuleSpace_mixin R_AbsRing.

Canonical R_ModuleSpace :=
  ModuleSpace.Pack _ R (ModuleSpace.Class _ _ _ R_ModuleSpace_mixin) R.

Canonical R_NormedModuleAux :=
  NormedModuleAux.Pack _ R (NormedModuleAux.Class _ _ (ModuleSpace.class _ R_ModuleSpace) (UniformSpace.class R_UniformSpace)) R.

Definition R_NormedModule_mixin :=
  AbsRing_NormedModule_mixin R_AbsRing.

Canonical R_NormedModule :=
  NormedModule.Pack _ R (NormedModule.Class _ _ _ R_NormedModule_mixin) R.

Canonical R_CompleteNormedModule :=
  CompleteNormedModule.Pack _ R (CompleteNormedModule.Class R_AbsRing _ (NormedModule.class _ R_NormedModule) R_CompleteSpace_mixin) R.

Definition at_left x := within (fun u : R ⇒ Rlt u x) (locally x).
Definition at_right x := within (fun u : R ⇒ Rlt x u) (locally x).

Global Instance at_right_proper_filter : ∀ (x : R),
  ProperFilter (at_right x).
Global Instance at_left_proper_filter : ∀ (x : R),
  ProperFilter (at_left x).

Lemma sum_n_Reals : ∀ a N, sum_n a N = sum_f_R0 a N.
Lemma sum_n_m_Reals a n m : (n ≤ m)%nat → sum_n_m a n m = sum_f n m a.

Lemma sum_n_m_const (n m : nat) (a : R) :
  sum_n_m (fun _ ⇒ a) n m = INR (S m - n) × a.
Lemma sum_n_const (n : nat) (a : R) :
  sum_n (fun _ ⇒ a) n = INR (S n) × a.

Lemma norm_sum_n_m {K : AbsRing} {V : NormedModule K} (a : nat → V) (n m : nat) :
  norm (sum_n_m a n m) ≤ sum_n_m (fun n ⇒ norm (a n)) n m.

Lemma sum_n_m_le (a b : nat → R) (n m : nat) :
  (∀ k, a k ≤ b k )
  → sum_n_m a n m ≤ sum_n_m b n m.

Lemma pow_n_pow :
  ∀ (x : R) k, pow_n x k = x ^k.

Continuity of norm

Lemma filterlim_norm {K : AbsRing} {V : NormedModule K} :
  ∀ (x : V), filterlim norm (locally x) (locally (norm x)).

Lemma filterlim_norm_zero {U} {K : AbsRing} {V : NormedModule K}
  {F : (U → Prop) → Prop} {FF : Filter F} (f : U → V) :
  filterlim (fun x ⇒ norm (f x)) F (locally 0)
  → filterlim f F (locally (zero (G := V))).

Lemma filterlim_bounded {K : AbsRing} {V : NormedModule K} (a : nat → V) :
  (∃ x, filterlim a eventually (locally x))
→ {M : R | ∀ n, norm (a n) ≤ M}.

Some open sets of R

Lemma open_lt :
  ∀ y : R, open (fun u : R ⇒ u < y).

Lemma open_gt :
  ∀ y : R, open (fun u : R ⇒ y < u).

Lemma open_neq :
  ∀ y : R, open (fun u : R ⇒ u ≠ y).

Some closed sets of R

Lemma closed_le :
  ∀ y : R, closed (fun u : R ⇒ u ≤ y).

Lemma closed_ge :
  ∀ y : R, closed (fun u : R ⇒ y ≤ u).

Lemma closed_eq :
  ∀ y : R, closed (fun u : R ⇒ u = y).

Local properties in R

Lemma locally_interval (P : R → Prop) (x : R) (a b : Rbar) :
  Rbar_lt a x → Rbar_lt x b →
  (∀ (y : R), Rbar_lt a y → Rbar_lt y b → P y ) →
  locally x P.

Topology on R²

Definition locally_2d (P : R → R → Prop) x y :=
  ∃ delta : posreal , ∀ u v, Rabs (u - x) < delta → Rabs (v - y) < delta → P u v.

Lemma locally_2d_locally :
  ∀ P x y,
  locally_2d P x y ↔ locally (x ,y ) (fun z ⇒ P (fst z) (snd z)).

Lemma locally_2d_impl_strong :
  ∀ (P Q : R → R → Prop) x y, locally_2d (fun u v ⇒ locally_2d P u v → Q u v) x y →
  locally_2d P x y → locally_2d Q x y.

Lemma locally_2d_singleton :
  ∀ (P : R → R → Prop) x y, locally_2d P x y → P x y.

Lemma locally_2d_impl :
  ∀ (P Q : R → R → Prop) x y, locally_2d (fun u v ⇒ P u v → Q u v) x y →
  locally_2d P x y → locally_2d Q x y.

Lemma locally_2d_forall :
  ∀ (P : R → R → Prop) x y, (∀ u v, P u v ) → locally_2d P x y.

Lemma locally_2d_and :
  ∀ (P Q : R → R → Prop) x y, locally_2d P x y → locally_2d Q x y →
  locally_2d (fun u v ⇒ P u v ∧ Q u v) x y.

Lemma locally_2d_align :
  ∀ (P Q : R → R → Prop) x y,
  ( ∀ eps : posreal, (∀ u v, Rabs (u - x) < eps → Rabs (v - y) < eps → P u v ) →
    ∀ u v, Rabs (u - x) < eps → Rabs (v - y) < eps → Q u v ) →
  locally_2d P x y → locally_2d Q x y.

Lemma locally_2d_1d_const_x :
  ∀ (P : R → R → Prop) x y,
  locally_2d P x y →
  locally y (fun t ⇒ P x t).

Lemma locally_2d_1d_const_y :
  ∀ (P : R → R → Prop) x y,
  locally_2d P x y →
  locally x (fun t ⇒ P t y).

Lemma locally_2d_1d_strong :
  ∀ (P : R → R → Prop) x y,
  locally_2d P x y →
  locally_2d (fun u v ⇒ ∀ t, 0 ≤ t ≤ 1 →
    locally t (fun z ⇒ locally_2d P (x + z × (u - x )) (y + z × (v - y )))) x y.

Lemma locally_2d_1d :
  ∀ (P : R → R → Prop) x y,
  locally_2d P x y →
  locally_2d (fun u v ⇒ ∀ t, 0 ≤ t ≤ 1 → locally_2d P (x + t × (u - x )) (y + t × (v - y ))) x y.

Lemma locally_2d_ex_dec :
  ∀ P x y,
  (∀ x y, P x y ∨ ¬P x y ) →
  locally_2d P x y →
  {d : posreal | ∀ u v, Rabs (u -x) < d → Rabs (v -y) < d → P u v }.

Some Topology on Rbar

Definition Rbar_locally' (a : Rbar) (P : R → Prop) :=
  match a with
    | Finite a ⇒ locally' a P
    | p_infty ⇒ ∃ M : R , ∀ x, M < x → P x
    | m_infty ⇒ ∃ M : R , ∀ x, x < M → P x
  end.
Definition Rbar_locally (a : Rbar) (P : R → Prop) :=
  match a with
    | Finite a ⇒ locally a P
    | p_infty ⇒ ∃ M : R , ∀ x, M < x → P x
    | m_infty ⇒ ∃ M : R , ∀ x, x < M → P x
  end.

Global Instance Rbar_locally'_filter :
  ∀ x, ProperFilter (Rbar_locally' x).

Global Instance Rbar_locally_filter :
  ∀ x, ProperFilter (Rbar_locally x).

Open sets in Rbar

Lemma open_Rbar_lt :
  ∀ y, open (fun u : R ⇒ Rbar_lt u y).

Lemma open_Rbar_gt :
  ∀ y, open (fun u : R ⇒ Rbar_lt y u).

Lemma open_Rbar_lt' :
  ∀ x y, Rbar_lt x y → Rbar_locally x (fun u ⇒ Rbar_lt u y).

Lemma open_Rbar_gt' :
  ∀ x y, Rbar_lt y x → Rbar_locally x (fun u ⇒ Rbar_lt y u).

Lemma Rbar_locally'_le :
  ∀ x, filter_le (Rbar_locally' x) (Rbar_locally x).

Lemma Rbar_locally'_le_finite :
  ∀ x : R, filter_le (Rbar_locally' x) (locally x).

Some limits on real functions

Definition Rbar_loc_seq (x : Rbar) (n : nat) := match x with
    | Finite x ⇒ x + / (INR n + 1)
    | p_infty ⇒ INR n
    | m_infty ⇒ - INR n
  end.

Lemma filterlim_Rbar_loc_seq :
  ∀ x, filterlim (Rbar_loc_seq x) eventually (Rbar_locally' x).

Lemma continuity_pt_locally :
  ∀ f x,
  continuity_pt f x ↔
  ∀ eps : posreal, locally x (fun u ⇒ Rabs (f u - f x) < eps).

Lemma continuity_pt_locally' :
  ∀ f x,
  continuity_pt f x ↔
  ∀ eps : posreal, locally' x (fun u ⇒ Rabs (f u - f x) < eps).

Lemma continuity_pt_filterlim :
  ∀ (f : R → R) (x : R),
  continuity_pt f x ↔
  filterlim f (locally x) (locally (f x)).

Lemma continuity_pt_filterlim' :
  ∀ f x,
  continuity_pt f x ↔
  filterlim f (locally' x) (locally (f x)).

Lemma locally_pt_comp (P : R → Prop) (f : R → R) (x : R) :
  locally (f x) P → continuity_pt f x →
  locally x (fun x ⇒ P (f x)).