Library Chaos

Require Import List.
Require Import Ensembles.
Require Import Reals.
Require Import Coq.Sets.Image.
Require Import Omega.
Require Import ListFacts.


Section RealLemmas.

Open Local Scope R_scope.
Variable f:R->R.

Definition inrange (a b x:R):=a<=x /\ x<=b.

Hypothesis f_01_01: forall x:R, inrange 0 1 x -> inrange 0 1 (f x).

Hypothesis suprayectiva: forall y:R, inrange 0 1 y->
exists x:R, inrange 0 1 x /\ f x=y.

Hypothesis continua: continuity f.

Record Interval := mkInt{
a:R; b:R;
le:a<=b
}.

Definition Intcontenido (I J:Interval):=J.(a)<=I.(a) /\ I.(b)<=J.(b).

Hint Unfold inrange Intcontenido.

Definition idInterval:=mkInt 0 1 Rle_0_1.

Definition contenido :=included.

Definition rangeInt (I:Interval):=fun x:R=>inrange I.(a) I.(b) x.

Definition map:=Im R R.

Hint Unfold idInterval contenido rangeInt map.

Lemma rangeInt_a: forall I:Interval, rangeInt I I.(a).

Lemma rangeInt_b: forall I:Interval, rangeInt I I.(b).

Lemma diff_comm: forall (A:Type) (x y:A), x<>y->y<>x.

Lemma diff_2_0: 2<>0.

Lemma real_middlepoint: forall (x y:R), x<y->exists m:R, x<m<y.

Lemma posreal_destruct: forall (r:R) (Hr:0<r),
pos (mkposreal r Hr)=r.

Lemma disc_destruct_up: forall (x y r:R) (Hr:0<r),
disc x (mkposreal r Hr) y->x-r<y.

Lemma disc_destruct_down: forall (x y r:R) (Hr:0<r),
disc x (mkposreal r Hr) y-> y<x+r.

Lemma Singleton_compact: forall (x:R), compact (Singleton R x).

Definition Preimage (E:R->Prop) (x:R):=E (f x).

Lemma preimage_complementary: forall (E:R->Prop),
complementary (Preimage E)=Preimage (complementary E).

Lemma preimage_closed: forall (E:R->Prop),
closed_set E-> closed_set (Preimage E).

Lemma complementary_intersection: forall A B:R->Prop,
complementary (intersection_domain A B)=union_domain
(complementary A) (complementary B).

Lemma closed_set_intersection: forall D1 D2:R->Prop,
closed_set D1 -> closed_set D2->closed_set (intersection_domain D1 D2).

Lemma closed_set_half: forall (b:R), closed_set (fun x:R=>x<=b).

Lemma closed_set_half_down: forall (b:R), closed_set (fun x:R=>b<=x).

Lemma eq_closedset: forall (E:R->Prop) (v:R), closed_set E->
closed_set (fun x:R=> E x/\ f x=v).

Lemma lub_closed: forall (E:R->Prop) (lub:R),
is_lub E lub->closed_set E->E lub.


Lemma real_lub_eq: forall (E:R->Prop) (lub v:R), closed_set E->
is_lub E lub->(forall x:R,E x->f x=v)->f lub=v.

Lemma real_lub_eq2: forall (lub v b:R),
is_lub (fun x:R=> x<=b/\f x=v) lub->f lub=v.

Definition is_lower_bound (E:R -> Prop) (m:R) := forall x:R, E x -> m <= x.
Definition lbound (E:R -> Prop) := exists m : R, is_lower_bound E m.
Definition is_glb (E:R -> Prop) (m:R) :=
  is_lower_bound E m /\ (forall b:R, is_lower_bound E b -> b <= m).

Hint Unfold is_lower_bound lbound is_glb.

Lemma real_le_signchange_l: forall (x y:R), -x<=y -> -y<=x.

Lemma real_le_signchange_r: forall (x y:R), x<=-y -> y<=-x.

Lemma
  lcompleteness :
    forall E:R -> Prop,
      lbound E -> (exists x : R, E x) -> { m:R | is_glb E m }.

Lemma glb_closed: forall (E:R->Prop) (glb:R),
is_glb E glb->closed_set E->E glb.

Lemma real_glb_eq: forall (E:R->Prop) (glb v:R), closed_set E->
is_glb E glb->(forall x:R,E x->f x=v)->f glb=v.

Lemma real_glb_eq2: forall (glb v b:R),
is_glb (fun x:R=> b<=x/\f x=v) glb->f glb=v.

Lemma IVT_any: forall (p x y:R), x<=y-> f x<=p<=f y->
exists z, x<=z<=y /\ f z=p.
SearchAbout continuity. Qed.

End RealLemmas.

Section RealLemmas'.

Open Local Scope R_scope.
Variable f:R->R.

Hypothesis f_01_01: forall x:R, inrange 0 1 x -> inrange 0 1 (f x).
Hypothesis suprayectiva: forall y:R, inrange 0 1 y->
exists x:R, inrange 0 1 x /\ f x=y.
Hypothesis continua: continuity f.

Lemma IVT_any_rev: forall (p x y:R), x<=y-> f y<=p<=f x->
exists z, x<=z<=y /\ f z=p.

Lemma lema0: forall I J:Interval, contenido (rangeInt J) (map (rangeInt I) f)->
exists Q:Interval, Intcontenido Q I /\ map (rangeInt Q) f=rangeInt J.

Fixpoint f_repeat (n:nat) (f:R->R) (x:R):=
match n with
|0=>x
|S p=> f (f_repeat p f x)
end.

Lemma continuity_identity: forall (f:R->R) (ID:forall x:R,f x=x), continuity f.

Lemma f_repeat_continua: forall (n:nat), continuity (f_repeat n f).

End RealLemmas'.

Section Lema2.

Open Local Scope R_scope.
Variable f:R->R.
Hypothesis continua:continuity f.

Lemma lema2eq: forall (I:Interval), (map (rangeInt I) f=rangeInt I)->
exists x:R, rangeInt I x /\ f x=x.

Lemma lema2a: forall (I:Interval),
contenido (map (rangeInt I) f) (rangeInt I)->
exists x:R, rangeInt I x /\ f x=x.

Lemma lema2: forall (I:Interval),
contenido (rangeInt I) (map (rangeInt I) f)->
exists x:R, rangeInt I x /\ f x=x.

End Lema2.

Lemma f_repeat_commS: forall (n:nat) (f:R->R) (x:R),
f_repeat n f (f x)=f_repeat (S n) f x.

Lemma f_repeat_comm: forall (n:nat) (f:R->R) (x:R),
f_repeat n f (f x)=f (f_repeat n f x).

Section Chaos_begin.
Variable f:R->R.
Hypothesis f_01_01: forall x:R, inrange 0 1 x -> inrange 0 1 (f x).
Hypothesis suprayectiva: forall y:R, inrange 0 1 y->
exists x:R, inrange 0 1 x /\ f x=y.
Hypothesis continua: continuity f.

Fixpoint map_repeat (n:nat) (E:R->Prop) (f:R->R):=
match n with
|O=> E
|S p=> map_repeat p (map E f) f
end.

Lemma map_repeat_comm: forall (n:nat) (E:R->Prop) (f:R->R),
map (map_repeat n E f) f=map_repeat (S n) E f.

Lemma map_repeat_cons: forall (n:nat) (E:R->Prop) (f:R->R),
map_repeat n (map E f) f=map_repeat (S n) E f.

Lemma map_repeat_to_f_repeat: forall (n:nat) (E:R->Prop) (f:R->R),
map_repeat n E f=map E (f_repeat n f).

Lemma contenido_self: forall (A:R->Prop),contenido A A.

Lemma Intcontenido_self: forall (I:Interval), Intcontenido I I.

Lemma map_idInterval: map (rangeInt idInterval) f = rangeInt idInterval.

Lemma maprepeat_idInterval: forall k:nat,
map_repeat k (rangeInt idInterval) f = rangeInt idInterval.

Lemma cons_to_app: forall (A:Type) (l:list A) (x:A),
x::l=x::List.nil++l.

Lemma contenido_Intcontenido: forall A B:Interval,
contenido (rangeInt A) (rangeInt B)->
Intcontenido A B.

Lemma Intcontenido_contenido: forall A B:Interval,
Intcontenido A B->contenido (rangeInt A) (rangeInt B).

Lemma lema1: forall I:list Interval,
(forall k:nat, contenido (rangeInt (nth k I idInterval))
 (map (rangeInt (nth (S k) I idInterval)) f))->
exists Q:list Interval, length Q=length I/\
last Q idInterval=last I idInterval /\
forall k:nat,
Intcontenido (nth k Q idInterval) (nth (S k) Q idInterval) /\
map_repeat (length Q-(S k))
 (rangeInt (nth k Q idInterval)) f=rangeInt (nth k I idInterval).
SearchAbout map_repeat.
Qed.


Definition period (n:nat) (x:R):=f_repeat n f x=x.
Definition minperiod (n:nat) (x:R):=period n x/\
forall k:nat,0<k -> k<n -> ~period k x.

Open Local Scope R_scope.

Lemma contenido_map_rangeInt: forall (a b:R) (le:a<=b) (fle:f a<=f b),
contenido (rangeInt (mkInt (f a) (f b) fle))
 (map (rangeInt (mkInt a b le)) f).

Lemma contenido_map_rangeInt_rev: forall (a b:R) (le:a<=b) (fle:f b<=f a),
contenido (rangeInt (mkInt (f b) (f a) fle))
 (map (rangeInt (mkInt a b le)) f).

Require Import types.

Lemma chaos_prev: forall (a:R), rangeInt idInterval a->
minperiod 3 a-> a<=f a<=f(f a)-> forall k:nat, (3<k)%nat-> exists r:R, period k r.
SearchAbout last.
Qed.

Lemma chaos_prev_rev: forall (a:R), rangeInt idInterval a->
minperiod 3 a-> f(f a)<=f a<=a-> forall k:nat, (3<k)%nat-> exists r:R, period k r.

Lemma period_f: forall (n:nat) (x:R), period n x->period n (f x).

Lemma f_repeat_plus: forall (f:R->R) (m n:nat) (x:R),
f_repeat m f (f_repeat n f x)=f_repeat (plus m n) f x.

Lemma period_f_rev: forall (m n:nat) (x:R), period (S m) x-> period n (f x)->period n x.

Lemma minperiod0: forall (x:R), minperiod 0 x.

Lemma minperiod_f: forall (n:nat) (x:R),
minperiod n x->minperiod n (f x).

End Chaos_begin.

Section Chaos.
Variable f:R->R.
Hypothesis f_01_01: forall x:R, inrange 0 1 x -> inrange 0 1 (f x).
Hypothesis suprayectiva: forall y:R, inrange 0 1 y->
exists x:R, inrange 0 1 x /\ f x=y.
Hypothesis continua: continuity f.
Open Local Scope R_scope.

Theorem chaos: forall (a:R), rangeInt idInterval a->
minperiod f 3 a-> forall k:nat, (3<k)%nat-> exists r:R, period f k r.

End Chaos.

Print Assumptions chaos.