proposition: Lemma Wallis_formula : forall Wn n, Rint (sin_n n) 0 (PI/2) Wn-> Rint (sin_n (S (S n))) 0 (PI/2) (Wn * (S n)/(S (S n))).
proof: Proof. intros Wn n H. pose (RiemannInt (integrable_sin_n (S (S n)))) as W2n. pose proof (Rint_RiemannInt_link _ _ _ (integrable_sin_n (S (S n)))) as HW2. assert (W2n = (S n) * (Wn - W2n)) as Heq. replace (S n * (Wn - W2n)) with (comp (fun x => x ^ (S n)) sin (PI/2) *((- cos)%F (PI/2)) - comp (fun x => x ^ (S n)) sin 0 *((- cos)%F 0) - (-(S n) * (Wn - W2n))). eapply Rint_parts with (f' := fun x => ((S n) * sin x ^ n)* cos x) (g' := sin). left; apply PI2_RGT_0. intros. apply derivable_pt_lim_comp. auto with Rcont. apply derivable_pt_lim_pow. intros. replace (sin x) with (- - sin x) by ring. auto with Rcont. intros. apply continuity_pt_mult. apply continuity_pt_mult; auto with Rcont. apply continuity_pt_const; intros u v; reflexivity. reg. auto with Rcont. auto with Rcont. apply Rint_eq_compat with (comp (fun x : R => x ^ S (S n)) sin). intros; unfold comp, mult_fct; simpl; ring. apply Rint_RiemannInt_link. apply Rint_eq_compat with (fun x => (- S n) * (sin x ^ n - sin x ^ (S (S n)))). intros. unfold mult_fct, opp_fct. rewrite Rmult_assoc. replace (cos x * - cos x) with (-(1 - (sin x)^2)). unfold Rsqr; simpl; ring. replace ((sin x) ^ 2) with ((sin x)²) by (unfold Rsqr; ring). rewrite <- (cos2 x); unfold Rsqr; ring. apply Rint_scalar_mult_compat_l. apply Rint_minus; trivial. unfold opp_fct, comp; rewrite cos_0, cos_PI2, sin_PI2, sin_0; simpl; ring. replace (Wn * S n / S (S n)) with (W2n). trivial. rewrite Rmult_comm. replace W2n with (/(S (S n)) * (S (S n))* W2n). replace Wn with ((Wn - W2n) + W2n) by ring. rewrite Rmult_plus_distr_l. rewrite <- Heq. unfold Rdiv. rewrite Rmult_comm with (r1 := (W2n + S n * W2n)). rewrite Rmult_assoc. apply Rmult_eq_compat_l. simpl; ring. field. auto with *. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics