proposition: Lemma Wallis_quotient_lim2 : forall l, l <> 0 -> (fun n => fact n) ~ (fun n => (n /(exp 1)) ^ n * sqrt n * l) -> Rseq_cv (fun n => W_odd n / W_even n) (l^2/(2*PI)).
proof: Proof. intros l Hneq Hl. apply Rseq_cv_eq_compat with (fun n => (2*2 ^ (4*n) * (fact n) ^ 4)/(PI*fact (2 * n) * fact (S (2 * n)))). intro; rewrite Wallis_quotient; reflexivity. assert (H2n : (fun n => fact (2 * n)) ~ (fun n => (2 * n / exp 1) ^ (2 * n) * sqrt (2 * n) * l)). assert (Hex : is_extractor (mult 2)). intros n; lia. pose (exist _ _ Hex) as db. assert (Hrw1 : extracted db fact == (fun n => fact (2 * n))). intros n; reflexivity. assert (Hrw2 : extracted db (fun n => (n / exp 1) ^ n * sqrt n * l) == (fun n => (2 * n / exp 1) ^ (2 * n) * sqrt (2 * n) * l)). intros n; unfold extracted. simpl. repeat rewrite plus_INR; simpl. replace (n + (n + 0)) with (2 * n) by field. reflexivity. eapply Rseq_equiv_eq_compat; [eassumption|eassumption|]. apply Rseq_equiv_subseq_compat with (Un := fact) (Vn := fun k : nat => (k / exp 1) ^ k * sqrt k * l) (phi := db). assumption. assert (H2n1 : (fun n : nat => fact (S(2*n))) ~ (fun n : nat => (S(2*n) / exp 1) ^ (S(2*n)) * sqrt (S(2*n)) * l)). assert (Hex : is_extractor (fun n => S (mult 2 n))). intros n; lia. pose (exist _ _ Hex) as db. apply Rseq_equiv_eq_compat with (extracted db fact) (extracted db (fun n : nat => (n / exp 1) ^ n * sqrt n * l)). intro n; unfold db; reflexivity. intro n; unfold db; reflexivity. apply Rseq_equiv_subseq_compat with (Un := fact) (Vn := fun k : nat => (k / exp 1) ^ k * sqrt k * l)(phi := db). assumption. apply Rseq_equiv_cv_constant. Local Open Scope Rseq_scope. apply Rseq_equiv_eq_compat with (Un := 2 * (fun n => 2 ^ (4 * n)) * fact * fact * fact * fact * / (PI * (fun n => fact (2 * n)) * (fun n => fact (S (2 * n))))) (Vn := (l^2 / (2 * PI))%R). intro n; unfold Rseq_mult, Rseq_inv, Rdiv, Rseq_constant; ring. intro; reflexivity. apply Rseq_equiv_trans with (2 * (fun n => 2 ^ (4 * n)) * ((fun n : nat => ((n / exp 1) ^ n * sqrt n * l)%R))*((fun n : nat => ((n / exp 1) ^ n * sqrt n * l)%R))*((fun n : nat => ((n / exp 1) ^ n * sqrt n * l)%R))*((fun n : nat => ((n / exp 1) ^ n * sqrt n * l)%R))* / (PI * (fun n : nat => ((2 * n / exp 1) ^ (2 * n) * sqrt (2 * n) * l)%R) * (fun n => (S (2 * n) / exp 1) ^ S (2 * n) * sqrt (S (2 * n)) * l)%R)). repeat apply Rseq_equiv_mult_compat; try apply Rseq_equiv_refl; try assumption. apply Rseq_equiv_inv_compat. exists O. intros n Hn. unfold Rseq_mult, Rseq_constant. apply Rmult_integral_contrapositive ; split ; [ apply Rmult_integral_contrapositive ; split ; [ apply PI_neq0 | apply INR_fact_neq_0] | apply INR_fact_neq_0 ]. exists (S O). intros n Hn; unfold Rseq_mult, Rseq_constant. assert(H : {m | n = S m}). exists (pred n). intuition. destruct H as (m, Subst). rewrite Subst. apply Rmult_integral_contrapositive ; split ; [ apply Rmult_integral_contrapositive ; split ; [ apply PI_neq0 | apply Rmult_integral_contrapositive ; split ; [ apply Rmult_integral_contrapositive ; split ; [ (apply pow_nonzero ; unfold Rdiv ; apply Rmult_integral_contrapositive ; split ; [ apply Rmult_integral_contrapositive ; split ; [ (intro ; lra) | (apply not_0_INR ; intuition) ] | (apply Rinv_neq_0_compat ; generalize (exp_pos 1) ; intros ; intro ; lra)]) | (intro H ; apply sqrt_eq_0 in H ; [ (apply Rmult_integral in H ; destruct H as [H|H] ; [ lra | (generalize H ; apply not_0_INR ; intuition) ]) | apply Rmult_le_pos ; intuition ]) ] | apply Hneq ] ] | apply Rmult_integral_contrapositive ; split ; [ apply Rmult_integral_contrapositive ; split ; [ (apply pow_nonzero ; unfold Rdiv ; apply Rmult_integral_contrapositive ; split ; [ apply not_0_INR ; intuition | (apply Rinv_neq_0_compat ; generalize (exp_pos 1) ; intros ; intro ; lra) ]) | (intro H ; apply sqrt_eq_0 in H ; [ (apply not_0_INR in H ; intuition ) | apply pos_INR ]) ] | apply Hneq ] ]. apply Rseq_equiv_mult_compat. apply Rseq_equiv_mult_compat. apply Rseq_equiv_refl. assumption. assumption. clear Hl H2n H2n1. apply Rseq_cv_equiv_constant. unfold Rdiv. apply Rmult_integral_contrapositive ; split . apply pow_nonzero; assumption. apply Rinv_neq_0_compat. apply Rmult_integral_contrapositive; split. intro ; lra. apply PI_neq0. unfold Rseq_constant, Rseq_mult, Rseq_div, Rseq_plus, Rseq_minus, Rseq_inv. apply Rseq_cv_eq_compat1 with (fun n:nat => (sqrt (2 * n) / sqrt (S (2 * n))) * (Rsqr l / PI * exp 1) * ((2 * n) / S (2 * n)) ^ (S (2 * n)) * /2)%R. exists (S O). intros n Hn. assert(H : {m | n = S m}). exists (pred n). intuition. destruct H as (m, Subst). unfold Rseq_constant. unfold Rdiv. ring_simplify. replace (sqrt n ^ 4) with (n ^ 2) by (rewrite <- (sqrt_sqrt n) at 1 ; [ring | intuition]). repeat rewrite Rpow_mult_distr. repeat rewrite <- pow_mult. repeat rewrite Rinv_mult_distr. replace (2 ^ (4 * n))%R with (2 ^ (2 * n) * 2 ^ (2 * n))%R by (repeat rewrite pow_mult ; rewrite <- Rpow_mult_distr ; replace (2 ^ 2 * 2 ^ 2)%R with (2 ^ 4)%R by (unfold pow ; ring) ; ring). rewrite (Nat.mul_comm n 4). replace (n ^ (4 * n))%R with (n ^ (2 * n) * n ^ (2 * n))%R by (rewrite <- pow_add ; ring_simplify (2 * n + 2 * n)%nat ; ring). replace ((/exp 1) ^ (4 * n))%R with ((/exp 1) ^ (2 * n) * (/exp 1) ^ (2 * n))%R by (rewrite <- pow_add ; ring_simplify (2 * n + 2 * n)%nat ; ring). repeat rewrite Rinv_pow. rewrite Rinv_involutive. rewrite <- tech_pow_Rmult with (exp 1) (2 * n)%nat. rewrite <- (Rinv_pow (exp 1) _). do 2 rewrite <- tech_pow_Rmult. replace (/sqrt (2 * n))%R with (sqrt (2 * n) / (2 * n))%R by (apply sqrt_id ; inversion Hn ; [intuition | apply not_0_INR ; intuition]). unfold Rsqr. unfold Rdiv. repeat rewrite <- Rinv_pow. field. split. assumption. split. intro H. apply sqrt_eq_0 in H. apply not_0_INR in H. assumption. intuition. intuition. split. apply pow_nonzero. apply not_0_INR. intuition. split. apply not_0_INR. intuition. split. apply pow_nonzero. apply not_0_INR. intuition. split. apply pow_nonzero. intro. lra. split. apply PI_neq0. apply pow_nonzero. intro. generalize (exp_pos 1) ; intros ; lra. apply not_0_INR. intuition. intro ; lra. apply not_0_INR. intuition. intro. generalize (exp_pos 1) ; intros ; lra. intro. generalize (exp_pos 1) ; intros ; lra. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. apply not_0_INR ; intuition. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. apply not_0_INR ; intuition. intro ; lra. apply pow_nonzero. apply not_0_INR ; intuition. apply pow_nonzero. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. apply Rmult_integral_contrapositive ; split. apply pow_nonzero. apply not_0_INR ; intuition. apply pow_nonzero. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. intro H. apply sqrt_eq_0 in H. generalize H. apply not_0_INR ; intuition. apply pos_INR. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply pow_nonzero. apply not_0_INR ; intuition. apply pow_nonzero. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. intro H. apply sqrt_eq_0 in H. generalize H. apply not_0_INR ; intuition. apply pos_INR. apply Hneq. apply pow_nonzero. intro ; lra. apply pow_nonzero. apply not_0_INR ; intuition. apply Rmult_integral_contrapositive ; split. apply pow_nonzero. intro ; lra. apply pow_nonzero. apply not_0_INR ; intuition. apply pow_nonzero. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply pow_nonzero. intro ; lra. apply pow_nonzero. apply not_0_INR ; intuition. apply pow_nonzero. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. intro H. apply sqrt_eq_0 in H. generalize H. apply Rmult_integral_contrapositive ; split. intro ; lra. apply not_0_INR. intuition. apply Rmult_le_pos. intuition. intuition. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply pow_nonzero. intro ; lra. apply pow_nonzero. apply not_0_INR ; intuition. apply pow_nonzero. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. intro H. apply sqrt_eq_0 in H. generalize H. apply Rmult_integral_contrapositive ; split. intro ; lra. apply not_0_INR. intuition. apply Rmult_le_pos. intuition. intuition. assumption. apply PI_neq0. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply pow_nonzero. intro ; lra. apply pow_nonzero. apply not_0_INR ; intuition. apply pow_nonzero. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. intro H. apply sqrt_eq_0 in H. generalize H. apply Rmult_integral_contrapositive ; split. intro ; lra. apply not_0_INR. intuition. apply Rmult_le_pos. intuition. intuition. assumption. apply Rmult_integral_contrapositive ; split. apply PI_neq0. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply pow_nonzero. intro ; lra. apply pow_nonzero. apply not_0_INR ; intuition. apply pow_nonzero. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. intro H. apply sqrt_eq_0 in H. generalize H. apply Rmult_integral_contrapositive ; split. intro ; lra. apply not_0_INR. intuition. apply Rmult_le_pos. intuition. intuition. assumption. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply Rmult_integral_contrapositive ; split. apply pow_nonzero. apply not_0_INR ; intuition. apply pow_nonzero. apply Rinv_neq_0_compat. intro. generalize (exp_pos 1) ; intros ; lra. intro H. apply sqrt_eq_0 in H. generalize H. apply not_0_INR. intuition. apply pos_INR. assumption. eapply Rseq_equiv_cv_compat. 2: reflexivity. symmetry; instantiate (1 := (1 * (Rsqr l / PI * exp 1) * /exp 1 * /2)). apply Rseq_equiv_mult_compat ; [ | apply Rseq_equiv_eq ; exists O ; intro ; intuition ]. apply Rseq_equiv_mult_compat. apply Rseq_equiv_mult_compat ; [ | apply Rseq_equiv_eq ; exists O ; intro ; intuition ]. pose (Un := (fun n => - / (2 * INR n + 1))%R). assert (Hcv0 : Rseq_cv Un 0). unfold Un. apply Rseq_cv_inv_INR_0_1. intros eps Heps. destruct (DL_sqrt_1 Un Hcv0 eps Heps) as (N, DL). exists N. intros n HN. generalize (DL n HN). intros DL1. unfold Rseq_constant, Rseq_plus, Rseq_minus, Rseq_mult, Rseq_inv, Un in *. rewrite <-sqrt_div ; [ | (apply Rmult_le_pos ; intuition) | intuition ]. rewrite S_INR. rewrite mult_INR. do 2 rewrite S_INR. replace (2 * n)%R with ((2 * n + 1) - 1)%R by ring. rewrite Rplus_0_l. unfold Rminus. rewrite Rinv_plus. rewrite Rinv_eq_1. unfold Rdiv in *. rewrite Ropp_mult_distr_l_reverse. rewrite Rmult_1_l. rewrite Rabs_minus_sym in DL1. apply DL1. generalize (pos_INR n) ; intuition ; lra. generalize (pos_INR n) ; intuition ; lra. apply Rseq_equiv_trans with (fun n : nat => exp ((2 * n + 1) * ln (1 - /(2 * INR n + 1)))). pose (Un := (fun n:nat => - /(2 * (INR n) + 1))%R). assert (Hcv0 : Rseq_cv Un 0). apply Rseq_cv_inv_INR_0_1. apply Rseq_equiv_trans with (fun n : nat => exp ((2 * n + 1) * (- / (2 * n + 1)))). apply Rseq_equiv_eq. exists O. intros n Hn. field_simplify ((2 * n + 1) * - / (2 * n + 1))%R. unfold Rseq_constant, Rseq_inv. rewrite <- exp_Ropp. unfold Rdiv. try rewrite Rinv_1. try rewrite Rmult_1_r. reflexivity. generalize (pos_INR n) ; intuition ; lra. apply Rseq_equiv_continuity with ((-1)). reg. generalize (exp_pos (-1)) ; intros l1 H1 ; lra. apply Rseq_cv_eq_compat with (-R1). intros n. unfold Rseq_constant, Rseq_minus, Rseq_plus, Rseq_opp. field. intros H1 ; generalize (pos_INR n) ; intros ; lra. change (-1)%R with (-(1%R))%R. intuition. eapply Rseq_equiv_cv_compat. 2: reflexivity. symmetry; instantiate (1 := (fun n => (2 * INR n + 1) * - / (2 * INR n + 1))%R). apply Rseq_equiv_mult_compat. apply Rseq_equiv_refl. apply Rseq_equiv_sym. apply Rseq_equiv_ln. apply Hcv0. apply Rseq_cv_eq_compat with (-R1). unfold Rseq_opp, Rseq_constant, Rseq_minus. intros n. field. generalize (pos_INR n) ; intuition ; lra. change (-1)%R with (-(1%R))%R. intuition. apply Rseq_equiv_eq. exists 1%nat. intros n Hn. rewrite pow_exp_ln. replace (2 * n)%R with ((2 * n + 1) - 1)%R by ring. rewrite S_INR. rewrite mult_INR. repeat rewrite S_INR. rewrite Rplus_0_l. unfold Rminus. rewrite Rinv_plus. rewrite Rinv_eq_1. ring_simplify (2 * n + 1 + -(1) + 1)%R. unfold Rdiv. ring_simplify (1 + -(1) * / ((1 + 1) * n + 1))%R. rewrite (Rplus_comm (- / (2 * n + 1)) _). reflexivity. generalize (pos_INR n) ; intuition ; lra. generalize (pos_INR n) ; intuition ; lra. unfold Rdiv. apply Rmult_lt_0_compat. apply Rmult_lt_0_compat ; intuition. apply Rinv_0_lt_compat. rewrite S_INR. generalize (pos_INR n) ; intuition ; lra. apply Rseq_cv_eq_compat with (Rsqr l / (2 * PI)). intro. unfold Rseq_mult, Rseq_plus, Rseq_constant, Rseq_div, Rseq_inv. field. split. apply PI_neq0. intro. generalize (exp_pos 1) ; intros ; lra. intros eps Heps. exists O. intros n Hn. unfold R_dist. unfold Rseq_constant, Rseq_div, Rseq_inv, Rseq_mult. unfold Rdiv, Rsqr. rewrite Rminus_diag_eq. rewrite Rabs_R0. apply Heps. ring. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics