Library Coqtail.Reals.RIVT

Require Import Rbase.
Require Export Rsequence.
Require Import Ranalysis.
Require Import Rfunctions.
Require Import Rseries_def.
Require Import Fourier.
Require Import RiemannInt.
Require Import SeqProp.
Require Import MyRIneq.
Require Import Rinterval Ranalysis_def Ranalysis_def_simpl.
Require Import Ranalysis_continuity.
Require Import Ass_handling.

Local Open Scope R_scope.

Intermediate Value Theorem on an Interval and its corollary

This proof was mainly taken from Reals.Rsqrt_def

Lemma dicho_steps_interval_compat : x y P N, x y
interval x y (dicho_up x y P N)
interval x y (dicho_lb x y P N).
Proof.
intros x y P N x_le_y ; induction N.
simpl ; split ; [apply interval_r | apply interval_l] ; assumption.
simpl ; split ; fold (middle (Dichotomy_lb x y P N) (Dichotomy_ub x y P N)) ;
destruct (P (middle (Dichotomy_lb x y P N) (Dichotomy_ub x y P N))) ;
try apply interval_middle_compat ; apply IHN.
Qed.

Lemma dicho_interval_compat : x y l P, x y
Rseq_cv (dicho_up x y P) linterval x y l.
Proof.
intros x y l P x_le_y Hl ; eapply Rseq_interval_compat ;
[| eassumption] ; intro ; apply dicho_steps_interval_compat ;
assumption.
Qed.

Lemma cond_positivity_car: x,
cond_positivity x = true 0 x.
Proof.
intro ; unfold cond_positivity ; destruct (Rle_dec 0 x) ;
intuition ; discriminate.
Qed.

Lemma cond_positivity_car': x,
cond_positivity x = false x < 0.
Proof.
intro ; unfold cond_positivity ; destruct (Rle_dec 0 x) ; intuition.
discriminate.
destruct (Rlt_irrefl 0) ; eapply Rle_lt_trans ; eassumption.
Qed.

Lemma Rseq_cv_0_abs_compat : Un,
Rseq_cv (| Un |) 0 → Rseq_cv Un 0.
Proof.
intros Un HUn eps eps_pos ; destruct (HUn _ eps_pos) as [N HN] ;
N ; intros n n_lb ; apply Rle_lt_trans with (R_dist (|Un| n)%R 0).
right ; unfold R_dist, Rseq_abs ; do 2 rewrite Rminus_0_r ;
rewrite Rabs_Rabsolu ; reflexivity.
apply HN ; assumption.
Qed.

Lemma dicho_diff_cv : x y P, x y
Rseq_cv (dicho_up x y P - dicho_lb x y P) 0.
Proof.
intros x y P xley ; eapply Rseq_cv_eq_compat.
intro n ; apply dicho_lb_dicho_up ; assumption.
eapply Rseq_cv_pos_infty_div_compat, Rseq_constant_cv.
apply Rseq_pow_gt_1_cv ; fourier.
Qed.

Lemma interval_open_interval : x y z,
interval x y zx zy z
open_interval x y z.
Proof.
intros x y z [xz zy] x_neq y_neq ; split ;
apply Rle_neq_lt ; auto.
Qed.

Lemma IVT_open_interval_prelim : (f : RR) (x y : R),
continuity_interval x y fx < yopen_interval (f x) (f y) 0 →
{z : R | open_interval x y z f z = 0}.
Proof.
intros f x y Hf xlty O_in ; assert (xley := Rlt_le _ _ xlty) ;
pose (P := fun zcond_positivity (f z)) ; pose (Zn := dicho_up x y P) ;
pose (Zn' := dicho_lb x y P) ; assert (Hcv := dicho_diff_cv _ _ P xley) ;
destruct (dicho_up_cv x y P xley) as [z Hz] ; z.
assert (Hz' : Rseq_cv Zn' z).
destruct (dicho_lb_cv x y P xley) as [z' Hz'] ;
rewrite <- (cv_dicho _ _ _ _ _ xley Hz' Hz) ; assumption.
assert (fz_eq : f z = 0).
apply Rle_antisym.

apply Rseq_negative_limit with (fun nf (Zn' n)).
intro n ; left ; rewrite <- cond_positivity_car' ; fold (P (Zn' n)) ;
apply dicho_lb_car ; unfold P ; rewrite cond_positivity_car' ; apply O_in.

eapply Rseq_cv_continuity_interval_compat ; [eapply dicho_interval_compat |
intro ; apply dicho_steps_interval_compat | |] ; eassumption.

apply Rseq_positive_limit with (fun nf (Zn n)).
intro n ; rewrite <- cond_positivity_car ; fold (P (Zn n)) ;
apply dicho_up_car ; unfold P ; rewrite cond_positivity_car ;
left ; apply O_in.
eapply Rseq_cv_continuity_interval_compat ; [eapply dicho_interval_compat |
intro ; apply dicho_steps_interval_compat | |] ; eassumption.

split ; [apply interval_open_interval | assumption].
eapply dicho_interval_compat ; eassumption.
intro Hfalse ; rewrite Hfalse in O_in ; apply (Rlt_irrefl 0) ;
apply Rle_lt_trans with (f z) ; [right ; symmetry ; apply fz_eq | apply O_in].
intro Hfalse ; rewrite Hfalse in O_in ; apply (Rlt_irrefl 0) ;
apply Rlt_le_trans with (f z) ; [apply O_in | right ; apply fz_eq].
Qed.

Lemma IVT_open_interval : (f : RR) (x y : R) l,
continuity_interval x y fx < yopen_interval (f x) (f y) l
{ z : R | open_interval x y z f z = l }.
Proof.
intros f x y l Hf Hxy Hl ;
destruct IVT_open_interval_prelim with (f - (fun _l))%F x y as [z [z_in Hz]].
apply continuity_in_minus, continuity_in_const ; assumption.
assumption.
clear - Hl; destruct Hl ; split ; unfold minus_fct ; fourier.
z ; split ; [assumption |].
clear - Hz ; unfold minus_fct in × ; intuition.
Qed.

Lemma IVT_interval : (f : RR) (x y : R) l,
continuity_interval x y fx yinterval (f x) (f y) l
{z : R | interval x y z f z = l}.
Proof.
intros f x y l Hf xley [fxlel llefy] ;
destruct (Rle_lt_or_eq_dec _ _ xley) as [xlty | xeqy].
destruct (Rle_lt_or_eq_dec _ _ fxlel) as [fxltl | fxeql].
destruct (Rle_lt_or_eq_dec _ _ llefy) as [lltfy | leqfy].
destruct (IVT_open_interval _ _ _ l Hf xlty) as [z [z_in Hz]].
split ; assumption.
z ; split ; [apply open_interval_interval |] ; assumption.
y ; split ; [apply interval_r |] ; auto.
x ; split ; [apply interval_l |] ; auto.
y ; subst ; split ; [apply interval_r | apply Rle_antisym] ; auto.
Qed.