Library Coquelicot.Equiv
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.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
Require Import Reals Psatz.
Require Import mathcomp.ssreflect.ssreflect.
Require Import Rbar Rcomplements Hierarchy.
This file gives definitions of equivalent (g ~ f) and dominant (g
= o(f)). This is used for defining differentiability on a
NormedModule.
Definition is_domin {T} {Ku Kv : AbsRing}
{U : NormedModule Ku} {V : NormedModule Kv}
(F : (T → Prop) → Prop) (f : T → U) (g : T → V) :=
∀ eps : posreal, F (fun x ⇒ norm (g x) ≤ eps × norm (f x)).
Definition is_equiv {T} {K : AbsRing} {V : NormedModule K}
(F : (T → Prop) → Prop) (f g : T → V) :=
is_domin F g (fun x ⇒ minus (g x) (f x)).
To be dominant is a partial strict order
Lemma domin_antisym {T} {K : AbsRing} {V : NormedModule K} :
∀ {F : (T → Prop) → Prop} {FF : ProperFilter F} (f : T → V),
F (fun x ⇒ norm (f x) ≠ 0) → ¬ is_domin F f f.
Lemma domin_trans {T} {Ku Kv Kw : AbsRing}
{U : NormedModule Ku} {V : NormedModule Kv} {W : NormedModule Kw} :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f : T → U) (g : T → V) (h : T → W),
is_domin F f g → is_domin F g h → is_domin F f h.
Relations between domination and equivalence
Lemma equiv_le_2 {T} {K : AbsRing} {V : NormedModule K}
F {FF : Filter F} (f g : T → V) :
is_equiv F f g →
F (fun x ⇒ norm (g x) ≤ 2 × norm (f x) ∧ norm (f x) ≤ 2 × norm (g x)).
Lemma domin_rw_l {T} {Ku Kv : AbsRing}
{U : NormedModule Ku} {V : NormedModule Kv} :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f1 f2 : T → U) (g : T → V),
is_equiv F f1 f2 → is_domin F f1 g → is_domin F f2 g.
Lemma domin_rw_r {T} {Ku Kv : AbsRing}
{U : NormedModule Ku} {V : NormedModule Kv} :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f : T → U) (g1 g2 : T → V),
is_equiv F g1 g2 → is_domin F f g1 → is_domin F f g2.
To be equivalent is an equivalence relation
Section Equiv.
Context {T : Type} {K : AbsRing} {V : NormedModule K}.
Lemma equiv_refl :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f : T → V),
is_equiv F f f.
Lemma equiv_sym :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f g : T → V),
is_equiv F f g → is_equiv F g f.
Lemma equiv_trans :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f g h : T → V),
is_equiv F f g → is_equiv F g h → is_equiv F f h.
Lemma equiv_carac_0 :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f g : T → V),
is_equiv F f g →
{o : T → V | (∀ x : T, f x = plus (g x) (o x)) ∧ is_domin F g o }.
Lemma equiv_carac_1 :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f g o : T → V),
(∀ x, f x = plus (g x) (o x)) → is_domin F g o → is_equiv F f g.
Lemma equiv_ext_loc {F : (T → Prop) → Prop} {FF : Filter F} (f g : T → V) :
F (fun x ⇒ f x = g x) → is_equiv F f g.
End Equiv.
Section Domin.
Context {T : Type} {Ku Kv : AbsRing}
{U : NormedModule Ku} {V : NormedModule Kv}.
Lemma is_domin_le {F G} (f : T → U) (g : T → V) :
is_domin F f g → filter_le G F → is_domin G f g.
Lemma domin_scal_r :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f : T → U) (g : T → V) (c : Kv),
is_domin F f g → is_domin F f (fun x ⇒ scal c (g x)).
Lemma domin_scal_l :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f : T → U) (g : T → V) (c : Ku),
(∃ y, mult y c = one) → is_domin F f g → is_domin F (fun x ⇒ scal c (f x)) g.
Lemma domin_plus :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f : T → U) (g1 g2 : T → V),
is_domin F f g1 → is_domin F f g2 → is_domin F f (fun x ⇒ plus (g1 x) (g2 x)).
End Domin.
is_equiv is compatible with the vector space structure
Section Equiv_VS.
Context {T : Type} {K : AbsRing} {V : NormedModule K}.
Lemma equiv_scal :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f g : T → V) (c : K),
(∃ y : K, mult y c = one) →
is_equiv F f g → is_equiv F (fun x ⇒ scal c (f x)) (fun x ⇒ scal c (g x)).
Lemma equiv_plus :
∀ {F : (T → Prop) → Prop} {FF : Filter F} (f o : T → V),
is_domin F f o → is_equiv F (fun x ⇒ plus (f x) (o x)) f.
End Equiv_VS.
Lemma domin_mult_r :
∀ {T} {F : (T → Prop) → Prop} {FF : Filter F} (f g h : T → R),
is_domin F f g → is_domin F (fun x ⇒ f x × h x) (fun x ⇒ g x × h x).
Lemma domin_mult_l :
∀ {T} {F : (T → Prop) → Prop} {FF : Filter F} (f g h : T → R),
is_domin F f g → is_domin F (fun x ⇒ h x × f x) (fun x ⇒ h x × g x).
Lemma domin_mult :
∀ {T} {F : (T → Prop) → Prop} {FF : Filter F} (f1 f2 g1 g2 : T → R),
is_domin F f1 g1 → is_domin F f2 g2 →
is_domin F (fun x ⇒ f1 x × f2 x) (fun x ⇒ g1 x × g2 x).
Lemma domin_inv :
∀ {T} {F : (T → Prop) → Prop} {FF : Filter F} (f g : T → R),
F (fun x ⇒ g x ≠ 0) → is_domin F f g →
is_domin F (fun x ⇒ / g x) (fun x ⇒ / f x).
Equivalence
Lemma equiv_mult :
∀ {T} {F : (T → Prop) → Prop} {FF : Filter F} (f1 f2 g1 g2 : T → R),
is_equiv F f1 g1 → is_equiv F f2 g2 →
is_equiv F (fun x ⇒ f1 x × f2 x) (fun x ⇒ g1 x × g2 x).
Lemma equiv_inv :
∀ {T} {F : (T → Prop) → Prop} {FF : Filter F} (f g : T → R),
F (fun x ⇒ g x ≠ 0) → is_equiv F f g →
is_equiv F (fun x ⇒ / f x) (fun x ⇒ / g x).
Section Domin_comp.
Context {T1 T2 : Type} {Ku Kv : AbsRing}
{U : NormedModule Ku} {V : NormedModule Kv}
(F : (T1 → Prop) → Prop) {FF : Filter F}
(G : (T2 → Prop) → Prop) {FG : Filter G}.
Lemma domin_comp (f : T2 → U) (g : T2 → V) (l : T1 → T2) :
filterlim l F G → is_domin G f g
→ is_domin F (fun t ⇒ f (l t)) (fun t ⇒ g (l t)).
End Domin_comp.