@user21820 I'm reading your statement in the uppermost starred comment above. In particular, regarding taking the definition of cosine in terms of complex exponentials and proving all the trig identities that way. I'm wondering if you can actually get away with that without effectively needing those trig identities for the real valued cosine and sine (which are typically defined via their taylor series).
I do think visual proofs are acceptable in geometry because geometry is an inherently visual field of mathematics. i'm skeptical that all theorems in geometry can be proven analytically. I do agree in this particular instance it is better to prove these trig theorems analytically.
In the physical sciences, outside of wave-like phenomena, sinusoids are almost always used visually (e.g. analyzing torque when a force is applied at a given angle)
Frequently you will need gemoetric results for things like vertical angles, alternating interior angles, etc to actually solve it
You can prove that alternating interior angles are equal without needing the visual notion of what these angles are?
I am skeptical of that
In particular, I was wondering whether 820's statement regarding trig identities being proven from the definition of the COMPLEX sinusoids can actually be done without needing these exact identities for the REAL sinusoids
as the complex sinusoids are defined in terms of the real sinusoids
It is easier to show the uniqueness of the definition in terms of real sinusoids, in the sense that definition is the only one that will naturally generalize the real exponential
You can avoid power series altogether if you have the existence and uniqueness theorems for ODEs, which give you much simpler proofs than using power series
it's easy calculus vs. dealing with Cauchy products
We want to define $$f(z)=e^z$$ in such a way that it satisfies the following properties: $$ f'(z) = f(z) , \quad f(x+ 0i) = e^x$$ In other words we want it to be its own derivative and we would like it to reduce to the regular exponential function when the exponent is purely real. Lets explore w...
Then $\exp(x+y)=\exp(x)\exp(y)$, because for fixed $y$, both satisfy the equation $f'=f$ with initial condition $f(0)=\exp(y)$, so they are equal due to the uniqueness teheorem
If you take the taylor series as the definition for the complex exponential you are left wondering whether there are other possible definitions that would naturally generalize the real exponential, Mathein is touching on this actually
Nvm, shes doing trig identies, mathjax is disabled :)
@MatheinBoulomenos I like your way actually. So you are using Picard's Theorem?
You can also define $\sin$ and via $f''=-f$ and $f(0)=0$ and $f'(0)=1$ and similar for $\cos$, then you can derive the addition formula in the same manner as above
And these theorems are CRUCIAL for physical applications
Not the trig identities, but the geometric notions
You need the fixed point theorem for picards theorem, although fairly trivial, is not generally on the table in intro to analysis, which I suppose is why the taylor series definition is used.
@user21820 I guess the strongest point that we seem to disagree on is that I don't believe that ALL of mathematics should be constrained to be first order expressable and/or provable within a formal logical system. It is too restrictive.
@DavidReed Then you should read the proofs in my related posts; there is absolutely no use of any identities to obtain the complex exponential function and its properties, and so you're wrong that there is no completely analytical proof.
There are two common ways of defining $π$, and they are interestingly and non-trivially equivalent.
$
\def\lfrac#1#2{{\large\frac{#1}{#2}}}
$
If you wish to define $π$ as the ratio of a circle's circumference to diameter, you would first have to define arc length, which is highly non-trivial. ...
Maybe I should post an answer, explaining how really $e^{iπ} + 1 = 0$ is forced by our choice of what we want the exponential function to be. This may either make one more fascinated by the way it is so forced, or less fascinated because now the mystery is more clearly unraveled. $\overset{..}\sm...
Which has been downvoted by two users who obviously don't appreciate mathematics.
A lot of people claim (wrongly) that one needs something like the uniform convergence theorem for series, but in the special case of exp, it turns out just the (asymptotic) definition of derivative is enough.
@MatheinBoulomenos <− You refer to this? That is in fact harder. Once you see my proofs you will know. It is 'nice' in the sense that it works for general ODEs, but if you know the proof of the solution existence theorem it's harder than my proof that exp as defined by the power series (rather than as a maximal solution of the ODE) converges.
He probably says it's simpler because he is thinking of the uniform convergence theorem in order to prove term-wise differentiation of power series, which is not in fact necessary for exp.
Proving the summation identity I would think you need the Cauchy product, which is a pain, I am still reviewing yours
The proof of Picard's theorem is fairly trivial though and widely applicable, so once you have that machinery I would imagine her way is easier, BUT I am still reading yours :)
as In I have not yet finished yours to make that determination
I will add, another way of defining pi is to define it to be twice the least positive zero of the cosine function
It's fairly easy taking the taylor series definition of cosine and using the IVT to show that such a zero exists
or twice the least positive zero of the sine function rather
@DavidReed That's correct, and is exactly the approach I would take if going via exp, because we can easily prove that exp is periodic, as in the linked post from the linked post:
There actually an elementary way to derive everything from series definitions of the exponential and trigonometric functions:
First obtain the series for $\exp$ on $\mathbb{C}$ about $0$ where $\exp$ is defined as a function such that $\exp' = \exp$ and $\exp(0) = 1$, and prove that the series c...
@DavidReed Read finish first. You will see that there is no Cauchy product needed for exp. =) It is true that you need it for more general termwise stuff, but exp converges so quickly that you can do without it.
By the way I won't prove any of these first until I have already constructed the exponential function and proven its properties, because then it is trivial to define cos(x) = (exp(ix)+exp(−ix))/2 and sin(x) = (exp(ix)−exp(−ix))/2i and get all the identities by purely algebraic manipulation.
Using this, sin(a+b) can be algebraically manipulated to get the desired identity.
You only need the property that exp(x+y) = exp(x)·exp(y), which I proved in my posts.
Well if you want I can prove it later. It however can be captured algebraically by an axiom.
Namely, given complex variable y varying with complex parameter x, if dy/dx = 0 then y is constant. (This is using the framework described here, which some cranky users downvoted.)
@LeakyNun I don't have time to read now, but the wikipedia article gives references for that, and I'm sure it's due to undecidability of the halting problem, just like incompleteness.
@DavidReed They were relevant to your conversation, so there is no need. If however you want to keep them in another room, I can move them. For example, you could expand your Logic Books room to Math Books room. =)
Though it's also true I'd rather not have too many screenshots at one go. =)
Yes, I figured once she read them you could just trash them once you got on. I think the logic books room has likely been deleted. I'm happy with either outcome
Though when I think about it, it does have relevance to reverse mathematics, which you are fond of
Incidentally, if you read my post about generalized differentiation, it's in fact much stronger than the usual inverse function theorem, and also the proof in my framework is extremely clean. I have not thought much about how to generalize to multivariable calculus, but since I don't use it much I didn't really try.
The inverse function theorem is huge in that it gives you the implicit function theorem (actually I think they are equivalent, though not 100% on that)
You need implicit function theorem for Lagrange multipliers for example, which is obviously of huge practical importance in fields like economics/finance
As mentioned, it is a pain to prove, I don't blame you for avoiding it :)
I meant for $\mathbb{R}^n$
Really I hate analytic proofs in general, writing $ < \epsilon$ gets very old very fast. I'm more of an algebraist, I find proofs in algebra to be much more elegant and interesting.
Anyways I'm off. Good chatting with you. I may drop in again tomorrow.
@user21820 I don't see where you need power series. All the statements you need, including $\exp=\cos+i\cdot \sin$ can be derived from the uniqueness theorem
I mean $\exp(ix)=\cos(x)+i\sin(x)$ of course
Both sides satisfy $f''=-f$ and $f(0)=1$, $f'(0)=i$
that sounds easier to me than proving that you can reorder an absolutely converging series
Where the definition of $\cos$ and $\sin$ are the solutions to $f''=-f$ with $f(0)=1$, $f'(0)=0$ for $\cos$ and with $f(0)=0$, $f'(0)=1$ for $\sin$
