proposition: Lemma integral_less_norm : forall a b Hab (F : PartIR) contF, let N := Norm_Funct contF in a [<] b -> forall x, Compact Hab x -> forall Hx, AbsIR (F x Hx) [<] N -> AbsIR (integral a b Hab F contF) [<] N[*] (b[-]a).
proof: Proof. intros a b Hab F contF N Hless x H Hx H0. set (e := (N[-]AbsIR (F x Hx)) [/]TwoNZ) in *. cut ([0] [<] e); intros. 2: unfold e in |- *; apply pos_div_two; apply shift_less_minus. 2: astepl (AbsIR (F x Hx)); auto. elim (contin_prop _ _ _ _ contF e); auto. intros d H2 H3. set (mid1 := Max a (x[-]d)) in *. set (mid2 := Min b (x[+]d)) in *. cut (a [<=] mid1); [ intro leEq1 | unfold mid1 in |- *; apply lft_leEq_Max ]. cut (mid1 [<=] mid2); [ intro leEq2 | unfold mid1, mid2 in |- *; inversion_clear H; apply leEq_transitive with x ]. 2: apply Max_leEq; auto. 2: apply less_leEq; apply shift_minus_less. 2: apply shift_less_plus'; astepl ZeroR; auto. 2: apply leEq_Min; auto. 2: apply less_leEq; apply shift_less_plus'. 2: astepl ZeroR; auto. cut (mid2 [<=] b); [ intro leEq3 | unfold mid2 in |- *; apply Min_leEq_lft ]. cut (Continuous_I leEq1 F). cut (Continuous_I leEq2 F). cut (Continuous_I leEq3 F). intros cont3 cont2 cont1. cut (Continuous_I (leEq_transitive _ _ _ _ leEq1 leEq2) F). intro H4. apply less_wdl with (AbsIR (integral _ _ _ _ cont1[+]integral _ _ _ _ cont2[+] integral _ _ _ _ cont3)). 2: apply AbsIR_wd. 2: apply eq_transitive_unfolded with (integral _ _ _ _ H4[+]integral _ _ _ _ cont3). 2: apply bin_op_wd_unfolded. 2: apply integral_plus_integral. 2: algebra. 2: apply integral_plus_integral. rstepr (N[*] (mid1[-]a) [+]N[*] (mid2[-]mid1) [+]N[*] (b[-]mid2)). eapply leEq_less_trans. apply triangle_IR. apply plus_resp_less_leEq. eapply leEq_less_trans. apply triangle_IR. apply plus_resp_leEq_less. eapply leEq_transitive. apply integral_leEq_norm. unfold N in |- *; apply mult_resp_leEq_rht. 2: apply shift_leEq_minus; astepl a; auto. apply included_imp_norm_leEq. apply included_compact. apply compact_inc_lft. split. unfold mid1 in |- *; apply lft_leEq_Max. apply leEq_transitive with mid2; auto. 2: eapply leEq_transitive. 2: apply integral_leEq_norm. 2: unfold N in |- *; apply mult_resp_leEq_rht. 3: apply shift_leEq_minus; astepl mid2; auto. 2: apply included_imp_norm_leEq. 2: apply included_compact. 2: split. 2: apply leEq_transitive with mid1; auto. 2: auto. 2: apply compact_inc_rht. eapply leEq_less_trans. apply integral_leEq_norm. apply mult_resp_less. apply leEq_less_trans with (N[-]e). 2: apply shift_minus_less; apply shift_less_plus'. 2: astepl ZeroR; auto. apply leEq_Norm_Funct; intros y Hy Hy'. apply leEq_wdr with (AbsIR (F x Hx) [+]e). 2: unfold e in |- *; rational. apply AbsIR_bnd_AbsIR. apply H3; auto. cut (included (Compact leEq2) (Compact Hab)); auto. apply included_compact. split; auto. apply leEq_transitive with mid2; auto. split; auto. apply leEq_transitive with mid1; auto. cut (x[-]d [<=] x[+]d). intro H5. apply compact_bnd_AbsIR with H5. cut (included (Compact leEq2) (Compact H5)); auto. apply included_compact; unfold mid1, mid2 in |- *; split. apply rht_leEq_Max. apply leEq_transitive with mid2; auto. unfold mid2 in |- *; apply Min_leEq_rht. apply leEq_transitive with mid1; auto. unfold mid1 in |- *; apply rht_leEq_Max. apply Min_leEq_rht. apply leEq_transitive with x. apply shift_minus_leEq; apply shift_leEq_plus'. astepl ZeroR; apply less_leEq; auto. apply shift_leEq_plus'. astepl ZeroR; apply less_leEq; auto. unfold mid2, mid1 in |- *. astepl (x[-]x). unfold cg_minus at 1 2 in |- *. inversion_clear H. elim (less_cotransitive_unfolded _ _ _ Hless x); intro. apply plus_resp_leEq_less. apply leEq_Min; auto. apply shift_leEq_plus'; astepl ZeroR; apply less_leEq; auto. apply inv_resp_less; apply Max_less; auto. apply shift_minus_less; apply shift_less_plus'. astepl ZeroR; auto. apply plus_resp_less_leEq. apply less_Min; auto. apply shift_less_plus'; astepl ZeroR; auto. apply inv_resp_leEq; apply Max_leEq; auto. apply shift_minus_leEq; apply shift_leEq_plus'. astepl ZeroR; apply less_leEq; auto. apply included_imp_contin with a b Hab; auto. apply included_compact. apply compact_inc_lft. split; auto. apply leEq_transitive with mid1; auto. apply included_imp_contin with a b Hab; auto. apply included_compact. split; auto. apply leEq_transitive with mid1; auto. apply compact_inc_rht. apply included_imp_contin with a b Hab; auto. apply included_compact. split; auto. apply leEq_transitive with mid2; auto. split; auto. apply leEq_transitive with mid1; auto. apply included_imp_contin with a b Hab; auto. apply included_compact. apply compact_inc_lft. split; auto. apply leEq_transitive with mid2; auto. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)