Commit d9fa8833 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add theorem ln_beta_gt.

parent d40d74c2
......@@ -2138,6 +2138,22 @@ apply bpow_lt_bpow.
now apply Rle_lt_trans with (Rabs x).
Qed.
Theorem ln_beta_gt :
forall x e,
(bpow e <= Rabs x)%R ->
(e < ln_beta x)%Z.
Proof.
intros x e Hx.
destruct (ln_beta x) as (ex, Ex) ; simpl.
apply lt_bpow.
apply Rle_lt_trans with (1 := Hx).
apply Ex.
intros Zx.
apply Rle_not_lt with (1 := Hx).
rewrite Zx, Rabs_R0.
apply bpow_gt_0.
Qed.
Theorem ln_beta_Z2R_le :
forall m e,
m <> Z0 ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment