Cauchy Equation

Stream: Is there code for X?

[Zhang Qinchuan]

Is there any theorem about Cauchy Equation (f(x+y)=f(x)+f(y) where x,y are real numbers)?

It would be nice if there is a theorem as follow :

If f(x) is continous and satisfies f(x+y)=f(x)+f(y), then f(x)=kx for all real numbers.

By the way, there is a lot of property that satisfies :

If f(x) has property p and satisfies f(x+y)=f(x)+f(y), then f(x)=kx for all real numbers.

[Joseph Myers]

The last comment in !3#12933 says "Ported to LeanCamCombi". I can't now locate this port in LeanCamCombi (or mathlib4), @Yaël Dillies where is this work now?

[Yaël Dillies]

Hmm, I think it's in a branch of LeanCamCombi. Let me dig it up

[Yaël Dillies]

Found it! Will make it available in LeanCamCombi soon

[Yaël Dillies]

@Joseph Myers, voilà : https://yaeldillies.github.io/LeanCamCombi/docs/LeanCamCombi/CauchyFunctionalEquation.html

[Zhang Qinchuan]

Yaël Dillies said:

Joseph Myers, voilà : https://yaeldillies.github.io/LeanCamCombi/docs/LeanCamCombi/CauchyFunctionalEquation.html

So these theorems are maintained in LeanCamCombi and will never push to Mathlib4. Am I right?

[Joseph Myers]

I hope it ends up in mathlib, it's a well known result that gets used in other proofs.

[Violeta Hernández]

hilbert said:

By the way, there is a lot of property that satisfies :

If f(x) has property p and satisfies f(x+y)=f(x)+f(y), then f(x)=kx for all real numbers.

Basically all such properties p are corollaries of the following: if f satisfies the Cauchy equation but isn't a scalar multiple of x, then its graph is a dense set in ℝ²

[Violeta Hernández]

(so if you can prove continuity, or continuity at a single point, or bounded at some nontrivial interval, etc, then f = kx follows)

[Violeta Hernández]

This isn't specific to the real numbers, it should hold for any linearly ordered archimedean field with the order topology. Admittedly all of those are subfields of ℝ though.

[Violeta Hernández]

And it's a basic consequence of linear algebra. If f x ≠ x * f 1, then (1, f 1) and (x, f x) are linearly independent over ℚ. Their ℚ-linear combinations are all in the graph of f, and by archimedeanness, they form a dense subset of it.

[Yaël Dillies]

hilbert said:

Yaël Dillies said:

Joseph Myers, voilà : https://yaeldillies.github.io/LeanCamCombi/docs/LeanCamCombi/CauchyFunctionalEquation.html

So these theorems are maintained in LeanCamCombi and will never push to Mathlib4. Am I right?

Nono. On the contrary, LeanCamCombi is like a giant treadmill of results that will eventually go to mathlib. I don't have time right now to specifically clean Cauchy's functional equation up and PR it, so you should feel free to do that :smile:

[Yaël Dillies]

First result toward Cauchy's functional equation: #20304