proposition: Lemma rho_incr (i j : int) : 2%:~R <= i -> 0 <= j -> i <= j -> rho i <= rho j.
proof: Proof. move=> le0i le0j leij. suff hsucc (k : int) : 2%:~R <= k -> rho k <= rho (k + 1). case: i j le0i leij le0j => [] // i [] // j le2i + _. rewrite lez_nat; elim: j => [ |j ihj]; first lia. rewrite leq_eqVlt => /predU1P [-> // | leij]. by rewrite -addn1 PoszD; apply/le_trans/hsucc; [exact: ihj | lia]. move=> le2k {i j le0i le0j leij}. pose Ralpha i : realalg := QtoR (alpha i). pose Rbeta i : realalg := QtoR (beta i). have lt_0_Rbeta (i : int) : 0 <= i -> 0 < Rbeta i%:Q. by move=> *; rewrite RealAlg.ltr_to_alg lt_0_beta ?ler0z. have lt_Rbeta_1 (i : int) : 0 <= i -> Rbeta i%:Q < 1. by move=> *; rewrite RealAlg.ltr_to_alg lt_beta_1 ?ler0z. have lt_Ralpha_0 (i : int) : 0 <= i -> 0 < Ralpha i%:Q. by move=> *; rewrite RealAlg.ltr_to_alg lt_0_alpha ?ler0z. pose hr (i : int) (x : realalg) : realalg := Ralpha i%:Q - Rbeta i%:Q / x. have h2hr (j : int) (x : rat) : QtoR (h j%:Q x) = hr j (QtoR x). rewrite /hr rmorphB /= [QtoR _]lock; congr (_ - _). - by rewrite -lock. - by rewrite rmorphM /= [QtoR x^-1]fmorphV. pose p (i : int) (x : realalg) := - (x * x) + Ralpha i%:Q * x - Rbeta i%:Q. have hr_p (i : int) (x : realalg) : x != 0 -> hr i x - x = (p i x) / x. by move=> xneq0; rewrite !mulrDl !mulNr !mulfK // addrC addrA. have lt0k : 0 < k by apply: lt_le_trans le2k. have le0k : 0 <= k by apply: ltW. suff toR : 0 <= p k (QtoR (rho k)). rewrite -RealAlg.ler_to_alg -subr_ge0. rewrite rho_rec // h2hr hr_p; last first. by apply: lt0r_neq0; rewrite RealAlg.ltr_to_alg lt_0_rho. by apply: divr_ge0; rewrite ?toR // RealAlg.ler_to_alg ltW // lt_0_rho. pose deltap (i : int) := QtoR (delta i%:Q). have deltap_pos (i : int) : 0 <= i -> 0 < deltap i. by move=> ?; rewrite /deltap RealAlg.ltr_to_alg lt_0_delta ?ler0z. pose xp (i : int) : realalg := (Ralpha i%:Q + Num.sqrt (deltap i)) / QtoR (rat_of_Z 2). pose yp (i : int) : realalg := (Ralpha i%:Q - Num.sqrt (deltap i)) / QtoR (rat_of_Z 2). have xyp i : 0 <= i -> xp i * yp i = Rbeta i%:Q. move=> ?; rewrite mulrC mulrACA -subr_sqr sqr_sqrtr. by rewrite /Ralpha /Rbeta /deltap /delta; field. exact/ltW/deltap_pos. have fac_p i x : 0 <= i -> p i x = - ((x - xp i) * (x - yp i)). move=> le0i. rewrite mulrBl !mulrBr [x * yp i]mulrC !opprB addrAC addrA -mulrDl. by rewrite [_ * x - x * x]addrC /p xyp // /xp /yp; field. have hr_p_pos i t (le0i : 0 <= i) : yp i <= t -> t <= xp i -> 0 <= p i t. move=> leypt letxp. by rewrite fac_p // oppr_ge0; apply: mulr_le0_ge0; rewrite subr_cp0. suff rho_in_Iyx i (le2i : 2%:~R <= i) : yp i <= QtoR (rho i) <= xp i. by have /andP[yr rx] := rho_in_Iyx _ le2k; apply: hr_p_pos. have lt_0_xp j : 0 <= j -> 0 < xp j. move=> le0j; rewrite /xp; apply: divr_gt0. exact/ltr_wpDr/lt_Ralpha_0/le0j/sqrtr_ge0. by rewrite RealAlg.ltr_to_alg. have le_1_xp j (le0j : 0 <= j) : 1 <= xp j. rewrite /xp lter_pdivlMr ?mul1r; last by rewrite RealAlg.ltr_to_alg. have trans : QtoR (rat_of_Z 2) <= Ralpha j%:Q. by apply: ltW; rewrite RealAlg.ltr_to_alg lt_2_alphaN // ler0z. apply: le_trans trans _; rewrite lerDl; exact: sqrtr_ge0. have le_yp_1 j : 2%:~R <= j -> yp j <= 1. move=> le2j. have le0j : 0 <= j by apply: le_trans le2j; rewrite le0z_nat. have -> : yp j = Rbeta j%:Q / xp j. by rewrite -xyp // mulrAC mulfV ?mul1r //; apply/lt0r_neq0/lt_0_xp. rewrite ler_pdivrMr ?lt_0_xp // mul1r. by apply/le_trans/le_1_xp/le0j/ltW/lt_Rbeta_1. have hr_incr j x y : 0 <= j -> 0 < x -> x <= y -> hr j x <= hr j y. move=> le0j lt0x lexy; rewrite -subr_ge0 /hr addrAC [- (Ralpha _ - _)]opprD. rewrite opprK addrA addrN add0r -mulrBr; apply: mulr_ge0. by rewrite RealAlg.ler_to_alg; apply/ltW/lt_0_beta; rewrite ler0z. by rewrite subr_ge0 lef_pV2 // posrE //; apply: lt_le_trans lexy. suff rho_in_I1x : 1 <= QtoR (rho i) <= xp i. by case/andP: rho_in_I1x => h1 ->; rewrite andbT; exact/le_trans/h1/le_yp_1. suff lerx : QtoR (rho i) <= xp i. by rewrite [X in X && _]RealAlg.ler_to_alg le_1_rho //=; apply: le_trans le2i. suff im_hr j x : 0 <= j -> 0 < x -> x <= xp j -> hr j x <= xp (j + 1). have base_case : QtoR (rho 2) <= xp 2. rewrite /xp ler_pdivlMr; last by rewrite RealAlg.ltr_to_alg. rewrite -lerBlDl; set lhs := (X in X <= _). have [le_lhs_0 | lt_0_lhs] := ler0P lhs. exact/le_trans/sqrtr_ge0/le_lhs_0. rewrite -[lhs]gtr0_norm // -sqrtr_sqr; apply: ler_wsqrtr; rewrite /lhs. rewrite -rmorphM /Ralpha -rmorphB -rmorphXn /deltap RealAlg.ler_to_alg. have ->: 2%:~R = rat_of_Z 2 by rewrite rat_of_ZEdef. by rewrite /delta rho2_eq /alpha [_ <= _]refines_eq; vm_compute. case: i le2i; last by discriminate. case; first by discriminate. case; first by discriminate. elim=> [| n ihn] _; first exact: base_case. move/(_ (eqxx _)): ihn => ler3x. have -> : n.+3 = Posz n.+2 + 1 :> int by rewrite -addn1 PoszD. have -> : QtoR (rho (Posz n.+2 + 1)) = hr n.+2 (QtoR (rho n.+2)). rewrite rho_rec // h2hr // ; exact: lt_0_rho. apply: le_trans (im_hr _ _ _ _ ler3x) _ => //. rewrite RealAlg.ltr_to_alg; exact: lt_0_rho. move=> le0j lt0x /(hr_incr j _ _ le0j lt0x) {i le2i}. have -> : hr j (xp j) = xp j. apply/eqP; rewrite -subr_eq0 hr_p; last exact/lt0r_neq0/lt_0_xp. suff -> : p j (xp j) = 0 by rewrite mul0r. by rewrite fac_p // subrr mul0r oppr0. move=> h; apply: le_trans h _. suff xp_incr : xp j <= xp (j + 1) by []. rewrite /xp ler_pM2r; last first. by rewrite invr_gt0 RealAlg.ltr_to_alg. apply: lerD. by rewrite RealAlg.ler_to_alg rmorphD /=; apply: alpha_incr; rewrite ler0z. rewrite ler_sqrt; last by try apply/ltW; apply/deltap_pos/addr_ge0. by rewrite /deltap RealAlg.ler_to_alg rmorphD; apply: delta_incr; rewrite ler0z. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) mathcomp(realalg) CoqEAL(hrel param refinements) CoqEAL(pos binnat binint rational) tactics shift binomialz bigopz rat_of_Z rho_computations seq_defs c_props initial_conds algo_closures