Banach fixed point theorem

CHANGELOG_UNRELEASED.md

@@ -11,6 +11,19 @@
   + lemmas `ltNye_eq`, `sube_lt0`, `subre_lt0`, `suber_lt0`, `sube_ge0`
   + lemmas `dsubre_gt0`, `dsuber_gt0`, `dsube_gt0`, `dsube_le0`
 
+- in `topology.v`:
+  + lemma `near_inftyS`
+- in `sequences.v`:
+  + lemmas `contraction_dist`, `contraction_cvg`,
+    `contraction_cvg_fixed`, `banach_fixed_point`,
+    `contraction_unique`
+- in `mathcomp_extra.v`:
+  + defintion `onem` and notation ``` `1- ```
+  + lemmas `onem0`, `onem1`, `onemK`, `onem_gt0`, `onem_ge0`, `onem_le1`, `onem_lt1`,
+    `onemX_ge0`, `onemX_lt1`, `onemD`, `onemMr`, `onemM`
+- in `signed.v`:
+  + lemmas `onem_PosNum`, `onemX_NngNum`
+
 ### Changed
 
 ### Renamed

theories/mathcomp_extra.v

@@ -739,3 +739,51 @@ Arguments bigminD1 {d T I x} j.
 Arguments bigmin_inf {d T I x} j.
 Arguments bigmin_eq_arg {d T I} x j.
 Arguments eq_bigmin {d T I x} j.
+
+Reserved Notation "`1- r" (format "`1- r", at level 2).
+
+Section onem.
+Variable R : numDomainType.
+Implicit Types r : R.
+
+Definition onem r := 1 - r.
+Local Notation "`1- r" := (onem r).
+
+Lemma onem0 : `1-0 = 1. Proof. by rewrite /onem subr0. Qed.
+
+Lemma onem1 : `1-1 = 0. Proof. by rewrite /onem subrr. Qed.
+
+Lemma onemK r : `1-(`1-r) = r.
+Proof. by rewrite /onem opprB addrCA subrr addr0. Qed.
+
+Lemma onem_gt0 r : r < 1 -> 0 < `1-r. Proof. by rewrite subr_gt0. Qed.
+
+Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r.
+Proof. by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed.
+
+Lemma onem_le1 r : 0 <= r -> `1-r <= 1.
+Proof. by rewrite ler_subl_addr ler_addl. Qed.
+
+Lemma onem_lt1 r : 0 < r -> `1-r < 1.
+Proof. by rewrite ltr_subl_addr ltr_addl. Qed.
+
+Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n).
+Proof. by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed.
+
+Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1.
+Proof. by move=> ?; rewrite onem_lt1// exprn_gt0. Qed.
+
+Lemma onemD r s : `1-(r + s) = `1-r - s.
+Proof. by rewrite /onem addrAC opprD addrA addrAC. Qed.
+
+Lemma onemMr r s : s * `1-r = s - s * r.
+Proof. by rewrite /onem mulrBr mulr1. Qed.
+
+Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s.
+Proof.
+rewrite /onem mulrBr mulr1 mulrBl mul1r opprB -addrA.
+by rewrite (addrC (1 - r)) !addrA subrK opprB addrA subrK addrK.
+Qed.
+
+End onem.
+Notation "`1- r" := (onem r) : ring_scope.

theories/sequences.v

@@ -2632,3 +2632,102 @@ by move/cvg_lim : ul => ->.
 Qed.
 
 End elim_sup_inf.
+
+Section banach_contraction.
+
+Context {R : realType} {X : completeNormedModType R} (U : set X).
+Variables (f : {fun U >-> U}).
+
+Section contractions.
+Variables (q : {nonneg R}) (ctrf : contraction q f) (base : X) (Ubase : U base).
+
+Lemma contraction_dist n m :
+  `| iter n f base - iter (n + m) f base| <=
+   (`|f base - base| / (1 - q%:num)) * q%:num ^+ n.
+Proof.
+case: ctrf => q1 ctrfq; pose y := fun n => iter n f base.
+have f1 k : `|y k.+1 - y k| <= q%:num ^+ k * `|f base - base|.
+  elim: k => [|k /(ler_wpmul2l [ge0 of q%:num])]; first by rewrite expr0 mul1r.
+  rewrite mulrA -exprS; apply: le_trans; rewrite ![y _.+1]iterS.
+  by apply: (ctrfq (iter k.+1 f base, _)); split; exact: funS.
+have /le_trans -> // : `| y n - y (n + m)%N| <=
+    series (geometric (`|f base - base| * q%:num ^+ n) q%:num) m.
+  elim: m => [|m ih].
+    by rewrite geometric_seriesE ?lt_eqF//= addn0 subrr normr0 subrr mulr0 mul0r.
+  rewrite (le_trans (ler_dist_add (y (n + m)%N) _ _))//.
+  apply: (le_trans (ler_add ih _)); first by rewrite distrC addnS; exact: f1.
+  rewrite [_ * `|_|]mulrC exprD mulrA geometric_seriesE ?lt_eqF//=.
+  rewrite -!/(`1-_) (onem_PosNum ctrf.1) (onemX_NngNum (ltW ctrf.1)).
+  rewrite -!mulrA -mulrDr ler_pmul// -mulrDr exprSr onemM -addrA.
+  rewrite -[in leRHS](mulrC _ `1-(_ ^+ m)) -onemMr onemK.
+  by rewrite [in leRHS]mulrDl mulrAC mulrV ?mul1r// unitf_gt0// onem_gt0.
+rewrite geometric_seriesE ?lt_eqF//=.
+rewrite -!/(`1-_) (onem_PosNum ctrf.1) (onemX_NngNum (ltW ctrf.1)).
+rewrite -!mulrA ler_pmul// [leRHS]mulrC ler_pmul// -ler_pdivl_mulr ?invr_gt0//.
+by rewrite divrr ?unitf_gt0// onem_le1.
+Qed.
+
+Lemma contraction_cvg : cvg (iter n f base @[n-->\oo]).
+Proof.
+apply/cauchy_cvgP; case: ctrf => q1 ctrfq.
+pose y := fun n => iter n f base; pose C := `|f base - base| / (1 - q%:num).
+apply/cauchy_ballP => _/posnumP[e]; near_simpl.
+have lt_min n m : `|y n - y m| <= C * q%:num ^+ minn n m.
+  wlog : n m / (n <= m)%N => W.
+    by case/orP: (leq_total n m) => /W //; rewrite distrC minnC.
+  rewrite -(@subnKC n m) //; apply: le_trans; first exact: contraction_dist.
+  by rewrite -/(`1-_) (onem_PosNum ctrf.1) ler_pmul ?subnKC//; move/minn_idPl : W => ->.
+have [Cpos| |C0] := ltrgt0P C; last first.
+  - near=> n m => /=; rewrite -ball_normE.
+    by apply: (le_lt_trans (lt_min _ _)); rewrite C0 mul0r.
+  - rewrite ltNge //; apply: contraNP => _; rewrite /C.
+    by rewrite -/(`1-_) (onem_PosNum ctrf.1).
+near=> n; rewrite -ball_normE /= (le_lt_trans (lt_min n.1 n.2)) //.
+rewrite // -ltr_pdivl_mull //.
+suff : ball 0 (C^-1 * e%:num) (q%:num ^+ minn n.1 n.2).
+  by rewrite /ball /= sub0r normrN ger0_norm.
+near: n; rewrite nbhs_simpl.
+pose g := fun w : nat * nat => q%:num ^+ minn w.1 w.2.
+have := @cvg_ball _ _ (g @ filter_prod \oo \oo) _ 0 _ (C^-1 * e%:num).
+move: (@cvg_geometric _ 1 q%:num); rewrite ger0_norm // => /(_ q1) geo.
+near_simpl; apply; last by rewrite mulr_gt0 // invr_gt0.
+apply/cvg_ballP => _/posnumP[delta]; near_simpl.
+have [N _ Q] : \forall N \near \oo, ball 0 delta%:num (geometric 1 q%:num N).
+  exact: (@cvg_ball R R _ _ 0 geo).
+exists ([set n | N <= n], [set n | N <= n])%N; first by split; exists N.
+move=> [n m] [Nn Nm]; rewrite /ball /= sub0r normrN ger0_norm /g //.
+apply: le_lt_trans; last by apply: (Q N) => /=.
+rewrite sub0r normrN ger0_norm /geometric //= mul1r.
+by rewrite ler_wiexpn2l // ?ltW // leq_min Nn.
+Unshelve. all: end_near. Qed.
+
+Lemma contraction_cvg_fixed :
+  closed U -> let p := lim ((fun n => iter n f base) @ \oo) in p = f p.
+Proof.
+move=> clU ; apply: cvg_lim => //; case: ctrf => q1 ctrfq.
+apply/cvg_distP => _/posnumP[e]; near_simpl; apply: near_inftyS.
+have [q_gt0 | | q0] := ltrgt0P q%:num.
+- near=> n => /=; apply: (le_lt_trans (ctrfq (_, _) _)) => //=.
+  + split; last exact: funS.
+    by apply: closed_cvg contraction_cvg => //; apply: nearW => ?; exact: funS.
+  + rewrite -ltr_pdivl_mull //; near: n; move/cvg_distP: contraction_cvg; apply.
+    by rewrite mulr_gt0 // invr_gt0.
+- by rewrite ltNge//; exact: contraNP.
+- apply: nearW => /= n; apply: (le_lt_trans (ctrfq (_, _) _)).
+  + split; last exact: funS.
+    by apply: closed_cvg contraction_cvg => //; apply: nearW => ?; exact: funS.
+  + by rewrite q0 mul0r.
+Unshelve. all: end_near. Qed.
+End contractions.
+
+Variable ctrf : is_contraction f.
+
+Theorem banach_fixed_point : closed U -> U !=set0 -> exists2 p, U p & p = f p.
+Proof.
+case: ctrf => q ctrq ? [base Ubase]; exists (lim (iter n f base @[n -->\oo])).
+  apply: closed_cvg (contraction_cvg ctrq Ubase) => //.
+  by apply: nearW => ?; exact: funS.
+exact: (contraction_cvg_fixed ctrq).
+Unshelve. all: end_near. Qed.
+
+End banach_contraction.

theories/signed.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
-Require Import boolp.
+Require Import boolp mathcomp_extra.
 
 (******************************************************************************)
 (* This file develops tools to make the manipulation of numbers with a known  *)
@@ -1141,8 +1141,6 @@ CoInductive nonneg_spec (R : numDomainType) (x : R) : R -> bool -> Type :=
 Lemma nonnegP (R : numDomainType) (x : R) : 0 <= x -> nonneg_spec x x (0 <= x).
 Proof. by move=> xge0; rewrite xge0 -[x]/(NngNum xge0)%:num; constructor. Qed.
 
-
-
 (* Section PosnumOrder. *)
 (* Variables (R : numDomainType). *)
 (* Local Notation nR := {posnum R}. *)
@@ -1168,3 +1166,20 @@ Proof. by move=> xge0; rewrite xge0 -[x]/(NngNum xge0)%:num; constructor. Qed.
 (* Canonical nonneg_orderType := OrderType nR nonneg_le_total. *)
 
 (* End NonnegOrder. *)
+
+(* These proofs help integrate more arithmetic with signed.v. The issue is    *)
+(* Terms like `0 < 1-q` with subtraction don't work well. So we hide the      *)
+(* subtractions behind `PosNum` and `NngNum` constructors, see sequences.v    *)
+(* for examples.                                                              *)
+Section onem_signed.
+Variable R : numDomainType.
+Implicit Types r : R.
+
+Lemma onem_PosNum r (r1 : r < 1) : `1-r = (PosNum (onem_gt0 r1))%:num.
+Proof. by []. Qed.
+
+Lemma onemX_NngNum r (r1 : r <= 1) (r0 : 0 <= r) n :
+  `1-(r ^+ n) = (NngNum (onemX_ge0 n r0 r1))%:num.
+Proof. by []. Qed.
+
+End onem_signed.

theories/topology.v

@@ -2127,6 +2127,10 @@ move=> N_gt0 P [n _ Pn]; exists (n * N)%N => //= m.
 by rewrite /= -leq_divRL//; apply: Pn.
 Qed.
 
+Lemma near_inftyS (P : set nat) : 
+  (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x).
+Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed.
+
 (** ** Topology on the product of two spaces *)
 
 Section Prod_Topology.