proposition: Lemma fun_lim_seq_integral_IR : conv_fun_seq'_IR J g G contg contG.
proof: Proof. red in |- *; intros. unfold g, G in |- *. cut (J a). intro H. set (h := fun n : nat => [-C-] (Integral (prim_lemma _ _ (contf n) x0 Hx0 a H))) in *. set (g' := fun n : nat => h n{+} ( [-S-]contf n) a H) in *. set (G' := [-C-] (Integral (prim_lemma _ _ contF x0 Hx0 a H)) {+} ( [-S-]contF) a H) in *. assert (H0 : forall n : nat, Continuous_I Hab (h n)). intro; unfold h in |- *; Contin. cut (forall n : nat, Continuous_I Hab (( [-S-]contf n) a H)). intro H1. assert (H2 : forall n : nat, Continuous_I Hab (g' n)). intro; unfold g' in |- *; Contin. cut (Continuous_I Hab (( [-S-]contF) a H)). intro H3. assert (H4 : Continuous_I Hab G'). unfold G' in |- *; Contin. apply conv_fun_seq'_wdl with g' H2 (included_imp_Continuous _ _ contG _ _ _ Hinc). intro; FEQ. simpl in |- *. apply eq_symmetric_unfolded; apply Integral_plus_Integral with (Min3_leEq_Max3 x0 x a). apply included_imp_Continuous with J; Contin. apply conv_fun_seq'_wdr with H2 G' H4. FEQ. simpl in |- *. apply eq_symmetric_unfolded; apply Integral_plus_Integral with (Min3_leEq_Max3 x0 x a). apply included_imp_Continuous with J; Contin. unfold g', G' in |- *. apply conv_fun_seq'_wdl with (f := g') (contf := fun n : nat => Continuous_I_plus _ _ _ _ _ (H0 n) (H1 n)) (contF := H4). unfold g' in H2. intro; apply Feq_reflexive; Included. unfold g', G' in |- *. apply (fun_Lim_seq_plus' _ _ Hab h (fun n : nat => ( [-S-]contf n) a H) H0 H1 _ _ (Continuous_I_const _ _ _ (Integral (prim_lemma _ _ contF x0 Hx0 a H))) H3). unfold h in |- *. apply seq_conv_imp_fun_conv with (x := fun n : nat => Integral (prim_lemma _ _ (contf n) x0 Hx0 a H)). apply limit_of_Integral with (Hf := fun n : nat => prim_lemma _ _ (contf n) x0 Hx0 a H); auto. Included. apply fun_lim_seq_integral with (fun n : nat => included_imp_Continuous _ _ (contf n) _ _ _ Hinc) (included_imp_Continuous _ _ contF _ _ _ Hinc). apply convF; auto. apply compact_inc_lft. apply included_imp_Continuous with J; Contin. intro; apply included_imp_Continuous with J; Contin. apply Hinc; apply compact_inc_lft. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems