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.

Require Import Reals 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 : (TProp) → Prop) (f : TU) (g : TV) :=
   eps : posreal, F (fun xnorm (g x) eps × norm (f x)).

Definition is_equiv {T} {K : AbsRing} {V : NormedModule K}
  (F : (TProp) → Prop) (f g : TV) :=
  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 : (TProp) → Prop} {FF : ProperFilter F} (f : TV),
  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 : (TProp) → Prop} {FF : Filter F} (f : TU) (g : TV) (h : TW),
  is_domin F f gis_domin F g his_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 : TV) :
  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 : (TProp) → Prop} {FF : Filter F} (f1 f2 : TU) (g : TV),
  is_equiv F f1 f2is_domin F f1 gis_domin F f2 g.

Lemma domin_rw_r {T} {Ku Kv : AbsRing}
  {U : NormedModule Ku} {V : NormedModule Kv} :
   {F : (TProp) → Prop} {FF : Filter F} (f : TU) (g1 g2 : TV),
  is_equiv F g1 g2is_domin F f g1is_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 : (TProp) → Prop} {FF : Filter F} (f : TV),
  is_equiv F f f.

Lemma equiv_sym :
   {F : (TProp) → Prop} {FF : Filter F} (f g : TV),
  is_equiv F f gis_equiv F g f.

Lemma equiv_trans :
   {F : (TProp) → Prop} {FF : Filter F} (f g h : TV),
  is_equiv F f gis_equiv F g his_equiv F f h.

Lemma equiv_carac_0 :
   {F : (TProp) → Prop} {FF : Filter F} (f g : TV),
  is_equiv F f g
  {o : TV | ( x : T, f x = plus (g x) (o x)) is_domin F g o }.

Lemma equiv_carac_1 :
   {F : (TProp) → Prop} {FF : Filter F} (f g o : TV),
  ( x, f x = plus (g x) (o x)) → is_domin F g ois_equiv F f g.

Lemma equiv_ext_loc {F : (TProp) → Prop} {FF : Filter F} (f g : TV) :
  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 : TU) (g : TV) :
  is_domin F f gfilter_le G Fis_domin G f g.

Lemma domin_scal_r :
   {F : (TProp) → Prop} {FF : Filter F} (f : TU) (g : TV) (c : Kv),
  is_domin F f gis_domin F f (fun xscal c (g x)).

Lemma domin_scal_l :
   {F : (TProp) → Prop} {FF : Filter F} (f : TU) (g : TV) (c : Ku),
  ( y, mult y c = one) → is_domin F f gis_domin F (fun xscal c (f x)) g.

Lemma domin_plus :
   {F : (TProp) → Prop} {FF : Filter F} (f : TU) (g1 g2 : TV),
  is_domin F f g1is_domin F f g2is_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 : (TProp) → Prop} {FF : Filter F} (f g : TV) (c : K),
  ( y : K, mult y c = one) →
  is_equiv F f gis_equiv F (fun xscal c (f x)) (fun xscal c (g x)).

Lemma equiv_plus :
   {F : (TProp) → Prop} {FF : Filter F} (f o : TV),
  is_domin F f ois_equiv F (fun xplus (f x) (o x)) f.

End Equiv_VS.

Multiplication and inverse

Domination

Lemma domin_mult_r :
   {T} {F : (TProp) → Prop} {FF : Filter F} (f g h : TR),
  is_domin F f gis_domin F (fun xf x × h x) (fun xg x × h x).

Lemma domin_mult_l :
   {T} {F : (TProp) → Prop} {FF : Filter F} (f g h : TR),
  is_domin F f gis_domin F (fun xh x × f x) (fun xh x × g x).

Lemma domin_mult :
   {T} {F : (TProp) → Prop} {FF : Filter F} (f1 f2 g1 g2 : TR),
  is_domin F f1 g1is_domin F f2 g2
  is_domin F (fun xf1 x × f2 x) (fun xg1 x × g2 x).

Lemma domin_inv :
   {T} {F : (TProp) → Prop} {FF : Filter F} (f g : TR),
  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 : (TProp) → Prop} {FF : Filter F} (f1 f2 g1 g2 : TR),
  is_equiv F f1 g1is_equiv F f2 g2
  is_equiv F (fun xf1 x × f2 x) (fun xg1 x × g2 x).

Lemma equiv_inv :
   {T} {F : (TProp) → Prop} {FF : Filter F} (f g : TR),
  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 : (T1Prop) → Prop) {FF : Filter F}
  (G : (T2Prop) → Prop) {FG : Filter G}.

Lemma domin_comp (f : T2U) (g : T2V) (l : T1T2) :
  filterlim l F Gis_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 : (TProp) → Prop} {FF : Filter F} (f g : TR) (l : Rbar),
  is_equiv F f g
  filterlim f F (Rbar_locally l) →
  filterlim g F (Rbar_locally l).