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.
J included in f(Q)
J included in f(Q)
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.