proposition: Lemma RiemannInt_P6 : forall (f:R -> R) (a b:R), a < b -> (forall x:R, a <= x <= b -> continuity_pt f x) -> Riemann_integrable f a b.
proof: Proof. intros; unfold Riemann_integrable; intro; assert (H1 : 0 < eps / (2 * (b - a))). { unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos eps) | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rlt_0_minus; assumption ] ]. } assert (H2 : Rmin a b = a). { apply Rlt_le in H. unfold Rmin; decide (Rle_dec a b) with H; reflexivity. } assert (H3 : Rmax a b = b). { apply Rlt_le in H. unfold Rmax; decide (Rle_dec a b) with H; reflexivity. } elim (Heine_cor2 H0 (mkposreal _ H1)); intros del H4; elim (SubEqui_P9 del f H); intros phi [H5 H6]; split with phi; split with (mkStepFun (StepFun_P4 a b (eps / (2 * (b - a))))); split. 2: rewrite StepFun_P18; unfold Rdiv; rewrite Rinv_mult. 2: do 2 rewrite Rmult_assoc; rewrite Rinv_l. 2: rewrite Rmult_1_r; rewrite Rabs_right. 2: apply Rmult_lt_reg_l with 2. 2: prove_sup0. 2: rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r. 2: rewrite Rmult_1_l; pattern (pos eps) at 1; rewrite <- Rplus_0_r; rewrite <-Rplus_diag; apply Rplus_lt_compat_l; apply (cond_pos eps). 2: discrR. 2: apply Rle_ge; left; apply Rmult_lt_0_compat. 2: apply (cond_pos eps). 2: apply Rinv_0_lt_compat; prove_sup0. 2: apply Rminus_eq_contra; red; intro; clear H6; rewrite H7 in H; elim (Rlt_irrefl _ H). intros; rewrite H2 in H7; rewrite H3 in H7; simpl; unfold fct_cte; cut (forall t:R, a <= t <= b -> t = b \/ (exists i : nat, (i < pred (length (SubEqui del H)))%nat /\ co_interval (pos_Rl (SubEqui del H) i) (pos_Rl (SubEqui del H) (S i)) t)). { intro; elim (H8 _ H7); intro. { rewrite H9; rewrite H5; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; left; assumption. } elim H9; clear H9; intros I [H9 H10]; assert (H11 := H6 I H9 t H10); rewrite H11; left; apply H4. - assumption. - apply SubEqui_P8; apply Nat.lt_trans with (pred (length (SubEqui del H))). { assumption. } apply Nat.lt_pred_l; red; intro; rewrite H12 in H9; elim (Nat.nlt_0_r _ H9). - unfold co_interval in H10; elim H10; clear H10; intros; rewrite Rabs_right. { rewrite SubEqui_P5 in H9; simpl in H9; inversion H9. { apply Rplus_lt_reg_l with (pos_Rl (SubEqui del H) (max_N del H)). replace (pos_Rl (SubEqui del H) (max_N del H) + (t - pos_Rl (SubEqui del H) (max_N del H))) with t; [ idtac | ring ]; apply Rlt_le_trans with b. { rewrite H14 in H12; assert (H13 : S (max_N del H) = pred (length (SubEqui del H))). { rewrite SubEqui_P5; reflexivity. } rewrite H13 in H12; rewrite SubEqui_P2 in H12; apply H12. } rewrite SubEqui_P6. 2: apply Nat.lt_succ_diag_r. unfold max_N; destruct (maxN del H) as (?&?&H13); replace (a + INR x * del + del) with (a + INR (S x) * del); [ assumption | rewrite S_INR; ring ]. } apply Rplus_lt_reg_l with (pos_Rl (SubEqui del H) I); replace (pos_Rl (SubEqui del H) I + (t - pos_Rl (SubEqui del H) I)) with t; [ idtac | ring ]; replace (pos_Rl (SubEqui del H) I + del) with (pos_Rl (SubEqui del H) (S I)). { assumption. } repeat rewrite SubEqui_P6. - rewrite S_INR; ring. - assumption. - apply Nat.lt_succ_r; assumption. } apply Rge_minus; apply Rle_ge; assumption. } intros; clear H0 H1 H4 phi H5 H6 t H7; case (Req_dec t0 b); intro. { left; assumption. } right; set (I := fun j:nat => a + INR j * del <= t0); assert (H1 : exists n : nat, I n). { exists 0%nat; unfold I; rewrite Rmult_0_l; rewrite Rplus_0_r; elim H8; intros; assumption. } assert (H4 : Nbound I). { unfold Nbound; exists (S (max_N del H)); intros; unfold max_N; destruct (maxN del H) as (?&_&H5); apply INR_le; apply Rmult_le_reg_l with (pos del). { apply (cond_pos del). } apply Rplus_le_reg_l with a; do 2 rewrite (Rmult_comm del); apply Rle_trans with t0; unfold I in H4; try assumption; apply Rle_trans with b; try assumption; elim H8; intros; assumption. } elim (Nzorn H1 H4); intros N [H5 H6]; assert (H7 : (N < S (max_N del H))%nat). { unfold max_N; case (maxN del H) as (?&?&?); apply INR_lt; apply Rmult_lt_reg_l with (pos del). { apply (cond_pos del). } apply Rplus_lt_reg_l with a; do 2 rewrite (Rmult_comm del); apply Rle_lt_trans with t0; unfold I in H5; try assumption; apply Rlt_le_trans with b; try assumption; elim H8; intros. elim H11; intro. { assumption. } elim H0; assumption. } exists N; split. { rewrite SubEqui_P5; simpl; assumption. } unfold co_interval; split. { rewrite SubEqui_P6. { apply H5. } assumption. } inversion H7. { replace (S (max_N del H)) with (pred (length (SubEqui del H))). { rewrite (SubEqui_P2 del H); elim H8; intros. elim H11; intro. { assumption. } elim H0; assumption. } rewrite SubEqui_P5; reflexivity. } rewrite SubEqui_P6. { destruct (Rle_dec (a + INR (S N) * del) t0) as [Hle|Hnle]. { assert (H11 := H6 (S N) Hle); elim (Nat.nle_succ_diag_l _ H11). } auto with real. } apply Nat.lt_succ_r; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra