Library Coquelicot.Hierarchy
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2017 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2017 Guillaume Melquiond
This file first describes Filters that are predicates of type
(T → Prop) → Prop used for limits and neighborhoods. Then the
algebraic hierarchy of the Coquelicot library is given: from the
AbelianMonoid to the CompleteNormedModule. Topologies on R and
R×R are also given.
More documentation details can be found in Coquelicot.html.
More documentation details can be found in Coquelicot.html.
Open Scope R_scope.
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
}.
#[global] Existing Instance filter_filter'.
Class ProperFilter {T : Type} (F : (T → Prop) → Prop) := {
filter_ex : ∀ P, F P → ∃ x, P x ;
filter_filter : Filter F
}.
#[global] Existing Instance filter_filter.
Global Instance Proper_StrongProper :
∀ {T : Type} (F : (T → Prop) → Prop),
ProperFilter F → ProperFilter' F.
Lemma filter_forall :
∀ {T : Type} {F} {FF: @Filter T F} (P : T → Prop),
(∀ x, P x) → F P.
Lemma filter_const :
∀ {T : Type} {F} {FF: @ProperFilter T F} (P : Prop),
F (fun _ ⇒ P) → P.
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_lim_ext_loc :
∀ {T U F G} {FF : Filter F} (f : T → U) (g : T → U → Prop),
F (fun x ⇒ g x (f x)) →
filterlim f F G →
filterlimi g F G.
Lemma filterlimi_lim_ext :
∀ {T U F G} {FF : Filter F} (f : T → U) (g : T → U → Prop),
(∀ x, g x (f x)) →
filterlim f F G →
filterlimi g F G.
Lemma filterlimi_filter_le_1 :
∀ {T U F G H} (f : T → U → Prop),
filter_le G F →
filterlimi f F H →
filterlimi f G H.
Lemma filterlimi_filter_le_2 :
∀ {T U F G H} (f : T → U → Prop),
filter_le G H →
filterlimi f F G →
filterlimi f F H.
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.
Lemma prod_filtermap_le {T1 T2 U1 U2 F G} {FF : Filter F} {FG : Filter G}
(f1 : T1 → U1) (f2 : T2 → U2) :
filter_le (filter_prod (filtermap f1 F) (filtermap f2 G))
(filtermap (fun x ⇒ (f1 (fst x), f2 (snd x))) (filter_prod F G)).
Lemma filtermap_prod_le {T1 T2 U1 U2 F G} {FF : Filter F} {FG : Filter G}
(f1 : T1 → U1) (f2 : T2 → U2) :
filter_le (filtermap (fun x ⇒ (f1 (fst x), f2 (snd x))) (filter_prod F G))
(filter_prod (filtermap f1 F) (filtermap f2 G)).
Lemma filterlim_prod {E} {T} {U} {F : (T → Prop) → Prop} {FF : Filter F} (g : E → U → U → Prop) (f : T → U) :
filterlim (fun x ⇒ (f (fst x), f (snd x))) (filter_prod F F) (fun P ⇒ ∃ e, ∀ u v, g e u v → P (u, v)) ↔
(∀ e, ∃ P, F P ∧ ∀ u v : T, P u → P v → g e (f u) (f v)).
Restriction of a filter to a domain
Definition within {T : Type} D (F : (T → Prop) → Prop) (P : T → Prop) :=
F (fun 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).
Module AbelianMonoid.
Record mixin_of (G : Type) := Mixin {
plus : G → G → G ;
zero : G ;
ax1 : ∀ x y, plus x y = plus y x ;
ax2 : ∀ x y z, plus x (plus y z) = plus (plus x y) z ;
ax3 : ∀ x, plus x zero = x ;
}.
Notation class_of := mixin_of (only parsing).
Section ClassDef.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Definition class (cT : type) := let: Pack _ c _ := cT return class_of cT in c.
End ClassDef.
Module Exports.
Coercion sort : type >-> Sortclass.
Notation AbelianMonoid := type.
End Exports.
End AbelianMonoid.
Export AbelianMonoid.Exports.
Arithmetic operations
Section AbelianMonoid1.
Context {G : AbelianMonoid}.
Definition zero := AbelianMonoid.zero _ (AbelianMonoid.class G).
Definition plus := AbelianMonoid.plus _ (AbelianMonoid.class G).
Lemma plus_comm :
∀ x y : G,
plus x y = plus y x.
Lemma plus_assoc :
∀ x y z : G,
plus x (plus y z) = plus (plus x y) z.
Lemma plus_zero_r :
∀ x : G,
plus x zero = x.
Lemma plus_zero_l :
∀ x : G,
plus zero x = x.
End AbelianMonoid1.
Sum
Section Sums1.
Context {G : AbelianMonoid}.
Definition sum_n_m (a : nat → G) n m :=
iter_nat plus zero a n m.
Definition sum_n (a : nat → G) n :=
sum_n_m a O n.
Lemma sum_n_m_Chasles (a : nat → G) (n m k : nat) :
(n ≤ S m)%nat → (m ≤ k)%nat
→ sum_n_m a n k = plus (sum_n_m a n m) (sum_n_m a (S m) k).
Lemma sum_n_n (a : nat → G) (n : nat) :
sum_n_m a n n = a n.
Lemma sum_O (a : nat → G) : sum_n a 0 = a O.
Lemma sum_n_Sm (a : nat → G) (n m : nat) :
(n ≤ S m)%nat → sum_n_m a n (S m) = plus (sum_n_m a n m) (a (S m)).
Lemma sum_Sn_m (a : nat → G) (n m : nat) :
(n ≤ m)%nat → sum_n_m a n m = plus (a n) (sum_n_m a (S n) m).
Lemma sum_n_m_S (a : nat → G) (n m : nat) :
sum_n_m (fun 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.
End Sums1.
Module AbelianGroup.
Record mixin_of (G : AbelianMonoid) := Mixin {
opp : G → G ;
ax1 : ∀ x, plus x (opp x) = zero
}.
Section ClassDef.
Record class_of (G : Type) := Class {
base : AbelianMonoid.class_of G ;
mixin : mixin_of (AbelianMonoid.Pack _ base G)
}.
Local Coercion base : class_of >-> AbelianMonoid.class_of.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable cT : type.
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> AbelianMonoid.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Notation AbelianGroup := type.
End Exports.
End AbelianGroup.
Export AbelianGroup.Exports.
Arithmetic operations
Section AbelianGroup1.
Context {G : AbelianGroup}.
Definition opp := AbelianGroup.opp _ (AbelianGroup.class G).
Definition minus x y := (plus x (opp y)).
Lemma plus_opp_r :
∀ x : G,
plus x (opp x) = zero.
Lemma plus_opp_l :
∀ x : G,
plus (opp x) x = zero.
Lemma opp_zero :
opp zero = zero.
Lemma minus_zero_r :
∀ x : G,
minus x zero = x.
Lemma minus_eq_zero (x : G) :
minus x x = zero.
Lemma plus_reg_l :
∀ r x y : G,
plus r x = plus r y → x = y.
Lemma plus_reg_r :
∀ r x y : G,
plus x r = plus y r → x = y.
Lemma opp_opp :
∀ x : G,
opp (opp x) = x.
Lemma opp_plus :
∀ x y : G,
opp (plus x y) = plus (opp x) (opp y).
Lemma opp_minus (x y : G) :
opp (minus x y) = minus y x.
Lemma minus_trans (r x y : G) :
minus x y = plus (minus x r) (minus r y).
End AbelianGroup1.
Sum
Section Sums2.
Context {G : AbelianGroup}.
Lemma sum_n_m_sum_n (a:nat → G) (n m : nat) :
(n ≤ m)%nat → sum_n_m a (S n) m = minus (sum_n a m) (sum_n a n).
End Sums2.
Module Ring.
Record mixin_of (K : AbelianGroup) := Mixin {
mult : K → K → K ;
one : K ;
ax1 : ∀ x y z, mult x (mult y z) = mult (mult x y) z ;
ax2 : ∀ x, mult x one = x ;
ax3 : ∀ x, mult one x = x ;
ax4 : ∀ x y z, mult (plus x y) z = plus (mult x z) (mult y z) ;
ax5 : ∀ x y z, mult x (plus y z) = plus (mult x y) (mult x z)
}.
Section ClassDef.
Record class_of (K : Type) := Class {
base : AbelianGroup.class_of K ;
mixin : mixin_of (AbelianGroup.Pack _ base K)
}.
Local Coercion base : class_of >-> AbelianGroup.class_of.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable cT : type.
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> AbelianGroup.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Notation Ring := type.
End Exports.
End Ring.
Export Ring.Exports.
Arithmetic operations
Section Ring1.
Context {K : Ring}.
Definition mult : K → K → K := Ring.mult _ (Ring.class K).
Definition one : K := Ring.one _ (Ring.class K).
Lemma mult_assoc :
∀ x y z : K,
mult x (mult y z) = mult (mult x y) z.
Lemma mult_one_r :
∀ x : K,
mult x one = x.
Lemma mult_one_l :
∀ x : K,
mult one x = x.
Lemma mult_distr_r :
∀ x y z : K,
mult (plus x y) z = plus (mult x z) (mult y z).
Lemma mult_distr_l :
∀ x y z : K,
mult x (plus y z) = plus (mult x y) (mult x z).
Lemma mult_zero_r :
∀ x : K,
mult x zero = zero.
Lemma mult_zero_l :
∀ x : K,
mult zero x = zero.
Lemma opp_mult_r :
∀ x y : K,
opp (mult x y) = mult x (opp y).
Lemma opp_mult_l :
∀ x y : K,
opp (mult x y) = mult (opp x) y.
Lemma opp_mult_m1 :
∀ x : K,
opp x = mult (opp one) x.
Lemma sum_n_m_mult_r :
∀ (a : K) (u : nat → K) (n m : nat),
sum_n_m (fun 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.
Module AbsRing.
Record mixin_of (K : Ring) := Mixin {
abs : K → R ;
ax1 : abs zero = 0 ;
ax2 : abs (opp one) = 1 ;
ax3 : ∀ x y : K, abs (plus x y) ≤ abs x + abs y ;
ax4 : ∀ x y : K, abs (mult x y) ≤ abs x × abs y ;
ax5 : ∀ x : K, abs x = 0 → x = zero
}.
Section ClassDef.
Record class_of (K : Type) := Class {
base : Ring.class_of K ;
mixin : mixin_of (Ring.Pack _ base K)
}.
Local Coercion base : class_of >-> Ring.class_of.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable cT : type.
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition Ring := Ring.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> Ring.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion Ring : type >-> Ring.type.
Canonical Ring.
Notation AbsRing := type.
End Exports.
End AbsRing.
Export AbsRing.Exports.
Usual properties
Section AbsRing1.
Context {K : AbsRing}.
Definition abs : K → R := AbsRing.abs _ (AbsRing.class K).
Lemma abs_zero :
abs zero = 0.
Lemma abs_opp_one :
abs (opp one) = 1.
Lemma abs_triangle :
∀ x y : K,
abs (plus x y) ≤ abs x + abs y.
Lemma abs_mult :
∀ x y : K,
abs (mult x y) ≤ abs x × abs y.
Lemma abs_eq_zero :
∀ x : K,
abs x = 0 → x = zero.
Lemma abs_opp :
∀ x, abs (opp x) = abs x.
Lemma abs_minus :
∀ x y : K, abs (minus x y) = abs (minus y x).
Lemma abs_one :
abs one = 1.
Lemma abs_ge_0 :
∀ x, 0 ≤ abs x.
Lemma abs_gt_0 :
∀ x : K,
x ≠ zero → 0 < abs x.
Lemma abs_minus_gt_0 :
∀ x y : K,
x ≠ y → 0 < abs (minus x y).
Lemma abs_pow_n :
∀ (x : K) n,
abs (pow_n x n) ≤ (abs x)^n.
End AbsRing1.
Module UniformSpace.
Record mixin_of (M : Type) := Mixin {
point_of : M ;
ball : M → R → M → Prop ;
ax1 : ∀ x (e : posreal), ball x e x ;
ax2 : ∀ x y e, ball x e y → ball y e x ;
ax3 : ∀ x y z e1 e2, ball x e1 y → ball y e2 z → ball x (e1 + e2) z
}.
Notation class_of := mixin_of (only parsing).
Section ClassDef.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Definition class (cT : type) := let: Pack _ c _ := cT return class_of cT in c.
End ClassDef.
Module Exports.
Coercion sort : type >-> Sortclass.
Notation UniformSpace := type.
End Exports.
End UniformSpace.
Export UniformSpace.Exports.
Section UniformSpace1.
Context {M : UniformSpace}.
Definition point_of := UniformSpace.point_of _ (UniformSpace.class M).
Definition ball := UniformSpace.ball _ (UniformSpace.class M).
Lemma ball_center :
∀ (x : M) (e : posreal),
ball x e x.
Lemma ball_sym :
∀ (x y : M) (e : R),
ball x e y → ball y e x.
Lemma ball_triangle :
∀ (x y z : M) (e1 e2 : R),
ball x e1 y → ball y e2 z → ball x (e1 + e2) z.
Lemma ball_le :
∀ (x : M) (e1 e2 : R), e1 ≤ e2 →
∀ (y : M), ball x e1 y → ball x e2 y.
Definition close (x y : M) : Prop := ∀ eps : posreal, ball x eps y.
Lemma close_refl (x : M) : close x x.
Lemma close_sym (x y : M) : close x y → close y x.
Lemma close_trans (x y z : M) : close x y → close y z → close x z.
End UniformSpace1.
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 _ zero _ 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 _ (fun _ ⇒ point_of) _ fct_ball_center fct_ball_sym fct_ball_triangle.
Canonical fct_UniformSpace :=
UniformSpace.Pack (T → U) fct_UniformSpace_mixin (T → U).
End fct_UniformSpace.
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).
closely
Section closely.
Context {T : UniformSpace}.
Definition closely (P : T × T → Prop) :=
∃ eps : posreal, ∀ u v : T, ball u eps v → P (u, v).
Global Instance closely_filter :
ProperFilter closely.
End closely.
Lemma filterlim_closely {T} {U : UniformSpace} {F : (T → Prop) → Prop} {FF : Filter F} (f : T → U) :
filterlim (fun x ⇒ (f (fst x), f (snd x))) (filter_prod F F) closely ↔
(∀ eps : posreal, ∃ P, F P ∧ ∀ u v : T, P u → P v → ball (f u) eps (f v)).
Pointed filter
Section at_point.
Context {T : UniformSpace}.
Definition at_point (a : T) (P : T → Prop) : Prop := P a.
Global Instance at_point_filter (a : T) :
ProperFilter (at_point a).
End at_point.
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)).
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.
Definition cauchy {T : UniformSpace} (F : (T → Prop) → Prop) :=
∀ eps : posreal, ∃ x, F (ball x eps).
Module CompleteSpace.
Record mixin_of (T : UniformSpace) := Mixin {
lim : ((T → Prop) → Prop) → T ;
ax1 : ∀ F, ProperFilter F → cauchy F → ∀ eps : posreal, F (ball (lim F) eps) ;
ax2 : ∀ F1 F2, filter_le F1 F2 → filter_le F2 F1 → close (lim F1) (lim F2)
}.
Section ClassDef.
Record class_of (T : Type) := Class {
base : UniformSpace.class_of T ;
mixin : mixin_of (UniformSpace.Pack _ base T)
}.
Local Coercion base : class_of >-> UniformSpace.class_of.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable cT : type.
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition UniformSpace := UniformSpace.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> UniformSpace.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Notation CompleteSpace := type.
End Exports.
End CompleteSpace.
Export CompleteSpace.Exports.
Section CompleteSpace1.
Context {T : CompleteSpace}.
Definition lim : ((T → Prop) → Prop) → T := CompleteSpace.lim _ (CompleteSpace.class T).
Lemma complete_cauchy :
∀ F : (T → Prop) → Prop,
ProperFilter F → cauchy F →
∀ eps : posreal,
F (ball (lim F) eps).
Lemma close_lim :
∀ F1 F2 : (T → Prop) → Prop,
filter_le F1 F2 → filter_le F2 F1 →
close (lim F1) (lim F2).
Definition iota (P : T → Prop) := lim (fun A ⇒ (∀ x, P x → A x)).
Lemma iota_correct_weak :
∀ P : T → Prop,
(∀ x y, P x → P y → close x y) →
∀ x, P x → close (iota P) x.
Lemma close_iota :
∀ P Q : T → Prop,
(∀ x, P x ↔ Q x) →
close (iota P) (iota Q).
End CompleteSpace1.
Lemma cauchy_distance' :
∀ {T : UniformSpace} {F} {FF : ProperFilter F},
cauchy F ↔ filter_le (filter_prod F F) (@closely T).
Lemma cauchy_distance :
∀ {T : UniformSpace} {F} {FF : ProperFilter F},
cauchy F ↔
(∀ eps : posreal, ∃ P, F P ∧ ∀ u v : T, P u → P v → ball u eps v).
Section fct_CompleteSpace.
Context {T : Type} {U : CompleteSpace}.
Lemma filterlim_locally_closely :
∀ {F} {FF : ProperFilter F} (f : T → U),
filterlim (fun x ⇒ (f (fst x), f (snd x))) (filter_prod F F) closely ↔
∃ y, filterlim f F (locally y).
Lemma filterlim_locally_cauchy :
∀ {F} {FF : ProperFilter F} (f : T → U),
(∀ eps : posreal, ∃ P, F P ∧ ∀ u v : T, P u → P v → ball (f u) eps (f v)) ↔
∃ y, filterlim f F (locally y).
Lemma filterlimi_locally_cauchy :
∀ {F} {FF : ProperFilter F} (f : T → U → Prop),
F (fun x ⇒ (∃ y, f x y) ∧
(∀ y1 y2, f x y1 → f x y2 → y1 = y2)) →
((∀ eps : posreal, ∃ P, F P ∧
∀ u v : T, P u → P v → ∀ u' v': U, f u u' → f v v' → ball u' eps v') ↔
∃ y, filterlimi f F (locally y)).
Definition lim_fct (F : ((T → U) → Prop) → Prop) (t : T) :=
lim (fun 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.
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).
Module ModuleSpace.
Record mixin_of (K : Ring) (V : AbelianGroup) := Mixin {
scal : K → V → V ;
ax1 : ∀ x y u, scal x (scal y u) = scal (mult x y) u ;
ax2 : ∀ u, scal one u = u ;
ax3 : ∀ x u v, scal x (plus u v) = plus (scal x u) (scal x v) ;
ax4 : ∀ x y u, scal (plus x y) u = plus (scal x u) (scal y u)
}.
Section ClassDef.
Variable K : Ring.
Record class_of (V : Type) := Class {
base : AbelianGroup.class_of V ;
mixin : mixin_of K (AbelianGroup.Pack _ base V)
}.
Local Coercion base : class_of >-> AbelianGroup.class_of.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable cT : type.
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> AbelianGroup.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Notation ModuleSpace := type.
End Exports.
End ModuleSpace.
Export ModuleSpace.Exports.
Section ModuleSpace1.
Context {K : Ring} {V : ModuleSpace K}.
Definition scal : K → V → V := ModuleSpace.scal _ _ (ModuleSpace.class K V).
Lemma scal_assoc :
∀ (x y : K) (u : V),
scal x (scal y u) = scal (mult x y) u.
Lemma scal_one :
∀ (u : V), scal one u = u.
Lemma scal_distr_l :
∀ (x : K) (u v : V),
scal x (plus u v) = plus (scal x u) (scal x v).
Lemma scal_distr_r :
∀ (x y : K) (u : V),
scal (plus x y) u = plus (scal x u) (scal y u).
Lemma scal_zero_r :
∀ x : K,
scal x zero = zero.
Lemma scal_zero_l :
∀ u : V,
scal zero u = zero.
Lemma scal_opp_l :
∀ (x : K) (u : V),
scal (opp x) u = opp (scal x u).
Lemma scal_opp_r :
∀ (x : K) (u : V),
scal x (opp u) = opp (scal x u).
Lemma scal_opp_one :
∀ u : V,
scal (opp one) u = opp u.
Lemma scal_minus_distr_l (x : K) (u v : V) :
scal x (minus u v) = minus (scal x u) (scal x v).
Lemma scal_minus_distr_r (x y : K) (u : V) :
scal (minus x y) u = minus (scal x u) (scal y u).
Lemma sum_n_m_scal_l :
∀ (a : K) (u : nat → V) (n m : nat),
sum_n_m (fun 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.
Module NormedModuleAux.
Section ClassDef.
Variable K : AbsRing.
Record class_of (T : Type) := Class {
base : ModuleSpace.class_of K T ;
mixin : UniformSpace.mixin_of T
}.
Local Coercion base : class_of >-> ModuleSpace.class_of.
Local Coercion mixin : class_of >-> UniformSpace.class_of.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable cT : type.
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition ModuleSpace := ModuleSpace.Pack _ cT xclass xT.
Definition UniformSpace := UniformSpace.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> ModuleSpace.class_of.
Coercion mixin : class_of >-> UniformSpace.class_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion ModuleSpace : type >-> ModuleSpace.type.
Canonical ModuleSpace.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Notation NormedModuleAux := type.
End Exports.
End NormedModuleAux.
Export NormedModuleAux.Exports.
Module NormedModule.
Record mixin_of (K : AbsRing) (V : NormedModuleAux K) := Mixin {
norm : V → R ;
norm_factor : R ;
ax1 : ∀ (x y : V), norm (plus x y) ≤ norm x + norm y ;
ax2 : ∀ (l : K) (x : V), norm (scal l x) ≤ abs l × norm x ;
ax3 : ∀ (x y : V) (eps : R), norm (minus y x) < eps → ball x eps y ;
ax4 : ∀ (x y : V) (eps : posreal), ball x eps y → norm (minus y x) < norm_factor × eps ;
ax5 : ∀ x : V, norm x = 0 → x = zero
}.
Section ClassDef.
Variable K : AbsRing.
Record class_of (T : Type) := Class {
base : NormedModuleAux.class_of K T ;
mixin : mixin_of K (NormedModuleAux.Pack K T base T)
}.
Local Coercion base : class_of >-> NormedModuleAux.class_of.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable cT : type.
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition ModuleSpace := ModuleSpace.Pack _ cT xclass xT.
Definition UniformSpace := UniformSpace.Pack cT xclass xT.
Definition NormedModuleAux := NormedModuleAux.Pack _ cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> NormedModuleAux.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion ModuleSpace : type >-> ModuleSpace.type.
Canonical ModuleSpace.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Coercion NormedModuleAux : type >-> NormedModuleAux.type.
Canonical NormedModuleAux.
Notation NormedModule := type.
End Exports.
End NormedModule.
Export NormedModule.Exports.
Section NormedModule1.
Context {K : AbsRing} {V : NormedModule K}.
Definition norm : V → R := NormedModule.norm K _ (NormedModule.class K V).
Definition norm_factor : R := NormedModule.norm_factor K _ (NormedModule.class K V).
Lemma norm_triangle :
∀ x y : V,
norm (plus x y) ≤ norm x + norm y.
Lemma norm_scal :
∀ (l : K) (x : V),
norm (scal l x) ≤ abs l × norm x.
Lemma norm_compat1 :
∀ (x y : V) (eps : R),
norm (minus y x) < eps → ball x eps y.
Lemma norm_compat2 :
∀ (x y : V) (eps : posreal), ball x eps y → norm (minus y x) < norm_factor × eps.
Lemma norm_eq_zero :
∀ x : V, norm x = 0 → x = zero.
Lemma norm_zero :
norm zero = 0.
Lemma norm_factor_gt_0 :
0 < norm_factor.
Lemma norm_opp :
∀ x : V,
norm (opp x) = norm x.
Lemma norm_ge_0 :
∀ x : V,
0 ≤ norm x.
Lemma norm_gt_0 :
∀ x : V,
x ≠ zero → 0 < norm x.
Lemma norm_minus_gt_0 :
∀ x y : V,
x ≠ y → 0 < norm (minus x y).
Lemma norm_triangle_inv :
∀ x y : V,
Rabs (norm x - norm y) ≤ norm (minus x y).
Lemma eq_dec :
∀ x y : V,
{ x = y } + { x ≠ y }.
Lemma eq_close :
∀ x y : V,
close x y → x = y.
Definition ball_norm (x : V) (eps : R) (y : V) := norm (minus y x) < eps.
Definition locally_norm (x : V) (P : V → Prop) :=
∃ eps : posreal, ∀ y, ball_norm x eps y → P y.
Lemma locally_le_locally_norm :
∀ x, filter_le (locally x) (locally_norm x).
Lemma locally_norm_le_locally :
∀ x, filter_le (locally_norm x) (locally x).
Lemma locally_norm_ball_norm :
∀ (x : V) (eps : posreal),
locally_norm x (ball_norm x eps).
Lemma locally_norm_ball :
∀ (x : V) (eps : posreal),
locally_norm x (ball x eps).
Lemma locally_ball_norm :
∀ (x : V) (eps : posreal),
locally x (ball_norm x eps).
Lemma ball_norm_triangle (x y z : V) (e1 e2 : R) :
ball_norm x e1 y → ball_norm y e2 z → ball_norm x (e1 + e2) z.
Lemma ball_norm_center (x : V) (e : posreal) :
ball_norm x e x.
Lemma ball_norm_dec : ∀ (x y : V) (eps : posreal),
{ball_norm x eps y} + {¬ ball_norm x eps y}.
Lemma ball_norm_sym :
∀ (x y : V) (eps : posreal), ball_norm x eps y → ball_norm y eps x.
Lemma ball_norm_le :
∀ (x : V) (e1 e2 : posreal), e1 ≤ e2 →
∀ y, ball_norm x e1 y → ball_norm x e2 y.
Lemma ball_norm_eq :
∀ x y : V,
(∀ eps : posreal, ball_norm x eps y) → x = y.
Lemma is_filter_lim_unique :
∀ {F} {FF : ProperFilter' F} (x y : V),
is_filter_lim F x → is_filter_lim F y → x = y.
Lemma is_filter_lim_locally_unique :
∀ (x y : V),
is_filter_lim (locally x) y → x = y.
Definition closely_norm (P : V × V → Prop) :=
∃ eps : posreal, ∀ x y, ball_norm x eps y → P (x, y).
Lemma closely_le_closely_norm :
filter_le closely closely_norm.
Lemma closely_norm_le_closely :
filter_le closely_norm closely.
End NormedModule1.
Section NormedModule2.
Context {T : Type} {K : AbsRing} {V : NormedModule K}.
Lemma filterlim_closely_norm {F : (T → Prop) → Prop} {FF : Filter F} (f : T → V) :
filterlim (fun x ⇒ (f (fst x), f (snd x))) (filter_prod F F) closely_norm ↔
(∀ eps : posreal, ∃ P, F P ∧ ∀ u v : T, P u → P v → ball_norm (f u) eps (f v)).
Lemma filterlim_locally_unique :
∀ {F} {FF : ProperFilter' F} (f : T → V) (x y : V),
filterlim f F (locally x) → filterlim f F (locally y) →
x = y.
Lemma filterlimi_locally_unique :
∀ {F} {FF : ProperFilter' F} (f : T → V → Prop) (x y : V),
F (fun x ⇒ ∀ y1 y2, f x y1 → f x y2 → y1 = y2) →
filterlimi f F (locally x) → filterlimi f F (locally y) →
x = y.
End NormedModule2.
Rings with absolute values are normed modules
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)).
Module CompleteNormedModule.
Section ClassDef.
Variable K : AbsRing.
Record class_of (T : Type) := Class {
base : NormedModule.class_of K T ;
mixin : CompleteSpace.mixin_of (UniformSpace.Pack T base T)
}.
Local Coercion base : class_of >-> NormedModule.class_of.
Definition base2 T (cT : class_of T) : CompleteSpace.class_of T :=
CompleteSpace.Class _ (base T cT) (mixin T cT).
Local Coercion base2 : class_of >-> CompleteSpace.class_of.
Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.
Variable cT : type.
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition ModuleSpace := ModuleSpace.Pack _ cT xclass xT.
Definition NormedModuleAux := NormedModuleAux.Pack _ cT xclass xT.
Definition NormedModule := NormedModule.Pack _ cT xclass xT.
Definition UniformSpace := UniformSpace.Pack cT xclass xT.
Definition CompleteSpace := CompleteSpace.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> NormedModule.class_of.
Coercion mixin : class_of >-> CompleteSpace.mixin_of.
Coercion base2 : class_of >-> CompleteSpace.class_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion ModuleSpace : type >-> ModuleSpace.type.
Canonical ModuleSpace.
Coercion NormedModuleAux : type >-> NormedModuleAux.type.
Canonical NormedModuleAux.
Coercion NormedModule : type >-> NormedModule.type.
Canonical NormedModule.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Coercion CompleteSpace : type >-> CompleteSpace.type.
Canonical CompleteSpace.
Notation CompleteNormedModule := type.
End Exports.
End CompleteNormedModule.
Export CompleteNormedModule.Exports.
Section CompleteNormedModule1.
Context {K : AbsRing} {V : CompleteNormedModule K}.
Lemma iota_unique :
∀ (P : V → Prop) (x : V),
(∀ y, P y → y = x) →
P x →
iota P = x.
Lemma iota_correct :
∀ P : V → Prop,
(∃! x : V, P x) →
P (iota P).
Lemma iota_is_filter_lim {F} {FF : ProperFilter' F} (l : V) :
is_filter_lim F l →
iota (is_filter_lim F) = l.
Context {T : Type}.
Lemma iota_filterlim_locally {F} {FF : ProperFilter' F} (f : T → V) l :
filterlim f F (locally l) →
iota (fun 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.
Section prod_AbelianMonoid.
Context {U V : AbelianMonoid}.
Definition prod_plus (x y : U × V) :=
(plus (fst x) (fst y), plus (snd x) (snd y)).
Definition prod_zero : U × V := (zero, zero).
Lemma prod_plus_comm :
∀ x y : U × V,
prod_plus x y = prod_plus y x.
Lemma prod_plus_assoc :
∀ x y z : U × V,
prod_plus x (prod_plus y z) = prod_plus (prod_plus x y) z.
Lemma prod_plus_zero_r :
∀ x : U × V,
prod_plus x prod_zero = x.
End prod_AbelianMonoid.
Definition prod_AbelianMonoid_mixin (U V : AbelianMonoid) :=
AbelianMonoid.Mixin (U × V) _ _ prod_plus_comm prod_plus_assoc prod_plus_zero_r.
Canonical prod_AbelianMonoid (U V : AbelianMonoid) :=
AbelianMonoid.Pack (U × V) (prod_AbelianMonoid_mixin U V) (U × V).
Section prod_AbelianGroup.
Context {U V : AbelianGroup}.
Definition prod_opp (x : U × V) :=
(opp (fst x), opp (snd x)).
Lemma prod_plus_opp_r :
∀ x : U × V,
prod_plus x (prod_opp x) = prod_zero.
End prod_AbelianGroup.
Definition prod_AbelianGroup_mixin (U V : AbelianGroup) :=
AbelianGroup.Mixin _ _ (@prod_plus_opp_r U V).
Canonical prod_AbelianGroup (U V : AbelianGroup) :=
AbelianGroup.Pack (U × V) (AbelianGroup.Class _ _ (prod_AbelianGroup_mixin U V)) (U × V).
Section prod_UniformSpace.
Context {U V : UniformSpace}.
Definition prod_ball (x : U × V) (eps : R) (y : U × V) :=
ball (fst x) eps (fst y) ∧ ball (snd x) eps (snd y).
Lemma prod_ball_center :
∀ (x : U × V) (eps : posreal),
prod_ball x eps x.
Lemma prod_ball_sym :
∀ (x y : U × V) (eps : R),
prod_ball x eps y → prod_ball y eps x.
Lemma prod_ball_triangle :
∀ (x y z : U × V) (e1 e2 : R),
prod_ball x e1 y → prod_ball y e2 z →
prod_ball x (e1 + e2) z.
End prod_UniformSpace.
Definition prod_UniformSpace_mixin (U V : UniformSpace) :=
UniformSpace.Mixin (U × V) (point_of, point_of) _ prod_ball_center prod_ball_sym prod_ball_triangle.
Canonical prod_UniformSpace (U V : UniformSpace) :=
UniformSpace.Pack (U × V) (prod_UniformSpace_mixin U V) (U × V).
Section prod_ModuleSpace.
Context {K : Ring} {U V : ModuleSpace K}.
Definition prod_scal (x : K) (u : U × V) :=
(scal x (fst u), scal x (snd u)).
Lemma prod_scal_assoc :
∀ (x y : K) (u : U × V),
prod_scal x (prod_scal y u) = prod_scal (mult x y) u.
Lemma prod_scal_one :
∀ u : U × V,
prod_scal one u = u.
Lemma prod_scal_distr_l :
∀ (x : K) (u v : U × V),
prod_scal x (prod_plus u v) = prod_plus (prod_scal x u) (prod_scal x v).
Lemma prod_scal_distr_r :
∀ (x y : K) (u : U × V),
prod_scal (plus x y) u = prod_plus (prod_scal x u) (prod_scal y u).
End prod_ModuleSpace.
Definition prod_ModuleSpace_mixin (K : Ring) (U V : ModuleSpace K) :=
ModuleSpace.Mixin K _ _ (@prod_scal_assoc K U V) prod_scal_one prod_scal_distr_l prod_scal_distr_r.
Canonical prod_ModuleSpace (K : Ring) (U V : ModuleSpace K) :=
ModuleSpace.Pack K (U × V) (ModuleSpace.Class _ _ _ (prod_ModuleSpace_mixin K U V)) (U × V).
Canonical prod_NormedModuleAux (K : AbsRing) (U V : NormedModuleAux K) :=
NormedModuleAux.Pack K (U × V) (NormedModuleAux.Class _ _ (ModuleSpace.class K _) (UniformSpace.class (prod_UniformSpace U V))) (U × V).
Lemma sqrt_plus_sqr :
∀ x y : R, Rmax (Rabs x) (Rabs y) ≤ sqrt (x ^ 2 + y ^ 2) ≤ sqrt 2 × Rmax (Rabs x) (Rabs y).
Section prod_NormedModule.
Context {K : AbsRing} {U V : NormedModule K}.
Definition prod_norm (x : U × V) :=
sqrt (norm (fst x) ^ 2 + norm (snd x) ^ 2).
Lemma prod_norm_triangle :
∀ x y : U × V,
prod_norm (plus x y) ≤ prod_norm x + prod_norm y.
Lemma prod_norm_scal :
∀ (l : K) (x : U × V),
prod_norm (scal l x) ≤ abs l × prod_norm x.
Lemma prod_norm_compat1 :
∀ (x y : U × V) (eps : R),
prod_norm (minus y x) < eps → ball x eps y.
Definition prod_norm_factor :=
sqrt 2 × Rmax (@norm_factor K U) (@norm_factor K V).
Lemma prod_norm_compat2 :
∀ (x y : U × V) (eps : posreal),
ball x eps y →
prod_norm (minus y x) < prod_norm_factor × eps.
Lemma prod_norm_eq_zero :
∀ x : U × V,
prod_norm x = 0 → x = zero.
End prod_NormedModule.
Definition prod_NormedModule_mixin (K : AbsRing) (U V : NormedModule K) :=
NormedModule.Mixin K _ (@prod_norm K U V) prod_norm_factor prod_norm_triangle
prod_norm_scal prod_norm_compat1 prod_norm_compat2 prod_norm_eq_zero.
Canonical prod_NormedModule (K : AbsRing) (U V : NormedModule K) :=
NormedModule.Pack K (U × V) (NormedModule.Class K (U × V) _ (prod_NormedModule_mixin K U V)) (U × V).
Lemma norm_prod {K : AbsRing}
{U : NormedModule K} {V : NormedModule K}
(x : U) (y : V) :
Rmax (norm x) (norm y) ≤ norm (x,y) ≤ sqrt 2 × Rmax (norm x) (norm y).
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).
Section Matrices.
Context {T : Type}.
Definition matrix (m n : nat) := Tn m (Tn n T).
Definition coeff_mat {m n : nat} (x0 : T) (A : matrix m n) (i j : nat) :=
coeff_Tn x0 (coeff_Tn (mk_Tn _ (fun _ ⇒ x0)) A i) j.
Definition mk_matrix (m n : nat) (U : nat → nat → T) : matrix m n :=
mk_Tn m (fun i ⇒ (mk_Tn n (U i))).
Lemma mk_matrix_bij {m n : nat} (x0 : T) (A : matrix m n) :
mk_matrix m n (coeff_mat x0 A) = A.
Lemma coeff_mat_bij {m n : nat} (x0 : T) (u : nat → nat → T) :
∀ i j, (i < m)%nat → (j < n)%nat → coeff_mat x0 (mk_matrix m n u) i j = u i j.
Lemma coeff_mat_ext_aux {m n : nat} (x1 x2 : T) (v1 v2 : matrix m n) :
v1 = v2 ↔ ∀ i j, (i < m)%nat → (j < n)%nat → (coeff_mat x1 v1 i j) = (coeff_mat x2 v2 i j).
Lemma coeff_mat_ext {m n : nat} (x0 : T) (v1 v2 : matrix m n) :
v1 = v2 ↔ ∀ i j, (coeff_mat x0 v1 i j) = (coeff_mat x0 v2 i j).
Lemma mk_matrix_ext (m n : nat) (u1 u2 : nat → nat → T) :
(∀ i j, (i < m)%nat → (j < n)%nat → (u1 i j) = (u2 i j))
↔ (mk_matrix m n u1) = (mk_matrix m n u2).
End Matrices.
Section MatrixMonoid.
Context {G : AbelianMonoid} {m n : nat}.
Definition Mzero := mk_matrix m n (fun i j ⇒ @zero G).
Definition Mplus (A B : @matrix G m n) :=
mk_matrix m n (fun i j ⇒ plus (coeff_mat zero A i j) (coeff_mat zero B i j)).
Lemma Mplus_comm :
∀ A B : @matrix G m n,
Mplus A B = Mplus B A.
Lemma Mplus_assoc :
∀ A B C : @matrix G m n,
Mplus A (Mplus B C) = Mplus (Mplus A B) C.
Lemma Mplus_zero_r :
∀ A : @matrix G m n,
Mplus A Mzero = A.
Definition matrix_AbelianMonoid_mixin :=
AbelianMonoid.Mixin _ _ _ Mplus_comm Mplus_assoc Mplus_zero_r.
Canonical matrix_AbelianMonoid :=