Library LM.fixed_point

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
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.

From Coquelicot Require Import Coquelicot.

From Numbers Require Import Numbers_wDep R_compl.

Fixed Point Theorem without subspaces


Section FixedPoint_1.

Context {X : UniformSpace}.
Context {Y : UniformSpace}.

Definition ball_x : X R X Prop := UniformSpace.ball _ (UniformSpace.class X).
Definition ball_y : Y R Y Prop := UniformSpace.ball _ (UniformSpace.class Y).

Lispchitz functions

Definition is_Lipschitz (f: X Y) (k:R) :=
  0 k
     x1 x2 r, 0 < r
      ball_x x1 r x2 ball_y (f x1) (k×r) (f x2).

Definition is_contraction (f: X Y) :=
   k, k < 1 is_Lipschitz f k.

End FixedPoint_1.

Balls and iterations

Section iter_dist.

Context {X : UniformSpace}.

Fixpoint iter (f:X X) (n:nat) (x:X) := match n with
   | Ox
   | S mf (iter f m x)
  end.

Lemma dist_iter_aux_aux: (f:XX) a k p D, 0 < k < 1 is_Lipschitz f k
    0 < D ball a D (f a)
   ball (iter f p a) (k ^ p × D) (iter f (p + 1) a).
Proof.
intros f a k p D (Hk1',Hk2') (_,Hk2) HD H.
induction p.
simpl.
now rewrite Rmult_1_l.
simpl.
rewrite Rmult_assoc.
apply Hk2.
apply Rmult_lt_0_compat; try assumption.
now apply pow_lt.
assumption.
Qed.

Lemma dist_iter_aux: (f:XX) a k p m D, 0 < k < 1 is_Lipschitz f k
    0 < D ball a D (f a) (0 < m)%nat
    ball (iter f p a) (k^p*(1-k^m)/(1-k) ×D) (iter f (p+m) a).
intros f a k p m D (Hk1',Hk2') (Hk1,Hk2) HD H Hm.
case_eq m.
intros Y; rewrite Y in Hm.
now contradict Hm.
intros n _; clear Hm.
induction n.
simpl.
rewrite Rmult_1_r.
replace (k ^ p × (1 - k) / (1 - k) × D) with (k^p×D).
2: field.
2: now apply Rgt_not_eq, Rlt_0_minus.
apply dist_iter_aux_aux; try split; assumption.
replace (k ^ p × (1 - k ^ S (S n)) / (1 - k) × D) with
   ((k ^ p × (1 - k ^ S n) / (1 - k) × D)+(k ^ (p+S n) × D)).
apply ball_triangle with (iter f (p + S n) a).
exact IHn.
replace (p + S (S n))%nat with ((p+S n)+1)%nat.
apply dist_iter_aux_aux; try split; assumption.
ring.
rewrite pow_add.
simpl; field.
now apply Rgt_not_eq, Rlt_0_minus.
Qed.

Lemma dist_iter: (f:XX) a k p m D, 0 < k < 1 is_Lipschitz f k
    0 < D ball a D (f a)
    ball (iter f p a) (k^p/(1-k) ×D) (iter f (p+m) a).
Proof.
intros f a k p m D H1 H2 H3 H4.
case_eq m.
intros _; rewrite Nat.add_0_r.
assert (L:(0 < k ^ p / (1 - k) × D)).
apply Rmult_lt_0_compat; trivial.
apply Rdiv_lt_0_compat.
now apply pow_lt.
now apply Rlt_0_minus.
replace (k ^ p / (1 - k) × D) with (pos (mkposreal _ L)) by reflexivity.
apply ball_center.
intros n Hn.
apply ball_le with (k^p*(1-k^m)/(1-k) ×D).
apply Rmult_le_compat_r.
now left.
unfold Rdiv; apply Rmult_le_compat_r.
left; apply Rinv_0_lt_compat.
now apply Rlt_0_minus.
rewrite <- (Rmult_1_r (k^p)) at 2.
apply Rmult_le_compat_l.
left; now apply pow_lt.
apply Rplus_le_reg_l with (-1).
ring_simplify.
rewrite <- Ropp_0.
apply Ropp_le_contravar.
left; now apply pow_lt.
rewrite Hn.
apply dist_iter_aux; try assumption.
auto with arith.
Qed.

Variable f: X X.
Variable phi: X Prop.
Hypothesis phi_f: x:X, phi x phi (f x).
Hypothesis phi_distanceable:
    (x y:X), phi x phi y M, 0 M ball x M y.

Lemma phi_iter_f: a n, phi a phi (iter f n a).
Proof.
intros a; induction n; intros Phi_a.
now simpl.
simpl.
now apply phi_f, IHn.
Qed.

Lemma dist_iter_aux_zero: (a:X) p m,
    phi a
    is_Lipschitz f 0
    (0 < p)%nat (0 < m)%nat
   ball (iter f p a) 0 (iter f m a).
Proof.
intros a p m phi_a (_,H) Hp Hm.
case_eq p.
intros V; rewrite V in Hp; now contradict Hp.
intros n1 Hn1.
case_eq m.
intros V; rewrite V in Hm; now contradict Hm.
intros n2 Hn2.
simpl.
destruct (phi_distanceable (iter f n1 a) (iter f n2 a)) as (M,(HM1,HM2)).
now apply phi_iter_f.
now apply phi_iter_f.
replace 0 with (0*(M+1)) by ring.
apply H; try assumption.
apply Rle_lt_trans with (M+0).
now rewrite Rplus_0_r.
apply Rplus_lt_compat_l, Rlt_0_1.
apply ball_le with M; try assumption.
apply Rle_trans with (M+0).
right; ring.
apply Rplus_le_compat_l, Rle_0_1.
Qed.

Lemma dist_iter_gen: a k p m n D, 0 k < 1 is_Lipschitz f k
   phi a
   0 < D ball a D (f a) (n p)%nat (n m)%nat (0 < n)%nat
    ball (iter f p a) (k^n/(1-k) ×D) (iter f m a).
Proof.
intros a k p m n D (H1,H1') H2 Phi_a H3 H4 Hp Hm Hn.
case H1; intros P.
case (Nat.le_gt_cases p m); intros H5.
replace m with (p+(m-p))%nat.
apply ball_le with (k^p/(1-k) ×D).
apply Rmult_le_compat_r.
now left.
unfold Rdiv; apply Rmult_le_compat_r.
left; apply Rinv_0_lt_compat.
now apply Rlt_0_minus.
apply Rle_pow_le; try assumption.
split; try left; try assumption.
apply dist_iter; try assumption.
split; assumption.
now rewrite Nat.add_comm, Nat.sub_add.
apply ball_sym.
replace p with (m+(p-m))%nat.
apply ball_le with (k^m/(1-k) ×D).
apply Rmult_le_compat_r.
now left.
unfold Rdiv; apply Rmult_le_compat_r.
left; apply Rinv_0_lt_compat.
now apply Rlt_0_minus.
apply Rle_pow_le; try assumption.
split; try left; assumption.
apply dist_iter; try assumption.
split; assumption.
rewrite Nat.add_comm, Nat.sub_add; [reflexivity | apply Nat.lt_le_incl; assumption].
apply ball_le with 0.
rewrite <- P.
rewrite pow_i; try assumption.
right; unfold Rdiv; ring.
apply dist_iter_aux_zero; try assumption.
now rewrite P.
now apply Nat.lt_le_trans with n.
now apply Nat.lt_le_trans with n.
Qed.

End iter_dist.

My_complete

Section closed_compl.

Context {X : CompleteSpace}.
Definition lim : ((X Prop) Prop) X := CompleteSpace.lim _ (CompleteSpace.class X).

Definition my_complete (phi:XProp) := ( (F:(X Prop) Prop),
    ProperFilter F cauchy F
   ( P, F P ~~( x, P x phi x)) phi (lim F)).

Lemma closed_my_complete: phi,
     closed phi my_complete phi.
Proof.
intros phi phi_closed F H1 H2 H3.
generalize (@complete_cauchy X F H1 H2).
intros H4.
unfold closed in *; unfold open in ×.
apply phi_closed.
intros H6'.
destruct H6' as (eps,H6).
specialize (H3 (ball (lim F) eps)).
apply H3.
apply H4.
intros (y,(Hy1,Hy2)).
specialize (H6 y Hy1).
now apply H6.
Qed.

End closed_compl.

Section closed_compl2.

Context {X : CompleteNormedModule R_AbsRing}.

Variable phi: X Prop.

Lemma my_complete_closed:
   my_complete phi closed phi.
Proof.
intros H x Hx.
pose (F:= locally x).
assert (ProperFilter F).
apply locally_filter.
assert (cauchy F).
intros e; unfold F.
x.
now e.
replace x with (lim F).
apply H; try assumption.
unfold F; intros P T1 T2.
destruct T1 as (e,He).
apply Hx.
e.
intros y Hy1 Hy2.
apply T2.
y; split; try easy.
now apply He.
apply sym_eq, eq_close.
intros e.
generalize (complete_cauchy F H0 H1 e).
unfold F; simpl.
intros (ee,Hee).
apply ball_sym.
apply Hee.
apply ball_center.
Qed.

End closed_compl2.

Fixed Point Theorem

Section FixedPoint_2.

Context {X : CompleteSpace}.

Variable (f:XX).

Variable phi: X Prop.

Hypothesis phi_f: x:X, phi x phi (f x).
Hypothesis phi_distanceable:
    (x y:X), phi x phi y M, 0 M ball x M y.

Lemma FixedPoint_uniqueness_weak: a b, is_contraction f
       phi a phi b
       close (f a) a close (f b) b
        close a b.
Proof.
intros a b (k,(Hk1,(Hk2,Hf))) Phi_a Phi_b Ha Hb eps.
destruct (phi_distanceable a b) as (M,(HM1,HM2)); try assumption.
destruct HM1.
pose (k' := (k + 1)/2).
assert (k < k').
unfold k'; apply Rmult_lt_reg_l with 2%R.
apply Rlt_0_2.
apply Rplus_lt_reg_l with (-k).
replace (-k+2×k) with k by ring.
replace (-k + 2 × ((k + 1) / 2)) with 1 by field.
assumption.
assert (0 < k' < 1).
split.
apply Rle_lt_trans with k; assumption.
unfold k'; apply Rmult_lt_reg_l with 2%R.
apply Rlt_0_2.
apply Rplus_lt_reg_l with (-1).
replace (-1+2×1) with 1 by ring.
replace (-1 + 2 × ((k + 1) / 2)) with k by field.
assumption.
destruct (contraction_lt_any k' (eps/M)) as (N,HN).
now (split; try left).
apply Rdiv_lt_0_compat; trivial.
destruct eps; simpl; easy.
apply ball_le with (M×k'^N).
apply Rmult_le_reg_r with (/M).
now apply Rinv_0_lt_compat.
left; apply Rle_lt_trans with (2:=HN).
right; field.
now apply Rgt_not_eq.
clear HN; induction N.
simpl; rewrite Rmult_1_r.
assumption.
assert (L:(0 < M×k'^S N*(k'-k)/2)).
apply Rdiv_lt_0_compat; try apply Rlt_0_2.
apply Rmult_lt_0_compat.
apply Rmult_lt_0_compat; try assumption.
now apply pow_lt.
now apply Rlt_0_minus.
specialize (Ha (mkposreal _ L)).
specialize (Hb (mkposreal _ L)).
apply ball_le with ((M × k' ^ (S N) × (k' - k) / 2) + ((k*(M × k' ^ N)) + (M × k' ^ (S N) × (k' - k) / 2))).
simpl.
apply Rle_trans with ((k'*(k' - k) + k)*M×k'^N).
right; field.
apply Rle_trans with (k'×M×k'^N).
2: right; ring.
apply Rmult_le_compat_r.
left; now apply pow_lt.
apply Rmult_le_compat_r.
now left.
apply Rplus_le_reg_l with (-k'*(k'-k)-k).
apply Rle_trans with 0.
right; ring.
apply Rle_trans with (Rsqr ((k-1)/2)).
apply Rle_0_sqr.
right; unfold Rsqr, k'.
field.
apply ball_triangle with (f a).
apply ball_sym, Ha.
apply ball_triangle with (f b).
apply Hf; try assumption.
apply Rmult_lt_0_compat; try assumption.
now apply pow_lt.
apply Hb.
apply ball_le with M; try assumption.
rewrite <- H; destruct eps; simpl; left; easy.
Qed.

Lemma Fixed_Point_aux_Proper: (a:X),
    ProperFilter (fun Peventually (fun nP (iter f n a))).
Proof.
intros a; split.
intros P (N,HN).
(iter f N a).
apply HN.
apply le_n.
split.
0%nat; easy.
intros P Q (N1,H1) (N2,H2).
(max N1 N2).
intros n Hn; split.
apply H1.
apply Nat.le_trans with (2:=Hn).
apply Nat.le_max_l.
apply H2.
apply Nat.le_trans with (2:=Hn).
apply Nat.le_max_r.
intros P Q H (N,HN).
N.
intros n Hn.
apply H.
now apply HN.
Qed.

Lemma Fixed_Point_aux_cauchy: (a:X), is_contraction f
    phi a cauchy (fun Peventually (fun nP (iter f n a))).
intros a (k,(Hk1,(Hk2,Hf))) Phi_a.
generalize (@cauchy_distance X _ (Fixed_Point_aux_Proper a)).
unfold cauchy; intros (_,T); apply T; clear T.
intros eps.
destruct (phi_distanceable a (f a)) as (M,(HM1,HM2)).
assumption.
now apply phi_f.
destruct HM1.
destruct (contraction_lt_any' k (eps/M*(1-k)*/3)) as (n,(Hn',Hn)).
now split.
apply Rmult_lt_0_compat.
apply Rmult_lt_0_compat.
apply Rdiv_lt_0_compat; trivial.
destruct eps; now simpl.
now apply Rlt_0_minus.
apply Rinv_0_lt_compat.
apply Rplus_lt_0_compat; try apply Rlt_0_1; apply Rlt_0_2.
(fun x m:nat, (n m)%nat close x (iter f m a)).
split.
n.
intros l Hl.
l; split; try easy.
intros E; apply ball_center.
intros u v (n1,(Hn1,Hu)) (n2,(Hn2,Hv)).
assert (L:(0 < eps/3)).
apply Rdiv_lt_0_compat.
destruct eps; now simpl.
apply Rplus_lt_0_compat; try apply Rlt_0_1; apply Rlt_0_2.
pose (e:=mkposreal _ L).
replace (pos eps) with (pos e+(pos e+pos e))%R by (simpl;field).
apply ball_triangle with (iter f n1 a).
apply Hu.
apply ball_triangle with (iter f n2 a).
2: apply ball_sym, Hv.
apply ball_le with (k ^ n / (1 - k) × M).
unfold e; simpl.
apply Rmult_le_reg_l with (/M).
now apply Rinv_0_lt_compat.
apply Rmult_le_reg_l with (1-k).
now apply Rlt_0_minus.
apply Rle_trans with (eps / M × (1 - k) × / 3).
2: right; unfold Rdiv; ring.
left; apply Rle_lt_trans with (2:=Hn).
right; field.
split; apply Rgt_not_eq; try assumption.
now apply Rlt_0_minus.
apply dist_iter_gen with phi; try assumption.
now split.
now split.
rewrite <- H in HM2.
assert ( n, close (iter f n a) a).
apply nat_ind_strong with (P:= fun nclose (iter f n a) a).
intros n; case n.
simpl; intros _.
intros e; apply ball_center.
clear n; intros n; case n.
intros _; simpl.
intros e; apply ball_sym, ball_le with 0; try assumption.
destruct e; left; now simpl.
clear n; intros n IH.
apply close_trans with (iter f (S n) a).
2: apply IH.
2: apply le_n.
simpl; intros e.
apply ball_le with (k×e).
rewrite <- (Rmult_1_l e) at 2.
apply Rmult_le_compat_r.
destruct e; left; now simpl.
now left.
apply Hf.
apply cond_pos.
assert (L:(close (iter f (S n) a) (iter f n a))).
apply close_trans with a.
apply IH.
apply le_n.
apply close_sym.
apply IH.
apply le_S, le_n.
apply L.
(fun xclose x a).
split.
0%nat.
intros n _; apply H0.
intros u v Hu Hv.
assert (close u v).
apply close_trans with a; try assumption.
now apply close_sym.
apply H1.
Qed.

Lemma FixedPoint_aux1: (a:X), is_contraction f phi a
  let x := lim (fun Peventually (fun nP (iter f n a))) in
      close (f x) x.
Proof.
intros a Hf Phi_a x.
generalize (complete_cauchy
   (fun Peventually (fun nP (iter f n a)))
    (Fixed_Point_aux_Proper a)
    (Fixed_Point_aux_cauchy a Hf Phi_a)).
replace ((Hierarchy.lim
         (fun P : X Propeventually (fun n0 : natP (iter f n0 a))))) with x by reflexivity.
intros H eps.
pose (e2 :=mkposreal _ (is_pos_div_2 eps)).
specialize (H e2).
destruct H as (n,Hn).
replace (pos eps) with (pos e2 + pos e2).
2: simpl; field.
apply ball_sym.
apply ball_triangle with (iter f (S n) a).
apply Hn.
apply le_S, le_n.
destruct Hf as (k,(Hk1,(Hk2,Hk3))).
apply ball_le with (k×e2).
rewrite <- (Rmult_1_l e2) at 2.
apply Rmult_le_compat_r.
destruct e2; left; now simpl.
now left.
simpl.
apply Hk3.
apply (cond_pos e2).
apply ball_sym.
apply Hn.
apply le_n.
Qed.

Hypothesis phi_X_not_empty: (a:X), phi a.
Hypothesis phi_closed: my_complete phi.

Lemma FixedPoint_aux2: (a:X), is_contraction f phi a
  let x := lim
  (fun Peventually (fun nP (iter f n a))) in
      phi x.
Proof.
intros a Hf Phi_a x.
apply phi_closed.
apply Fixed_Point_aux_Proper.
now apply Fixed_Point_aux_cauchy.
intros P (N,HN).
intros K; apply K.
(iter f N a).
split.
apply HN.
apply le_n.
now apply phi_iter_f.
Qed.

Theorem FixedPoint_C: is_contraction f
    a:X,
     phi a
       close (f a) a
       ( b, phi b close (f b) b close b a)
     x, phi x close (lim (fun Peventually (fun nP (iter f n x)))) a.
Proof.
intros Hf.
destruct phi_X_not_empty as (a, Ha).
(lim (fun Peventually (fun nP (iter f n a)))).
split.
now apply FixedPoint_aux2.
split.
now apply FixedPoint_aux1.
split.
intros b Phi_b Hb.
apply FixedPoint_uniqueness_weak; try assumption.
now apply FixedPoint_aux2.
now apply FixedPoint_aux1.
intros x Phi_x.
apply FixedPoint_uniqueness_weak; try assumption.
now apply FixedPoint_aux2.
now apply FixedPoint_aux2.
now apply FixedPoint_aux1.
now apply FixedPoint_aux1.
Qed.

End FixedPoint_2.

Fixed Point Theorem without norms

Section FixedPoint_Normed.

Variable K : AbsRing.
Context {X : CompleteNormedModule K}.

Variable (f:XX).

Variable phi: X Prop.
Hypothesis phi_f: x:X, phi x phi (f x).
Hypothesis phi_X_not_empty: (a:X), phi a.
Hypothesis phi_closed: my_complete phi.

Theorem FixedPoint: is_contraction f
    a:X,
     phi a
       f a = a
       ( b, phi b f b = b b = a)
     x, phi x lim (fun Peventually (fun nP (iter f n x))) = a.
Proof.
intros Hf.
destruct (FixedPoint_C f phi) as (a,Ha); try assumption.
intros x y _ _.
case (Rle_lt_or_eq_dec 0 (norm (minus y x))).
apply norm_ge_0.
intros H1.
assert (Y: 0 < 2×norm (minus y x)).
apply Rmult_lt_0_compat; try apply Rlt_0_2; assumption.
(mkposreal _ Y).
split.
left; apply cond_pos.
apply (norm_compat1 x y).
simpl.
apply Rplus_lt_reg_r with (-norm (minus y x)).
ring_simplify.
apply Rle_lt_trans with (2:=H1).
apply Rle_minus.
right; reflexivity.
intros H1.
(mkposreal _ Rlt_0_1).
split.
left; apply cond_pos.
replace x with y.
apply ball_center.
apply plus_reg_r with (opp x).
rewrite plus_opp_r.
apply (norm_eq_zero (plus y (opp x))).
now apply sym_eq.
destruct Ha as (Ha1,(Ha2,(Ha3,Ha4))).
a.
split; [assumption|split].
now apply eq_close.
split.
intros b Hb1 Hb2.
apply eq_close, Ha3; try assumption.
rewrite Hb2; now apply close_refl.
intros x Hx.
apply eq_close, Ha4; try assumption.
Qed.

End FixedPoint_Normed.

Fixed Point Theorem with subsets


Section FixedPoint_1_sub.

Context {X : UniformSpace}.
Context {Y : UniformSpace}.

Lispchitz functions with subsets

Definition is_Lipschitz_phi (f: X Y) (k:R) (P : X Prop) :=
  0 k
     x1 x2 r, 0 < r P x1 P x2
      ball_x x1 r x2 ball_y (f x1) (k×r) (f x2).

Definition is_contraction_phi (f: X Y) (P : X Prop) :=
   k, k < 1 is_Lipschitz_phi f k P.

End FixedPoint_1_sub.

Balls and iterations with subsets

Section iter_dist_sub.

Context {X : UniformSpace}.

Lemma dist_iter_aux_aux_phi: (f:XX) (P : X Prop) a k p D, 0 < k < 1
    ( p, P (iter f p a)) is_Lipschitz_phi f k P 0 < D ball a D (f a)
   ball (iter f p a) (k ^ p × D) (iter f (p + 1) a).
Proof.
intros f P a k p D (Hk1',Hk2') HH (_,Hk2) HD H.
induction p.
simpl.
now rewrite Rmult_1_l.
simpl.
rewrite Rmult_assoc.
apply Hk2.
apply Rmult_lt_0_compat; try assumption.
now apply pow_lt.
apply HH.
apply HH.
assumption.
Qed.

Lemma dist_iter_aux_phi : (f:XX) (P : X Prop) a k p m D,
    0 < k < 1 ( p, P (iter f p a)) is_Lipschitz_phi f k P
    0 < D ball a D (f a) (0 < m)%nat
    ball (iter f p a) (k^p*(1-k^m)/(1-k) ×D) (iter f (p+m) a).
intros f P a k p m D (Hk1',Hk2') HH (Hk1,Hk2) HD H Hm.
case_eq m.
intros Y; rewrite Y in Hm.
now contradict Hm.
intros n _; clear Hm.
induction n.
simpl.
rewrite Rmult_1_r.
replace (k ^ p × (1 - k) / (1 - k) × D) with (k^p×D).
2: field.
2: now apply Rgt_not_eq, Rlt_0_minus.
apply dist_iter_aux_aux_phi with P; try split; assumption.
replace (k ^ p × (1 - k ^ S (S n)) / (1 - k) × D) with
   ((k ^ p × (1 - k ^ S n) / (1 - k) × D)+(k ^ (p+S n) × D)).
apply ball_triangle with (iter f (p + S n) a).
exact IHn.
replace (p + S (S n))%nat with ((p+S n)+1)%nat.
apply dist_iter_aux_aux_phi with P; try split; assumption.
ring.
rewrite pow_add.
simpl; field.
now apply Rgt_not_eq, Rlt_0_minus.
Qed.

Lemma dist_iter_phi: (f:XX) (P:X Prop) a k p m D, 0 < k < 1
     ( p, P (iter f p a)) is_Lipschitz_phi f k P
    0 < D ball a D (f a)
    ball (iter f p a) (k^p/(1-k) ×D) (iter f (p+m) a).
Proof.
intros f P a k p m D H1 H2 HH H3 H4.
case_eq m.
intros _; rewrite Nat.add_0_r.
assert (L:(0 < k ^ p / (1 - k) × D)).
apply Rmult_lt_0_compat; trivial.
apply Rdiv_lt_0_compat.
now apply pow_lt.
now apply Rlt_0_minus.
replace (k ^ p / (1 - k) × D) with (pos (mkposreal _ L)) by reflexivity.
apply ball_center.
intros n Hn.
apply ball_le with (k^p*(1-k^m)/(1-k) ×D).
apply Rmult_le_compat_r.
now left.
unfold Rdiv; apply Rmult_le_compat_r.
left; apply Rinv_0_lt_compat.
now apply Rlt_0_minus.
rewrite <- (Rmult_1_r (k^p)) at 2.
apply Rmult_le_compat_l.
left; now apply pow_lt.
apply Rplus_le_reg_l with (-1).
ring_simplify.
rewrite <- Ropp_0.
apply Ropp_le_contravar.
left; now apply pow_lt.
rewrite Hn.
apply dist_iter_aux_phi with P; try assumption.
auto with arith.
Qed.

Variable f: X X.
Variable phi: X Prop.

Hypothesis phi_f: x:X, phi x phi (f x).

Hypothesis phi_distanceable:
    (x y:X), phi x phi y M, 0 M ball x M y.

Lemma dist_iter_aux_zero_phi : (a:X) p m,
    phi a
    is_Lipschitz_phi f 0 phi
    (0 < p)%nat (0 < m)%nat
   ball (iter f p a) 0 (iter f m a).
Proof.
intros a p m phi_a (_,H) Hp Hm.
case_eq p.
intros V; rewrite V in Hp; now contradict Hp.
intros n1 Hn1.
case_eq m.
intros V; rewrite V in Hm; now contradict Hm.
intros n2 Hn2.
simpl.
destruct (phi_distanceable (iter f n1 a) (iter f n2 a)) as (M,(HM1,HM2)).
now apply phi_iter_f.
now apply phi_iter_f.
replace 0 with (0*(M+1)) by ring.
apply H; try assumption.
apply Rle_lt_trans with (M+0).
now rewrite Rplus_0_r.
apply Rplus_lt_compat_l, Rlt_0_1.
apply phi_iter_f.
trivial.
trivial.
apply phi_iter_f.
trivial.
trivial.
apply ball_le with M; try assumption.
apply Rle_trans with (M+0).
right; ring.
apply Rplus_le_compat_l, Rle_0_1.
Qed.

Lemma dist_iter_gen_phi : a k p m n D, 0 k < 1 is_Lipschitz_phi f k phi
   phi a
   0 < D ball a D (f a) (n p)%nat (n m)%nat (0 < n)%nat
    ball (iter f p a) (k^n/(1-k) ×D) (iter f m a).
Proof.
intros a k p m n D (H1,H1') H2 Phi_a H3 H4 Hp Hm Hn.
case H1; intros P0.
case (Nat.le_gt_cases p m); intros H5.
replace m with (p+(m-p))%nat.
apply ball_le with (k^p/(1-k) ×D).
apply Rmult_le_compat_r.
now left.
unfold Rdiv; apply Rmult_le_compat_r.
left; apply Rinv_0_lt_compat.
now apply Rlt_0_minus.
apply Rle_pow_le; try assumption.
split; try left; try assumption.
apply dist_iter_phi with phi; try assumption.
split; assumption.
intros p0.
apply phi_iter_f.
trivial.
trivial.
now rewrite Nat.add_comm, Nat.sub_add.
apply ball_sym.
replace p with (m+(p-m))%nat.
apply ball_le with (k^m/(1-k) ×D).
apply Rmult_le_compat_r.
now left.
unfold Rdiv; apply Rmult_le_compat_r.
left; apply Rinv_0_lt_compat.
now apply Rlt_0_minus.
apply Rle_pow_le; try assumption.
split; try left; assumption.
apply dist_iter_phi with phi; try assumption.
split; assumption.
intros p0.
apply phi_iter_f; trivial.
now rewrite Nat.add_comm, Nat.sub_add; [idtac | apply Nat.lt_le_incl].
apply ball_le with 0.
rewrite <- P0.
rewrite pow_i; try assumption.
right; unfold Rdiv; ring.
apply dist_iter_aux_zero_phi; try assumption.
now rewrite P0.
now apply Nat.lt_le_trans with n.
now apply Nat.lt_le_trans with n.
Qed.

End iter_dist_sub.

Fixed Point Theorem with subsets

Section FixedPoint_2_sub.

Context {X : CompleteSpace}.

Variable (f:XX).

Variable phi: X Prop.

Hypothesis phi_f: x:X, phi x phi (f x).
Hypothesis phi_distanceable:
    (x y:X), phi x phi y M, 0 M ball x M y.
Hypothesis phi_c : my_complete phi.

Lemma FixedPoint_uniqueness_weak_phi : a b, is_contraction_phi f phi
       phi a phi b
       close (f a) a close (f b) b
        close a b.
Proof.
intros a b (k,(Hk1,(Hk2,Hf))) Phi_a Phi_b Ha Hb eps.
destruct (phi_distanceable a b) as (M,(HM1,HM2)); try assumption.
destruct HM1.
pose (k' := (k + 1)/2).
assert (k < k').
unfold k'; apply Rmult_lt_reg_l with 2%R.
apply Rlt_0_2.
apply Rplus_lt_reg_l with (-k).
replace (-k+2×k) with k by ring.
replace (-k + 2 × ((k + 1) / 2)) with 1 by field.
assumption.
assert (0 < k' < 1).
split.
apply Rle_lt_trans with k; assumption.
unfold k'; apply Rmult_lt_reg_l with 2%R.
apply Rlt_0_2.
apply Rplus_lt_reg_l with (-1).
replace (-1+2×1) with 1 by ring.
replace (-1 + 2 × ((k + 1) / 2)) with k by field.
assumption.
destruct (contraction_lt_any k' (eps/M)) as (N,HN).
now (split; try left).
apply Rdiv_lt_0_compat; trivial.
destruct eps; simpl; easy.
apply ball_le with (M×k'^N).
apply Rmult_le_reg_r with (/M).
now apply Rinv_0_lt_compat.
left; apply Rle_lt_trans with (2:=HN).
right; field.
now apply Rgt_not_eq.
clear HN; induction N.
simpl; rewrite Rmult_1_r.
assumption.
assert (L:(0 < M×k'^S N*(k'-k)/2)).
apply Rdiv_lt_0_compat; try apply Rlt_0_2.
apply Rmult_lt_0_compat.
apply Rmult_lt_0_compat; try assumption.
now apply pow_lt.
now apply Rlt_0_minus.
specialize (Ha (mkposreal _ L)).
specialize (Hb (mkposreal _ L)).
apply ball_le with ((M × k' ^ (S N) × (k' - k) / 2) + ((k*(M × k' ^ N)) + (M × k' ^ (S N) × (k' - k) / 2))).
simpl.
apply Rle_trans with ((k'*(k' - k) + k)*M×k'^N).
right; field.
apply Rle_trans with (k'×M×k'^N).
2: right; ring.
apply Rmult_le_compat_r.
left; now apply pow_lt.
apply Rmult_le_compat_r.
now left.
apply Rplus_le_reg_l with (-k'*(k'-k)-k).
apply Rle_trans with 0.
right; ring.
apply Rle_trans with (Rsqr ((k-1)/2)).
apply Rle_0_sqr.
right; unfold Rsqr, k'.
field.
apply ball_triangle with (f a).
apply ball_sym, Ha.
apply ball_triangle with (f b).
apply Hf; try assumption.
apply Rmult_lt_0_compat; try assumption.
now apply pow_lt.
apply Hb.
apply ball_le with M; try assumption.
rewrite <- H; destruct eps; simpl; left; easy.
Qed.

Lemma Fixed_Point_aux_Proper_phi : (a:X),
    ProperFilter (fun Peventually (fun nP (iter f n a))).
Proof.
intros a; split.
intros P (N,HN).
(iter f N a).
apply HN.
apply le_n.
split.
0%nat; easy.
intros P Q (N1,H1) (N2,H2).
(max N1 N2).
intros n Hn; split.
apply H1.
apply Nat.le_trans with (2:=Hn).
apply Nat.le_max_l.
apply H2.
apply Nat.le_trans with (2:=Hn).
apply Nat.le_max_r.
intros P Q H (N,HN).
N.
intros n Hn.
apply H.
now apply HN.
Qed.

Lemma Fixed_Point_aux_cauchy_phi : (a:X), is_contraction_phi f phi
    phi a cauchy (fun Peventually (fun nP (iter f n a))).
intros a (k,(Hk1,(Hk2,Hf))) Phi_a.
generalize (@cauchy_distance X _ (Fixed_Point_aux_Proper_phi a)).
unfold cauchy; intros (_,T); apply T; clear T.
intros eps.
destruct (phi_distanceable a (f a)) as (M,(HM1,HM2)).
assumption.
now apply phi_f.
destruct HM1.
destruct (contraction_lt_any' k (eps/M*(1-k)*/3)) as (n,(Hn',Hn)).
now split.
apply Rmult_lt_0_compat.
apply Rmult_lt_0_compat.
apply Rdiv_lt_0_compat; trivial.
destruct eps; now simpl.
now apply Rlt_0_minus.
apply Rinv_0_lt_compat.
apply Rplus_lt_0_compat; try apply Rlt_0_1; apply Rlt_0_2.
(fun x m:nat, (n m)%nat close x (iter f m a)).
split.
n.
intros l Hl.
l; split; try easy.
intros E; apply ball_center.
intros u v (n1,(Hn1,Hu)) (n2,(Hn2,Hv)).
assert (L:(0 < eps/3)).
apply Rdiv_lt_0_compat.
destruct eps; now simpl.
apply Rplus_lt_0_compat; try apply Rlt_0_1; apply Rlt_0_2.
pose (e:=mkposreal _ L).
replace (pos eps) with (pos e+(pos e+pos e))%R by (simpl;field).
apply ball_triangle with (iter f n1 a).
apply Hu.
apply ball_triangle with (iter f n2 a).
2: apply ball_sym, Hv.
apply ball_le with (k ^ n / (1 - k) × M).
unfold e; simpl.
apply Rmult_le_reg_l with (/M).
now apply Rinv_0_lt_compat.
apply Rmult_le_reg_l with (1-k).
now apply Rlt_0_minus.
apply Rle_trans with (eps / M × (1 - k) × / 3).
2: right; unfold Rdiv; ring.
left; apply Rle_lt_trans with (2:=Hn).
right; field.
split; apply Rgt_not_eq; try assumption.
now apply Rlt_0_minus.
apply dist_iter_gen_phi with phi; try assumption.
now split.
now split.
rewrite <- H in HM2.
assert ( n, close (iter f n a) a).
apply nat_ind_strong with (P:= fun nclose (iter f n a) a).
intros n; case n.
simpl; intros _.
intros e; apply ball_center.
clear n; intros n; case n.
intros _; simpl.
intros e; apply ball_sym, ball_le with 0; try assumption.
destruct e; left; now simpl.
clear n; intros n IH.
apply close_trans with (iter f (S n) a).
2: apply IH.
2: apply le_n.
simpl; intros e.
apply ball_le with (k×e).
rewrite <- (Rmult_1_l e) at 2.
apply Rmult_le_compat_r.
destruct e; left; now simpl.
now left.
apply Hf.
apply cond_pos.
apply phi_iter_f.
intros x Hx.
apply phi_f; trivial.
apply phi_f; trivial.
apply phi_iter_f.
apply phi_f; trivial.
trivial.
assert (L:(close (iter f (S n) a) (iter f n a))).
apply close_trans with a.
apply IH.
apply le_n.
apply close_sym.
apply IH.
apply le_S, le_n.
apply L.
(fun xclose x a).
split.
0%nat.
intros n _; apply H0.
intros u v Hu Hv.
assert (close u v).
apply close_trans with a; try assumption.
now apply close_sym.
apply H1.
Qed.

Lemma FixedPoint_aux1_phi : (a:X), is_contraction_phi f phi phi a
  let x := lim (fun Peventually (fun nP (iter f n a))) in
      close (f x) x.
Proof.
intros a Hf Phi_a x.
generalize (complete_cauchy
   (fun Peventually (fun nP (iter f n a)))
    (Fixed_Point_aux_Proper_phi a)
    (Fixed_Point_aux_cauchy_phi _ Hf Phi_a)).
replace ((Hierarchy.lim
         (fun P : X Propeventually (fun n0 : natP (iter f n0 a))))) with x by reflexivity.
intros H eps.
pose (e2 :=mkposreal _ (is_pos_div_2 eps)).
specialize (H e2).
destruct H as (n,Hn).
replace (pos eps) with (pos e2 + pos e2).
2: simpl; field.
apply ball_sym.
apply ball_triangle with (iter f (S n) a).
apply Hn.
apply le_S, le_n.
generalize Hf; intro Hf'.
destruct Hf as (k,(Hk1,(Hk2,Hk3))).
apply ball_le with (k×e2).
rewrite <- (Rmult_1_l e2) at 2.
apply Rmult_le_compat_r.
destruct e2; left; now simpl.
now left.
simpl.
apply Hk3.
apply (cond_pos e2).
apply phi_iter_f.
intros xx Hxx.
apply phi_f; trivial.
trivial.
unfold x.
unfold my_complete in phi_c.
apply phi_c.
apply Fixed_Point_aux_Proper_phi.
apply Fixed_Point_aux_cauchy_phi.
trivial.
trivial.
intros P Hev.
intro.
apply H.
unfold eventually in Hev.
destruct Hev as (N,Hev).
specialize (Hev (N+1)%nat).
assert (Hev' : P (iter f (N+1) a)).
apply Hev.
auto with arith.
(iter f (N+1) a).
split; try assumption.
apply phi_iter_f.
trivial.
trivial.
apply ball_sym.
apply Hn.
apply le_n.
Qed.

Hypothesis phi_X_not_empty: (a:X), phi a.
Hypothesis phi_closed: my_complete phi.

Lemma FixedPoint_aux2_phi : (a:X), is_contraction_phi f phi phi a
  let x := lim
  (fun Peventually (fun nP (iter f n a))) in
      phi x.
Proof.
intros a Hf Phi_a x.
apply phi_closed.
apply Fixed_Point_aux_Proper_phi.
now apply Fixed_Point_aux_cauchy_phi.
intros P (N,HN).
intros K; apply K.
(iter f N a).
split.
apply HN.
apply le_n.
now apply phi_iter_f.
Qed.

Theorem FixedPoint_C_phi : is_contraction_phi f phi
    a:X,
     phi a
       close (f a) a
       ( b, phi b close (f b) b close b a)
     x, phi x close (lim (fun Peventually (fun nP (iter f n x)))) a.
Proof.
intros Hf.
destruct phi_X_not_empty as (a, Ha).
(lim (fun Peventually (fun nP (iter f n a)))).
split.
now apply FixedPoint_aux2_phi.
split.
now apply FixedPoint_aux1_phi.
split.
intros b Phi_b Hb.
apply FixedPoint_uniqueness_weak_phi; try assumption.
now apply FixedPoint_aux2_phi.
now apply FixedPoint_aux1_phi.
intros x Phi_x.
apply FixedPoint_uniqueness_weak_phi; try assumption.
now apply FixedPoint_aux2_phi.
now apply FixedPoint_aux2_phi.
now apply FixedPoint_aux1_phi.
now apply FixedPoint_aux1_phi.
Qed.

End FixedPoint_2_sub.