proposition: Lemma IntegrationSubs01 : forall a b (Hab: Min a b[<=]Max a b) (H01: [0][<=][1]) F (HFG: Continuous_I H01 ((F[o]([-C-](b[-]a){*}(Fid IR){+}[-C-]a)))) (HF: Continuous_I Hab F), (b[-]a)[*]integral _ _ _ _ HFG[=]Integral HF.
proof: Proof. intros. assert (HFG0:Continuous_I (a:=[0]) (b:=[1]) H01 ((b[-]a){**}(F[o][-C-](b[-]a){*}FId{+}[-C-]a))). Contin. stepr (integral _ _ _ _ HFG0). apply eq_symmetric. apply integral_comm_scal. assert (HFG1:Continuous_I (a:=[0]) (b:=[1]) H01 ((F[o][-C-](b[-]a){*}FId{+}[-C-]a){*}[-C-](b[-]a))). Contin. stepr (integral _ _ _ _ HFG1). apply integral_wd. FEQ. assert (H01':Min [0] [1][<=]Max [0] [1]). apply Min_leEq_Max. assert (HFG2:Continuous_I H01' ((F[o][-C-](b[-]a){*}FId{+}[-C-]a){*}[-C-](b[-]a))). apply (included_imp_contin _ _ H01). apply included2_compact. apply compact_inc_lft. apply compact_inc_rht. assumption. stepr (Integral HFG2). apply eq_symmetric. apply Integral_integral. clear - H01. set (G:=[-C-](b[-]a){*}FId{+}[-C-]a) in *. assert (HG0 : Dom G [0]). repeat constructor. assert (HG1 : Dom G [1]). repeat constructor. assert (Hab':Min (G [0] HG0) (G [1] HG1)[<=]Max (G [0] HG0) (G [1] HG1)). apply Min_leEq_Max. assert (HF':Continuous_I Hab' F). apply (included_imp_contin _ _ Hab). unfold G. apply included2_compact. apply (compact_wd _ _ Hab a). apply compact_Min_lft. simpl. rational. apply (compact_wd _ _ Hab b). apply compact_Min_rht. simpl. rational. assumption. stepl (Integral HF'). apply Integral_wd'; simpl; rational. apply eq_symmetric. assert (X:included (Compact H01') (Compact (less_leEq _ _ _ (pos_one IR)))). apply included2_compact. apply compact_inc_lft. apply compact_inc_rht. eapply (IntegrationBySubstition). apply X. unfold G. New_Deriv. apply Feq_reflexive. repeat constructor. apply (included_Feq (Compact (less_leEq IR [0] [1] (pos_one IR))) realline). repeat constructor. FEQ. split. apply contin_imp_inc. apply HF'. intros x Hx [H0 H1]. assert (H0':[0][<=]x). stepl (Min [0] [1]);[assumption|]. apply leEq_imp_Min_is_lft. apply (less_leEq _ _ _ (pos_one IR)). assert (H1':x[<=][1]). stepr (Max [0] [1]);[assumption|]. apply leEq_imp_Max_is_rht. apply (less_leEq _ _ _ (pos_one IR)). unfold G. simpl. split. stepl (Min a b); [| apply MIN_wd; rational]. assert (Z:=leEq_or_leEq _ a b). rewrite -> leEq_def. intros Z0. apply Z. clear Z. intros Z. revert Z0. change (Not ((b[-]a)[*]x[+]a[<]Min a b)). rewrite <- leEq_def. destruct Z. stepl a; [| apply eq_symmetric; apply leEq_imp_Min_is_lft; auto]. apply shift_leEq_plus. rstepl ([0]:IR). apply mult_resp_nonneg; auto. apply shift_leEq_lft. assumption. stepl (Min b a); [| apply Min_comm]. stepl b; [| apply eq_symmetric; apply leEq_imp_Min_is_lft; auto]. apply shift_leEq_plus. apply shift_leEq_rht. rstepr ((a[-]b)[*]([1][-]x)). apply mult_resp_nonneg; apply shift_leEq_lft; assumption. stepr (Max a b); [| apply MAX_wd;rational]. assert (Z:=leEq_or_leEq _ a b). rewrite -> leEq_def. intros Z0. apply Z. clear Z. intros Z. revert Z0. change (Not (Max a b[<](b[-]a)[*]x[+]a)). rewrite <- leEq_def. destruct Z. stepr b; [| apply eq_symmetric; apply leEq_imp_Max_is_rht; auto]. apply shift_plus_leEq. apply shift_leEq_rht. rstepr ((b[-]a)[*]([1][-]x)). apply mult_resp_nonneg; apply shift_leEq_lft; assumption. stepr (Max b a); [| apply Max_comm]. stepr a; [| apply eq_symmetric; apply leEq_imp_Max_is_rht; auto]. apply shift_plus_leEq. rstepr ([0]:IR). apply shift_leEq_rht. rstepr ((a[-]b)[*]x). apply mult_resp_nonneg; auto. apply shift_leEq_lft. assumption. assumption. Qed.
imports: CoRN.ftc.FTC CoRN.ftc.Composition