CoRN.examples.Picard

Require Import CRtrans.
Require Import Qmetric.


Section ODE.
Open Scope uc_scope.
Require Import ProductMetric CompleteProduct.
Require Import Unicode.Utf8.
Require Import CPoly_Newton.
Require Import metric2.Classified.
Require Import Circle.
Notation "X * Y":=(ProductMS X Y).
Notation " f >> g ":= (Cbind_slow f ∘ g) (at level 50).
Notation " x >>= f ":= (Cbind_slow f x) (at level 50).

Section Picard_op.
Require Import AbstractIntegration.

Variable v: (Q×Q) -->CR.
Variable f:Q-->CR.
Notation "( f , g )":= (together f g).
Definition vxfx:= (v >> Couple ∘ (Cunit, f) ∘ diag _).

Require Import SimpleIntegration.


Definition integral: ((Q-->CR) × Q × Q) → CR.
intros [[g a] b].
destruct (QMinMax.Qlt_le_dec_fast b a).
assert (a_min_b:Qpos). ∃ (a-b) . admit.
exact (- ∫ g b (a_min_b))%CR.

assert (b_min_a:Qpos). ∃ (b-a). admit.
exact ( ∫ g a (b_min_a))%CR.
Defined.



Definition Picard_raw:=fun t:Q ⇒ integral (f, 0, t).

Lemma Picard_uc: (is_UniformlyContinuousFunction Picard_raw (fun e ⇒ e)%Qpos).
admit.
Qed.

Definition Picard:=(Cbind_slow (Build_UniformlyContinuousFunction Picard_uc)).
End Picard_op.

Section Banach_it.
Context {X} `(F:X-->X).
Fixpoint Banach_seq (n : nat) : X --> X :=
         match n with
         | O ⇒ F
         | S m ⇒ F ∘ (Banach_seq m)
         end.

Variable f:CR-->CR.
Check Picard.
Fixpoint Picard_seq (n : nat) : Q --> CR :=
         match n with
         | O ⇒ f ∘ Cunit
         | S m ⇒ (Picard (Picard_seq m) )∘ Cunit
         end.
End Banach_it.

Section Picard.
Variable L:Qpos.
Variable c:Qpos.
Hypothesis c_unit:1-c>0.
Program Definition oneminc:=(1-c):Qpos.
Next Obligation.
admit.
Defined.
Variables a K:Q.
Hypothesis aL_le_c:(a×L<c).
Require Import Qabs.
Require Export CRabs.
Require Import Interval.

Variable v: (Q×Q) -->CR.

Hypothesis Lipschitz: ∀ x, -a≤x → x≤a → ∀ y, -K≤y → y≤K →
  ∀ y':Q, -K≤y' → y ≤K →
 ((CRabs ((v (x, y)) - (v (x, y'))))<= 'L× 'Qabs (y-y'))%CR.

Section BanachFPT.
Context (X: MetricSpace).
Context (d:X→X→CR).

Variable metric_function: ∀ e x y, ball e x y ↔ ((d x y) <='e)%CR.
Class Contraction `(F:X-->X)`(c:Qpos):= contraction:
  c<1-> ∀ x x', ((d x x') ≤ 'c*(d (F x) (F x')))%CR.

Context {F}`{conF: Contraction F}.
Require Export CRGeometricSum.


Lemma bla: ∀ n m:nat, ∀ x:X,
  (ball (c^m) (@Banach_seq _ F n x) (@Banach_seq _ F (n+m) x)).
Admitted.

Lemma bla2: ∀ n:nat, ∀ x:X, (ball (Qpos_inv oneminc) x (@Banach_seq _ F n x)).
Admitted.

Lemma bla3: ∀ n m:nat, ∀ x:X, ∀ e,
  (ball e x (F x)) →
  (ball (c^m*(Qpos_inv oneminc)*e) (@Banach_seq _ F n x) (@Banach_seq _ F m x)).
Admitted.

Variable x:X.
Definition DiffSeries:=fun n ⇒ d (@Banach_seq _ F n x) (@Banach_seq _ F (S n) x).
Require Import StreamMemo.
Definition DiffStream:=(memo_list _ DiffSeries).
Require Import Streams.

Definition GeometricSeriesCR (c:CR):=
  (ForAll (fun s:Stream CR ⇒ (CRabs ((hd (tl s))) ≤ c*(CRabs(hd s)))%CR)).

Lemma GeomDiff:GeometricSeriesCR ('c)%CR DiffStream.
unfold GeometricSeriesCR.
unfold DiffStream.
unfold memo_list.
unfold memo_make.
simpl.
admit.
Qed.



Lemma BanachCauchy: ∀ ϵ:Qpos, ∃ N, ∀ n m:nat , n ≥N→ m≥ N →
   (ball ϵ (@Banach_seq _ F n x) (@Banach_seq _ F m x)).
intros.
set ceil:=(Qabs (approximate (d (@Banach_seq _ F 0 x) (@Banach_seq _ F 1 x))
  (Qpos2QposInf (1#1))))+1:Qpos.

∃ ( /((ϵ×oneminc/ceil)(oneminc))).


End BanachFPT.

Section BanachFPT2.
Context {X} (F:Complete X--> Complete X) `{conF: Contraction (Complete X) F}.
Theorem BanachFPT : ∃ x, (F x) =x.
eexists y.
Admitted.


Theorem PicardFPT: ∃ f, (Picard f) = (f ∘ Cunit).
apply BanachFPT.
Qed.