Re: [Hol-info] "Wrong" definitions of transcendental functions (sin, cos, exp)?

Sorry... I'm wrong, these definitions are correct. I was confused by the definition of "suminf" for reals with the one for extreals. The one for reals is based on "sums" and "convergent", should be able to handle negative values. So, it should be possible to prove a full version of EXP_LE_X. -

[Hol-info] "Wrong" definitions of transcendental functions (sin, cos, exp)?

Hi, does anyone notice that, the 3 basic transcendental functions (sin, cos, exp) in HOL4 are only correctly defined on positive inputs? I say this because all these definitions are based on suminf which gives desired results only for all positive summations: [exp] Definition ⊢ ∀x. ex