proposition: Lemma Rint_Cauchy_Schwarz : forall f g a b x y z, a <= b -> (forall x, a <= x <= b -> continuity_pt f x) -> (forall x, a <= x <= b -> continuity_pt g x) -> Rint (f * f)%F a b x -> Rint (g * g)%F a b y -> Rint (f * g)%F a b z -> z^2 <= x * y.
proof: Proof. intros f g a b x y z Hle Hfc Hgc Hf Hg Hfg. assert (H0 : {y = 0} + {y <> 0}). destruct (total_order_T y 0) as [[H|H]|H]. right; apply Rlt_not_eq; assumption. left; assumption. right; apply Rgt_not_eq; assumption. destruct H0 as [H0|H0]. assert (Hz : z = 0). destruct (Rle_lt_or_eq_dec a b Hle); [| subst; apply (Rint_uniqueness (f * g)%F b b z 0 Hfg (Rint_singleton (f * g)%F b))]. eapply Rint_uniqueness; [apply Hfg|]. eapply Rint_eq_compat with (fun _ => 0). intros. unfold mult_fct. apply Rmult_eq_0_compat_l. apply Rsqr_eq_0_reg. replace (g x0 * g x0) with ((g * g)%F x0) by auto. replace (Rmin a b) with a in * by (symmetry; apply Rmin_def; apply Hle). replace (Rmax a b) with b in * by (symmetry; apply Rmax_def; apply Hle). apply Rint_continuous_pos_eq_0 with a b; auto. intros; apply continuity_pt_mult; apply Hgc; assumption. intros; apply Rle_0_sqr. subst; assumption. pose (fun _:R => 0) as null; fold null. replace 0 with (0 * (b - a)) by ring. apply Rint_constant. subst y; subst z. repeat rewrite Rmult_0_r. rewrite pow_ne_zero; auto with *. assert (Hy : 0 <= y). eapply Rint_pos with (f := (g * g)%F). eexact Hle. intros u Hu; apply Rle_0_sqr. assumption. pose (F k x := (f x - k * g x)²). assert (Hpos : forall k i, Rint (F k) a b i -> 0 <= i). intros k i H. eapply Rint_pos with (f := F k). eexact Hle. intros u Hu; apply Rle_0_sqr. assumption. assert (Heq : forall k, Rint (F k) a b (x - 2 * k * z + k² * y)). intros k. apply Rint_eq_compat with (f := ((f * f) - (fct_cte (2 * k)) * (f * g) + (fct_cte k² )* (g * g))%F). intros; unfold fct_cte, F, plus_fct, mult_fct, minus_fct, Rsqr; ring. auto with Rint. assert (Hcs : 0 <= x - z² / y). eapply Hpos. replace (x - z² / y) with (x - 2 * (z / y) * z + (z / y)² * y). apply Heq. unfold Rsqr; field; assumption. apply Rle_ge in Hcs; apply Rminus_ge in Hcs; apply Rge_le in Hcs. apply Rmult_le_compat_r with (r := y) in Hcs; [|assumption]. replace (z² / y * y) with z² in Hcs by (field; assumption). unfold Rsqr in Hcs. ring_simplify in Hcs. apply Hcs. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions