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

Require Import Reals 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 : (TProp) → Prop) := {
  filter_true : F (fun _True) ;
  filter_and : P Q : TProp, F PF QF (fun xP x Q x) ;
  filter_imp : P Q : TProp, ( x, P xQ x) → F PF Q
}.

Class ProperFilter' {T : Type} (F : (TProp) → Prop) := {
  filter_not_empty : not (F (fun _False)) ;
  filter_filter' :> Filter F
}.

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

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

Lemma filter_forall :
   {T : Type} {F} {FF: @Filter T F} (P : TProp),
  ( 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 : (TProp) → Prop) :=
   P, G PF P.

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

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

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

Global Instance filtermap_filter :
   T U (f : TU) (F : (TProp) → Prop),
  Filter FFilter (filtermap f F).

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

Global Instance filtermap_proper_filter :
   T U (f : TU) (F : (TProp) → Prop),
  ProperFilter FProperFilter (filtermap f F).

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

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

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

Lemma filterlim_ext_loc :
   {T U F G} {FF : Filter F} (f g : TU),
  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 : TU),
  ( x, f x = g x) →
  filterlim f F G
  filterlim g F G.

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

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

Specific filters

Filters for pairs

Inductive filter_prod {T U : Type} (F G : _Prop) (P : T × UProp) : Prop :=
  Filter_prod (Q : TProp) (R : UProp) :
    F QG R → ( x y, Q xR yP (x, y)) → filter_prod F G P.

Global Instance filter_prod_filter :
   T U (F : (TProp) → Prop) (G : (UProp) → Prop),
  Filter FFilter GFilter (filter_prod F G).

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

Global Instance filter_prod_proper {T1 T2 : Type}
  {F : (T1Prop) → Prop} {G : (T2Prop) → 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 : TU) (g : TV),
  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 : TU) (g : TV) (h : UVW),
  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.

Restriction of a filter to a domain

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

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

Lemma filter_le_within :
   {T} {F : (TProp) → 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 : TU),
  ( x, D xf x = g x) →
  filterlim f (within D F) G
  filterlim g (within D F) G.

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

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

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

Lemma subset_filter_proper :
   {T F} {FF : Filter F} (dom : TProp),
  ( 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 : GGG ;
  opp : GG ;
  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 }.
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 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 yx = y.
Lemma plus_reg_r :
   r x y : G,
  plus x r = plus y rx = 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 : natG) n m :=
  iter_nat plus zero a n m.
Definition sum_n (a : natG) n :=
  sum_n_m a O n.

Lemma sum_n_m_Chasles (a : natG) (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 : natG) (n : nat) :
  sum_n_m a n n = a n.
Lemma sum_O (a : natG) : sum_n a 0 = a O.
Lemma sum_n_Sm (a : natG) (n m : nat) :
  (n S m)%natsum_n_m a n (S m) = plus (sum_n_m a n m) (a (S m)).
Lemma sum_Sn_m (a : natG) (n m : nat) :
  (n m)%natsum_n_m a n m = plus (a n) (sum_n_m a (S n) m).
Lemma sum_n_m_S (a : natG) (n m : nat) :
  sum_n_m (fun na (S n)) n m = sum_n_m a (S n) (S m).

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

Lemma sum_n_m_zero (a : natG) (n m : nat) :
  (m < n)%natsum_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 : natG) (n m : nat) :
  ( k, (n k m)%nata k = b k) →
  sum_n_m a n m = sum_n_m b n m.
Lemma sum_n_m_ext (a b : natG) 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 : natG) N,
  ( n, (n N)%nata n = b n) →
  sum_n a N = sum_n b N.
Lemma sum_n_ext :
   (a b : natG) N,
  ( n, a n = b n) →
  sum_n a N = sum_n b N.

Lemma sum_n_m_plus :
   (u v : natG) (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 : natG) (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 : natnatG) (m n : nat),
  sum_n (fun isum_n (u i) n) m = sum_n (fun jsum_n (fun iu i j) m) n.

Lemma sum_n_m_sum_n (a:natG) (n m : nat) :
  (n m)%natsum_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 : KKK ;
  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 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 : KKK := 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 : natK) (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 : natK) (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 : natK) (n : nat),
  sum_n (fun kmult (u k) a) n = mult (sum_n u n) a.

Lemma sum_n_mult_l :
  (a : K) (u : natK) (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 : KR ;
  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 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 : KR := 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 : MRMProp ;
  ax1 : x (e : posreal), ball x e x ;
  ax2 : x y e, ball x e yball y e x ;
  ax3 : x y z e1 e2, ball x e1 yball y e2 zball 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 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 yball y e x.

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

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

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 yAbsRing_ball y e x.

Lemma AbsRing_ball_triangle :
   (x y z : K) (e1 e2 : R),
  AbsRing_ball x e1 yAbsRing_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 : TU) (eps : R) (y : TU) :=
   t : T, ball (x t) eps (y t).

Lemma fct_ball_center :
   (x : TU) (e : posreal),
  fct_ball x e x.

Lemma fct_ball_sym :
   (x y : TU) (e : R),
  fct_ball x e yfct_ball y e x.

Lemma fct_ball_triangle :
   (x y z : TU) (e1 e2 : R),
  fct_ball x e1 yfct_ball y e2 zfct_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 (TU) fct_UniformSpace_mixin (TU).

End fct_UniformSpace.

Local predicates

locally_dist

Definition locally_dist {T : Type} (d : TR) (P : TProp) :=
   delta : posreal, y, d y < deltaP y.

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

locally

Section Locally.

Context {T : UniformSpace}.

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

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

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

Lemma locally_singleton :
   (x : T) (P : TProp),
  locally x PP x.

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

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

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

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

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

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

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

Lemma is_filter_lim_close {F} {FF : ProperFilter F} (x y : T) :
  is_filter_lim F xis_filter_lim F y eps : posreal, ball x eps y.

Lemma is_filter_lim_locally_close (x y : T) :
  is_filter_lim (locally x) y eps : posreal, ball x eps y.

End Locally.

Lemma filterlim_const :
   {T} {U : UniformSpace} {F : (TProp) → 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 : TU) y,
  filterlim f F (locally y)
   eps : posreal, F (fun xball y eps (f x)).

Lemma filterlim_locally_close:
   {F} {FF: ProperFilter F} (f : TU) l l',
  filterlim f F (locally l) → filterlim f F (locally l') →
   eps : posreal, ball l eps l'.

End Locally_fct.

Lemma is_filter_lim_filtermap {T: UniformSpace} {U : UniformSpace} :
F x (f : TU),
  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).

Pointed filter

Section at_point.

Context {T : UniformSpace}.

Definition at_point (a : T) (P : TProp) : Prop :=
   y, ( eps : posreal, ball a eps y) → P y.
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 : TProp) :=
   x, D xlocally x D.

Lemma locally_open :
   (D E : TProp),
  open D
  ( x : T, D xE x) →
   x : T, D x
  locally x E.

Lemma open_ext :
   D E : TProp,
  ( x, D x E x) →
  open Dopen E.

Lemma open_and :
   D E : TProp,
  open Dopen E
  open (fun xD x E x).

Lemma open_or :
   D E : TProp,
  open Dopen 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 : TU) (D : UProp),
  ( x, D (f x) → filterlim f (locally x) (locally (f x))) →
  open Dopen (fun x : TD (f x)).

Closed sets in uniform spaces


Section Closed.

Context {T : UniformSpace}.

Definition closed (D : TProp) :=
  open (fun x : Tnot (D x)).

Lemma closed_ext :
   D E : TProp,
  ( x, D x E x) →
  closed Dclosed E.

Lemma closed_and :
   D E : TProp,
  closed Dclosed E
  closed (fun xD x E x).

Lemma closed_or :
   D E : TProp,
  closed Dclosed 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 : TU) (D : UProp),
  ( x, filterlim f (locally x) (locally (f x))) →
  closed Dclosed (fun x : TD (f x)).

Complete uniform spaces


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

Module CompleteSpace.

Record mixin_of (T : UniformSpace) := Mixin {
  lim : ((TProp) → Prop) → T ;
  ax1 : F, ProperFilter Fcauchy F eps : posreal, F (ball (lim F) eps)
}.

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 : ((TProp) → Prop) → T := CompleteSpace.lim _ (CompleteSpace.class T).

Lemma complete_cauchy :
   F : (TProp) → Prop,
  ProperFilter Fcauchy F
   eps : posreal,
  F (ball (lim F) eps).

Definition iota (P : TProp) := lim (fun A ⇒ ( x, P xA x)).

Lemma iota_correct_weak :
   P : TProp,
  ( x y, P xP y eps : posreal, ball x eps y) →
   x, P x eps : posreal, ball (iota P) eps x.

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 uP vball u eps v).

Section fct_CompleteSpace.

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

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

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

Lemma complete_cauchy_fct :
   (F : ((TU) → Prop) → Prop),
  ProperFilter F
  ( eps : posreal, f : TU, F (ball f eps)) →
   eps : posreal, F (ball (lim_fct F) eps).

Definition fct_CompleteSpace_mixin :=
  CompleteSpace.Mixin _ lim_fct complete_cauchy_fct.

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

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 : T1T2U) 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 : T1T2U) 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 : T1T2U) 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 : T2Prop) (HF2 : P, F2 P x, dom x P x)
  (f : T1T2U) 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 : KVV ;
  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 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 : KVV := 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 : natV) (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 : natV) (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 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 : VR ;
  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) < epsball x eps y ;
  ax4 : (x y : V) (eps : posreal), ball x eps ynorm (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 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 : VR := 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) < epsball x eps y.

Lemma norm_compat2 :
   (x y : V) (eps : posreal), ball x eps ynorm (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 ball_eq :
   x y : V,
  ( eps : posreal, ball x eps y) → x = y.

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

Definition locally_norm (x : V) (P : VProp) :=
   eps : posreal, y, ball_norm x eps yP 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 yball_norm y e2 zball_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 yball_norm y eps x.

Lemma ball_norm_le :
   (x : V) (e1 e2 : posreal), e1 e2
   y, ball_norm x e1 yball_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 xis_filter_lim F yx = y.

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

End NormedModule1.

Section NormedModule2.

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

Lemma filterlim_locally_unique :
   {F} {FF : ProperFilter' F} (f : TV) (x y : V),
  filterlim f F (locally x) → filterlim 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 : (TProp) → Prop} {FF : Filter F} (f : TU) (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 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 {T : Type} {K : AbsRing} {V : CompleteNormedModule K}.

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

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 yprod_ball y eps x.

Lemma prod_ball_triangle :
   (x y z : U × V) (e1 e2 : R),
  prod_ball x e1 yprod_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) < epsball 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 : natT) : 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) → natT :=
  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 : natT) :
   i, (i < n)%natcoeff_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)%natcoeff_Tn x1 v1 i = coeff_Tn x2 v2 i.
Lemma mk_Tn_ext {T} (n : nat) (u1 u2 : natT) :
  ( 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 nTFn 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 : natnatT) : 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 : natnatT) :
   i j, (i < m)%nat → (j < n)%natcoeff_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 : natnatT) :
  ( 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 jplus (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 jopp (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, Oone
    | O, S _ | S _, Ozero
    | S i, S jMone_seq i j end.

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

Lemma Mone_seq_diag :
   i j : nat, i = jMone_seq i j = @one T.
Lemma Mone_seq_not_diag :
   i j : nat, i jMone_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 jsum_n (fun lmult (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 : natProp) :=
   N : nat, n, (N n)%natP n.

Global Instance eventually_filter : ProperFilter eventually.

The topology on real numbers


Definition R_AbelianGroup_mixin :=
  AbelianGroup.Mixin _ _ _ _ Rplus_comm (fun x y zsym_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 zsym_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 yReq_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 : (RProp) → Prop) : R :=
  Lub_Rbar (fun x : RF (ball (x + 1) (mkposreal _ Rlt_0_1))).

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

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

Definition R_CompleteSpace_mixin :=
  CompleteSpace.Mixin _ R_complete_lim R_complete.

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 : RRlt u x) (locally x).
Definition at_right x := within (fun u : RRlt 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)%natsum_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 : natV) (n m : nat) :
  norm (sum_n_m a n m) sum_n_m (fun nnorm (a n)) n m.

Lemma sum_n_m_le (a b : natR) (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 : (UProp) → Prop} {FF : Filter F} (f : UV) :
  filterlim (fun xnorm (f x)) F (locally 0)
  → filterlim f F (locally (zero (G := V))).

Lemma filterlim_bounded {K : AbsRing} {V : NormedModule K} (a : natV) :
  ( 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 : Ru < y).

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

Lemma open_neq :
   y : R, open (fun u : Ru y).

Local properties in R

Lemma locally_interval (P : RProp) (x : R) (a b : Rbar) :
  Rbar_lt a xRbar_lt x b
  ( (y : R), Rbar_lt a yRbar_lt y bP y) →
  locally x P.

Topology on R²


Definition locally_2d (P : RRProp) x y :=
   delta : posreal, u v, Rabs (u - x) < deltaRabs (v - y) < deltaP u v.

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

Lemma locally_2d_impl_strong :
   (P Q : RRProp) x y, locally_2d (fun u vlocally_2d P u vQ u v) x y
  locally_2d P x ylocally_2d Q x y.

Lemma locally_2d_singleton :
   (P : RRProp) x y, locally_2d P x yP x y.

Lemma locally_2d_impl :
   (P Q : RRProp) x y, locally_2d (fun u vP u vQ u v) x y
  locally_2d P x ylocally_2d Q x y.

Lemma locally_2d_forall :
   (P : RRProp) x y, ( u v, P u v) → locally_2d P x y.

Lemma locally_2d_and :
   (P Q : RRProp) x y, locally_2d P x ylocally_2d Q x y
  locally_2d (fun u vP u v Q u v) x y.

Lemma locally_2d_align :
   (P Q : RRProp) x y,
  ( eps : posreal, ( u v, Rabs (u - x) < epsRabs (v - y) < epsP u v) →
     u v, Rabs (u - x) < epsRabs (v - y) < epsQ u v ) →
  locally_2d P x ylocally_2d Q x y.

Lemma locally_2d_1d_const_x :
   (P : RRProp) x y,
  locally_2d P x y
  locally y (fun tP x t).

Lemma locally_2d_1d_const_y :
   (P : RRProp) x y,
  locally_2d P x y
  locally x (fun tP t y).

Lemma locally_2d_1d_strong :
   (P : RRProp) x y,
  locally_2d P x y
  locally_2d (fun u v t, 0 t 1 →
    locally t (fun zlocally_2d P (x + z × (u - x)) (y + z × (v - y)))) x y.

Lemma locally_2d_1d :
   (P : RRProp) 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) < dRabs (v-y) < dP u v}.

Some Topology on Rbar


Definition Rbar_locally' (a : Rbar) (P : RProp) :=
  match a with
    | Finite alocally' a P
    | p_infty M : R, x, M < xP x
    | m_infty M : R, x, x < MP x
  end.
Definition Rbar_locally (a : Rbar) (P : RProp) :=
  match a with
    | Finite alocally a P
    | p_infty M : R, x, M < xP x
    | m_infty M : R, x, x < MP 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 : RRbar_lt u y).

Lemma open_Rbar_gt :
   y, open (fun u : RRbar_lt y u).

Lemma open_Rbar_lt' :
   x y, Rbar_lt x yRbar_locally x (fun uRbar_lt u y).

Lemma open_Rbar_gt' :
   x y, Rbar_lt y xRbar_locally x (fun uRbar_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 xx + / (INR n + 1)
    | p_inftyINR 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 uRabs (f u - f x) < eps).

Lemma continuity_pt_locally' :
   f x,
  continuity_pt f x
   eps : posreal, locally' x (fun uRabs (f u - f x) < eps).

Lemma continuity_pt_filterlim :
   (f : RR) (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 : RProp) (f : RR) (x : R) :
  locally (f x) Pcontinuity_pt f x
  locally x (fun xP (f x)).