picard.v

Require Import Utf8.

(*

  F⁰, F¹, F², F³, ...

  (0,1) (1,2) (2,3) (3,4)

  map ∥·∥ (F_n - F_m)

  Σⁿ := sum (take n ...)

  Lemma cauchy : ∀ε, ∀N, ∀m≥N,  ∥ Σ^m - Σ^(N+1) ∥ ≤ ε

  Lemma has_precision n : Σⁿ = x - Fⁿ⁺¹ x

*)

Require Import series canonical_names abstract_algebra streams vectorspace.

(** Operators on a banach/vector/normed space *)
Section operators.

Class Operator V W := T: V → W. (*.. hmm ..*)

Section contraction_operator.
 Context `{SemiNormedSpace K V} `{Lt K}.
 Context (q:K) `{PropHolds (0 < q < 1)}. (* Lipschitz constant *)
 Class Contraction (T:V → V) := contraction: ∀ v, ∥T v∥ ≤ q * ∥v∥.
End contraction_operator.

Section bounded_operator.
 Context {K X Y} `{Lt K} `{Le K} `{Zero K} `{Mult K} {nx:Norm K X} {ny:Norm K Y}.
 Context (M:K) `{PropHolds (0 < M)}.
 Notation "'norm_X'" := (@norm _ _ nx).
 Notation "'norm_Y'" := (@norm _ _ ny).
 Class Bounded (T:X → Y) := bounded: ∀ v, norm_Y (T v) ≤ M * norm_X v.
End bounded_operator.

End operators.

Section metricspace.
(* Normed space implies metric space *)
Context `{SemiNormedSpace K V}.
Definition induced_metric (x y:V) := ∥ x & (-y) ∥.
Require Import Metric.

(* TODO show that we have a metric space
Record MetricSpace : Type := Build_MetricSpace
  { msp_is_setoid : RSetoid;
    ball : Qpos → msp_is_setoid → msp_is_setoid → Prop;
    ball_wd : ∀ e1 e2 : Qpos,
              QposEq e1 e2
              → (∀ x1 x2 : msp_is_setoid,
                 st_eq x1 x2
                 → (∀ y1 y2 : msp_is_setoid,
                    st_eq y1 y2 → (ball e1 x1 y1 ↔ ball e2 x2 y2)));
    msp : is_MetricSpace msp_is_setoid ball }
Record RSetoid : Type := Build_RSetoid
  { st_car : Type;  st_eq : Equiv st_car;  st_isSetoid : Setoid st_car }
*) 

Require Import UniformContinuity.

Open Scope uc_scope.
Notation "x ⟼ y" := (fun x => y) (at level 40).

Section test.
  Parameter X : MetricSpace.
  Parameter F : X --> X.
  Implicit Arguments iter [A].
  Definition Banach_iter n := iter n (f ⟼ (F ∘ f)) F.
(*  Definition Banach_iter n := iter n (λ f, F ∘ f) F. *)
End test.

Print Banach_iter.
(*
   Banach_iter = λ n : Z, iter n (X --> X) (λ f : X --> X, F ∘ f) F
     : Z → X --> X

   Banach_iter = n ⟼ iter n (X --> X) (f ⟼ (F ∘ f)) F
     : Z → X --> X
*)

Section norm.
Parameter norm : X → Q.

Definition is_Contraction O : Prop := ∥ O ∥ < 1.



Lemma fooo : Setoid_Theory V Veq.
Print Setoid_Theory.

Require Import Complete.
Context {K V} `{SemiNormedSpace K V}.
Check Complete.
Class BanachSpace K (Complete V) :=
  ba_seminormed :> @SemiNormedSpace K V.





Section banach_sequence.

 (** The sequence (0,1) (1,2) (2,3) ... *)
 Context `{SemiGroup}.
 CoFixpoint pairseq n := Cons (n, n + 1) $ pairseq (n + 1).

 (** (n,m) ⟼ (λ x, ∥ T^m x - T^n x ∥) *)

 Context `(T:V → V).

 Definition operatormap `{Contraction T} t := λ a, ∥ T^(fst t) a - (snd t) a ∥.
 
 (* id, T, T∘T, T∘T∘T, ... *)
 Definition T_inf := [T]∞.


Section banach_space.
(** We defined a banach space as the completion of a seminormed space *)




End banach_space.

Section banach_fpt.

(** Banach Fixed Point theorem.

    Let (X,d) be a complete, non-empty metric space (X,d) and T a contraction map X → X.

    (B1). The map T admits one and only one fixed point x_inf ∈ X.
    (B2). This point can be found by iterating T, ie. lim n→∞, Tⁿ(x) = x_inf
    (B3). The speed of convergence is: d(x_inf, x_n) ≤ (qⁿ / (1-q)) * d(x₀, x₁)
*)

Context `{Contraction T}.
Context `{SemiNormedSpace

Lemma banach_fpt_exist : 
Lemma conv_speed : d xinf xn ≤ (q ^ n) / (1 - q) * (d x₁ x₀).

End banach_fpt.