proposition: Lemma Rint_substitution : forall f g g' a b I, a <= b -> (forall x, a <= x <= b -> g a <= g x <= g b) -> (forall x, g a <= x <= g b -> continuity_pt f x) -> (forall x, a <= x <= b -> derivable_pt_lim g x (g' x)) -> (forall x, a <= x <= b -> continuity_pt g' x) -> Rint (fun x => f (g x) * g' x) a b I -> Rint f (g a) (g b) I.
proof: Proof. intros f g g' a b I Hab Habgab Hcontf Hder Hcontg' HI. destruct (Habgab a) as [_ Hgab]; auto with *. assert (Hpr : forall x : R, g a <= x -> x <= g b -> Riemann_integrable f (g a) x). intros. apply continuity_implies_RiemannInt; trivial. intros; apply Hcontf; split. tauto. apply Rle_trans with x; intuition; trivial. pose (primitive Hgab (FTC_P1 Hgab Hcontf)) as F. assert(Hfab : Riemann_integrable f (g a) (g b)). apply Hpr; auto with *. assert(HF := RiemannInt_P20 Hgab (FTC_P1 Hgab Hcontf) Hfab). assert(Heq : Rint f (g a) (g b) (F(g b) - (F(g a)))). unfold F; rewrite <- HF. apply Rint_RiemannInt_link. replace I with (comp F g b - comp F g a). apply Heq. symmetry. eapply Rint_uniqueness. apply HI. apply Rint_derive. trivial. intros. apply derivable_pt_lim_comp. auto. apply RiemannInt_P28; auto. intros. apply continuity_pt_mult. apply continuity_pt_comp. apply derivable_continuous_pt. exists (g' x); apply Hder; apply H. auto. auto. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions