proposition: Lemma Integral_less_norm : a [#] b -> forall x, Compact Hab x -> forall Hx, AbsIR (F x Hx) [<] Norm_Funct contF -> AbsIR (Integral contF) [<] Norm_Funct contF[*]AbsIR (b[-]a).
proof: Proof. intros H x H0 Hx H1. set (N := Norm_Funct contF) in *. elim (ap_imp_less _ _ _ H); intro. apply less_wdr with (N[*] (b[-]a)). eapply less_wdl. eapply less_leEq_trans. apply integral_less_norm with (contF := included_imp_contin _ _ _ _ _ _ _ (compact_map2 a b (less_leEq _ _ _ a0) Hab) contF) (Hx := Hx); auto. apply compact_map1 with (Hab' := Hab); auto. eapply less_leEq_trans. apply H1. unfold N in |- *; apply included_imp_norm_leEq. apply compact_map1. apply mult_resp_leEq_rht. unfold N in |- *; apply included_imp_norm_leEq. apply compact_map2. apply shift_leEq_minus; apply less_leEq. astepl a; auto. apply AbsIR_wd; apply eq_symmetric_unfolded. apply Integral_integral. apply mult_wdr. apply eq_symmetric_unfolded; apply AbsIR_eq_x. apply shift_leEq_minus; apply less_leEq. astepl a; auto. apply less_wdr with (N[*] (a[-]b)). set (Hmin := Min_leEq_Max b a) in *. cut (included (Compact Hmin) (Compact Hab)). cut (included (Compact Hab) (Compact Hmin)). intros H2 H3. cut (Continuous_I Hmin F). intro H4. eapply less_wdl. eapply less_leEq_trans. apply integral_less_norm with (contF := included_imp_contin _ _ _ _ _ _ _ (compact_map2 _ _ (less_leEq _ _ _ b0) Hmin) H4) (Hx := Hx); auto. apply compact_map1 with (Hab' := Hmin); auto. eapply less_leEq_trans. apply H1. unfold N in |- *; apply included_imp_norm_leEq. eapply included_trans. 2: apply compact_map1 with (Hab' := Hmin). apply H2. apply mult_resp_leEq_rht. unfold N in |- *; apply included_imp_norm_leEq. eapply included_trans. apply compact_map2 with (Hab' := Hmin). apply H3. apply shift_leEq_minus; apply less_leEq. astepl b; auto. eapply eq_transitive_unfolded. apply AbsIR_inv. apply AbsIR_wd; apply eq_symmetric_unfolded. apply eq_transitive_unfolded with ( [--] (Integral (included_imp_contin _ _ _ _ _ _ _ H3 contF))). apply Integral_op. apply un_op_wd_unfolded. apply Integral_integral. apply included_imp_contin with (Hab := Hab); auto. red in |- *; intros. apply compact_wd' with (Hab := Hab). apply Min_comm. apply Max_comm. auto. red in |- *; intros. apply compact_wd' with (Hab := Hmin). apply Min_comm. apply Max_comm. auto. apply mult_wdr. eapply eq_transitive_unfolded. apply eq_symmetric_unfolded; apply AbsIR_eq_x. apply shift_leEq_minus; apply less_leEq. astepl b; auto. apply AbsIR_minus. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions