Library Top.fixed_point

This file is part of the Elfic 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.

Require Export Reals Coquelicot.Coquelicot.
Require Export R_compl.
Require Export logic_tricks.

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).

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).

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).

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).

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).

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).

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 (fun x~~ phi x).

End closed_compl.

Section closed_compl2.

Context {X : CompleteNormedModule R_AbsRing}.

Variable phi: X Prop.

Lemma my_complete_closed:
   my_complete (fun x~~ phi x) closed phi.

End closed_compl2.

Fixed Point Theorem

Section FixedPoint_2.

Context {X : CompleteSpace}.

Definition is_eq : X X Prop := fun a b eps:posreal, ball a eps b.

Lemma is_eq_trans: x y z, is_eq x y is_eq y z is_eq x z.

Lemma is_eq_sym: x y, is_eq x y is_eq y x.

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
       is_eq (f a) a is_eq (f b) b
        is_eq a b.

Lemma Fixed_Point_aux_Proper: (a:X),
    ProperFilter (fun Peventually (fun nP (iter f n a))).

Lemma Fixed_Point_aux_cauchy: (a:X), is_contraction f
    phi a cauchy (fun Peventually (fun nP (iter f n a))).

Lemma FixedPoint_aux1: (a:X), is_contraction f phi a
  let x := lim (fun Peventually (fun nP (iter f n a))) in
      is_eq (f x) x.

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.

Theorem FixedPoint_C: is_contraction f
    a:X,
     phi a
       is_eq (f a) a
       ( b, phi b is_eq (f b) b is_eq b a)
     x, phi x is_eq (lim (fun Peventually (fun nP (iter f n x)))) a.

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.

Lemma is_eq_eq: (x y:X), is_eq x y x = y.

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.

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).

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).

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).

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).

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).

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
       is_eq (f a) a is_eq (f b) b
        is_eq a b.

Lemma Fixed_Point_aux_Proper_phi : (a:X),
    ProperFilter (fun Peventually (fun nP (iter f n a))).

Lemma Fixed_Point_aux_cauchy_phi : (a:X), is_contraction_phi f phi
    phi a cauchy (fun Peventually (fun nP (iter f n a))).

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
      is_eq (f x) x.

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.

Theorem FixedPoint_C_phi : is_contraction_phi f phi
    a:X,
     phi a
       is_eq (f a) a
       ( b, phi b is_eq (f b) b is_eq b a)
     x, phi x is_eq (lim (fun Peventually (fun nP (iter f n x)))) a.

End FixedPoint_2_sub.