proposition: Theorem spec_fun_bound : forall x : R, (Rpower 2 (1 + (1 + (1 + (1 + 3)))) <= x)%R -> (Rpower (2 * x) (sqrt (2 * x) / 2) < Rpower (1 + 3) (x / 3))%R.
proof: Proof. intros x H. cut (0 < x)%R; [ intros Hx | apply Rlt_le_trans with (2 := H); unfold Rpower in |- *; auto with real ]. apply ln_lt_inv. unfold Rpower in |- *; auto with real. unfold Rpower in |- *; auto with real. unfold Rdiv in |- *; auto with real. unfold Rpower in |- *. repeat rewrite ln_exp. cut (0 < sqrt (2 * x))%R; [ intros Hs | apply sqrt_lt_R0; auto with real; apply Rmult_lt_0_compat; auto with real ]. apply Rmult_lt_reg_l with (r := (/ sqrt (2 * x))%R); auto with real. repeat rewrite <- Rmult_assoc. rewrite Rinv_l; auto with real. rewrite Rmult_1_l. pattern x at 3 in |- *; rewrite <- (sqrt_square x); auto with real. repeat rewrite sqrt_mult; auto with real. replace (/ (sqrt 2 * sqrt x) * (sqrt x * sqrt x) * / 3 * ln (1 + 3))%R with (ln (1 + 3) / (sqrt 2 * 3) * sqrt x)%R; [ idtac | field ]. 2: split; apply Compare.not_eq_sym; auto with real. apply Rminus_lt; apply Ropp_lt_cancel; rewrite Ropp_minus_distr; rewrite Ropp_0. apply Rlt_increasing with (a := Rpower 2 (1 + (1 + (1 + (1 + 3))))) (f := fun x => (ln (1 + 3) / (sqrt 2 * 3) * sqrt x - / 2 * ln (2 * x))%R) (f' := fun x : R => (ln (1 + 3) / (sqrt 2 * 3) * / (2 * sqrt x) - / 2 * (2 * / (2 * x)))%R); auto. intros y Hy Hy1. cut (0 < y)%R; [ intros Hyy | apply Rlt_le_trans with (2 := Hy); unfold Rpower in |- *; auto with real ]. apply derivable_pt_lim_minus with (f1 := fun x0 : R => (ln (1 + 3) / (sqrt 2 * 3) * sqrt x0)%R) (f2 := fun x0 : R => (/ 2 * ln (2 * x0))%R). apply derivable_pt_lim_scal with (f := sqrt) (a := (ln (1 + 3) / (sqrt 2 * 3))%R). apply derivable_pt_lim_sqrt; auto. apply derivable_pt_lim_scal with (f := fun x0 : R => ln (2 * x0)) (a := (/ 2)%R). rewrite (fun x y => Rmult_comm x (/ y)). apply derivable_pt_lim_comp with (f1 := fun x0 : R => (2 * x0)%R) (f2 := ln). pattern 2%R at 2 in |- *; rewrite <- (Rmult_1_r 2). apply derivable_pt_lim_scal with (f := id) (a := 2%R). apply derivable_pt_lim_id. apply derivable_pt_lim_ln. apply Rmult_lt_0_compat; auto with real. intros z H1 H2; apply Rlt_le. cut (0 < z)%R; [ intros Hz | idtac ]. apply Rlt_Rminus_ZERO. repeat rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. rewrite Rmult_1_l. apply Rmult_lt_reg_l with (r := (2 * z)%R); auto with real. rewrite Rinv_r; auto with real. replace (ln (1 + 3)) with (2 * ln 2)%R. pattern z at 1 in |- *; rewrite <- sqrt_square; auto with real. rewrite sqrt_mult; auto with real. replace (2 * (sqrt z * sqrt z) * (2 * ln 2 / (sqrt 2 * 3) * / (2 * sqrt z)))%R with (2 * sqrt z * (ln 2 / (sqrt 2 * 3)))%R. apply Rlt_le_trans with (2 * sqrt (Rpower 2 (1 + (1 + (1 + (1 + 3))))) * (ln 2 / (sqrt 2 * 3)))%R. rewrite Rpower_plus. rewrite Rpower_1; auto with real. rewrite sqrt_mult; auto with real. rewrite <- (fun x y => Rpower_sqrt (Rpower x y)); auto with real. rewrite Rpower_mult; auto with real. replace ((1 + (1 + (1 + 3))) * / 2)%R with 3%R; [ idtac | field ]. replace (2 * (sqrt 2 * Rpower 2 3) * (ln 2 / (sqrt 2 * 3)))%R with (2 * Rpower 2 3 * (ln 2 / 3))%R. pattern 2%R at 1 in |- *; rewrite <- (Rpower_1 2); auto with real. rewrite <- Rpower_plus. apply Rmult_lt_reg_l with (r := 3%R); auto with real. repeat apply Rplus_lt_0_compat; auto with real. rewrite Rmult_1_r. apply Rlt_trans with (3 * (Rpower 2 (1 + 3) * (/ 2 / 3)))%R. replace (1+3)%R with (1+1+1+1)%R by ring. repeat rewrite Rpower_plus; repeat rewrite Rpower_1; lra. apply Rmult_lt_compat_l. lra. apply Rmult_lt_compat_l. unfold Rpower in |- *; auto with real. unfold Rdiv in |- *; apply Rmult_lt_compat_r. lra. apply ln_lt_2. cut (forall x y z : R, (0 < z)%R -> (2 * x * (y / 3))%R = (2 * (z * x) * (y / (z * 3)))%R); [ intros Htmp; apply Htmp | intros; field ]; auto with real. unfold Rpower in |- *; auto with real. unfold Rpower in |- *; auto with real. unfold Rdiv in |- *. repeat apply Rmult_le_compat; auto with real. repeat apply Rmult_le_pos; auto with real. apply sqrt_positivity; auto with real. unfold Rpower in |- *; auto with real. repeat apply Rmult_le_pos; auto with real. rewrite <- ln_1; auto with real. apply sqrt_positivity; auto with real. unfold Rpower in |- *; auto with real. apply sqrt_le_1; auto with real. unfold Rpower in |- *; auto with real. rewrite <- ln_1; auto with real. field; auto with real. split; apply Compare.not_eq_sym; apply Rlt_not_eq; auto with real. apply exp_inv. rewrite exp_ln. change (Rpower 2 2 = (1 + 3)%R) in |- *. replace (2)%R with (1+1)%R at 2 by ring. repeat rewrite Rpower_plus; repeat rewrite Rpower_1; (ring||lra). lra. apply Rlt_le_trans with (2 := H1). unfold Rpower in |- *; auto with real. pattern (Rpower 2 (1 + (1 + (1 + (1 + 3))))) at 1 in |- *; rewrite Rpower_plus; rewrite Rpower_1; auto with real. rewrite sqrt_mult; auto with real. 2: unfold Rpower in |- *; auto with real. rewrite ln_mult. pattern (sqrt (Rpower 2 (1 + (1 + (1 + 3))))) at 1 in |- *; rewrite <- Rpower_sqrt. rewrite Rpower_mult. replace ((1 + (1 + (1 + 3))) * / 2)%R with 3%R; [ idtac | field ]. replace (ln (1 + 3)) with (2 * ln 2)%R. pattern (ln (Rpower 2 (1 + (1 + (1 + (1 + 3)))))) at 1 in |- *; unfold Rpower in |- *; rewrite ln_exp; auto with real. replace (2 * ln 2 / (sqrt 2 * 3) * (sqrt 2 * exp (3 * ln 2)))%R with (2 * ln 2 * (/ 3 * Rpower 2 3))%R. 2: cut (forall x y z : R, (0 < y)%R -> (2 * x * (/ 3 * z))%R = (2 * x / (y * 3) * (y * z))%R); [ intros Htmp; fold Rpower in |- *; apply Htmp | intros; field ]; auto with real. apply Rlt_Rminus_ZERO. pattern (ln 2) at 1 in |- *; rewrite <- Rmult_1_l. rewrite <- Rmult_plus_distr_r. replace (/ 2 * ((1 + (1 + (1 + (1 + (1 + 3))))) * ln 2))%R with (2 * ln 2 * 2)%R. apply Rmult_lt_compat_l; auto with real. repeat apply Rmult_lt_0_compat; auto with real. rewrite <- ln_1; auto with real. apply Rmult_lt_reg_l with (r := 3%R); auto with real. repeat apply Rplus_lt_0_compat; auto with real. repeat rewrite <- Rmult_assoc; rewrite Rinv_r; auto with arith. rewrite Rmult_1_l. replace (3)%R with (1+1+1)%R at 2 by ring. repeat rewrite Rpower_plus; repeat rewrite Rpower_1; try ring. lra. lra. field. apply exp_inv. rewrite exp_ln. change (Rpower 2 2 = (1 + 3)%R) in |- *. replace (2)%R with (1+1)%R at 2 by ring. repeat rewrite Rpower_plus; repeat rewrite Rpower_1; try ring. lra. lra. unfold Rpower in |- *; auto with real. lra. unfold Rpower in |- *; auto with real. Qed.
imports: Coq(Wf_nat Ranalysis Rtrigo ArithRing Lra)