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.

From Coq Require Import Reals Psatz 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 xnorm (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 xminus (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 xnorm (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 xnorm (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 xf x = g x) is_equiv F f g.

End Equiv.

Vector space

is_domin is a vector space

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 xscal 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 xscal 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 xplus (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 xscal c (f x)) (fun xscal 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 xplus (f x) (o x)) f.

End Equiv_VS.

Multiplication and inverse

Domination

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 xf x × h x) (fun xg 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 xh x × f x) (fun xh 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 xf1 x × f2 x) (fun xg1 x × g2 x).

Lemma domin_inv :
   {T} {F : (T Prop) Prop} {FF : Filter F} (f g : T R),
  F (fun xg 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 xf1 x × f2 x) (fun xg1 x × g2 x).

Lemma equiv_inv :
   {T} {F : (T Prop) Prop} {FF : Filter F} (f g : T R),
  F (fun xg x 0) is_equiv F f g
  is_equiv F (fun x/ f x) (fun x/ g x).

Domination and composition


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 tf (l t)) (fun tg (l t)).

End Domin_comp.

Equivalence and limits


Lemma filterlim_equiv :
   {T} {F : (T Prop) Prop} {FF : Filter F} (f g : T R) (l : Rbar),
  is_equiv F f g
  filterlim f F (Rbar_locally l)
  filterlim g F (Rbar_locally l).