The natural exponential function on real numbers #1747
Conversation
…da.md Co-authored-by: Fredrik Bakke <[email protected]>
…da.md Co-authored-by: Fredrik Bakke <[email protected]>
…s.lagda.md Co-authored-by: Fredrik Bakke <[email protected]>
| exp-power-series-at-zero-ℝ : (l : Level) → power-series-at-zero-ℝ l | ||
| exp-power-series-at-zero-ℝ l = | ||
| power-series-at-zero-coefficients-ℝ | ||
| ( λ n → raise-real-ℚ l (reciprocal-rational-ℕ⁺ (nonzero-factorial-ℕ n))) |
There was a problem hiding this comment.
Couldn't we define exp-power-series-XXX in the settings of ring extension of ℚ. For the definition you only need to invert factorial-ℕ n in a ring structure so this should be enough to define the power series. Then apply this to Banach algebras to define exponentials of real numbers, complex numbers, matrices, etc.
There was a problem hiding this comment.
We can, but it's not obvious to me we'd ever find a use for it in something that isn't also a ring extension of the real numbers?
There was a problem hiding this comment.
We can, but it's not obvious to me we'd ever find a use for it in something that isn't also a ring extension of the real numbers?
There was a problem hiding this comment.
Sure. But now you're defining the exponential series living in formal-power-series-Commutative-Ring (commutative-ring-ℝ l) not some ring extension of the real numbers. I think it should be in some formal-power-series-Commutative-Ring (???) for a larger class of rings, be it rational extensions, or real extensions if you prefer, but not restricted to real numbers themselves.
There was a problem hiding this comment.
Fair. And there's another reason that occurs to me: computing rates of convergence ought be aided by having explicit rationals instead of reals, preventing the need for any flavor of choice.
3 participants
Depends on #1716.