Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I do not think the change in #3 is an improvement.
Two things that are lost by removing the previous contents are:
The first is a critical loss. The latter, I suspect, is a main part of the reason the page was created in the first place.
I do not think it improves clarity to replace all uses of the square root function with a more complicated expression via $\exp$ and $\log$.
And… I’m not sure imprecisely belaboring the high school algebra to solve the functional equation adds any value for the intended audience of this page. I feel like that’s a lot of detail spelling out something the reader would already be proficient in (and is still missing the detail to get the logic exactly right).
Well, at this point I expect this is trolling.
I rolled back the changes made by the guest.
Theresa Leba
The original proof relies on the inverse function theorem. The subsection titled “In constructive mathematics” needs to state that the quadratic function is analytic or uniformly differentiable or something similar, since a function being continuously differentiable is not enough for the inverse function theorem to apply to the function in constructive mathematics from what i could remember.
Hello, I was the author of the new proof.
First of all, I do admit that overwriting the existing proof was a mistake - it is good to have multiple proofs of the same thing in an article. (See the fundamental theorem of algebra article where the same thing gets proven multiple times).
Secondly, to Todd Trimble’s comment; this was not a troll, this was a serious effort that was just poorly executed.
The exponential and natural logarithm functions are real analytic in character: the existence of the former rely on Cauchy completeness of the real numbers and the existence of the latter rely on the inverse function theorem on the domain of the exponential function, or some other definition, like the integral definition or the analytic completion of power series definition, and proofs that they are inverses of each other rely on other theorems of real analysis.
The algebra was an attempt to prove that partial inverses exist of the quadratic functions, but it relied on another property of the exponential and natural logarithm, the fact that exponential and natural logarithm are group isomorphisms between addition on the real numbers and multiplication on the positive real numbers, and I never explicitly mentioned that in my proof. More specifically, given that the exponential function is a group isomorphism from the additive group of real numbers and the multiplicative group of positive real numbers, then
$y = x^2 = x x = \exp(\ln(x)) \exp(\ln(x)) = \exp(\ln(x) + \ln(x)) = \exp(2 \ln(x))$and then one gets $\ln(y) = 2 \ln (x)$ and $\exp\left(\frac{1}{2} \ln(y)\right) = x$, the latter which is the inverse of $x^2$ on the domain $(0, \infty)$ and codomain $(0, \infty)$, and thus we could call it the square root $\mathrm{sqrt}(x)$. The other branch, when $x \lt 0$ for $x \mapsto x^2$, follows from
$y = x^2 = (-x) (-x) = \exp(\ln(-x)) \exp(\ln(-x)) = \exp(\ln(-x) + \ln(-x)) = \exp(2 \ln(-x))$and then one gets $\ln(y) = 2 \ln (-x)$ and $-\exp\left(\frac{1}{2} \ln(y)\right) = x$, which is just the negation of $\mathrm{sqrt}(x)$.
1 to 8 of 8