Cauchy's Functional Equation over R

Stream: new members

[Gareth Ma]

Hi. The functional equation f(x + y) = f(x) + f(y) is known as Cauchy's Functional Equation, and it is known that while all such functions f : Q -> Q must be in the form f(x) = cx, this is not the case for real functions assuming the axiom of choice, since every vector space has a basis that way, and R can be viewed as a vector space over Q, and we can for example map f(q * sqrt(2)) = 0, and f(x) = x otherwise. I have formalised this as follows:

example : ∃ f : ℝ → ℝ, (∀ x y, f (x + y) = f x + f y) ∧ (∃ x : ℝ, f x ≠ x * f 1) :=
begin
  sorry,
end

My questions are:

1. How should I construct such a function? In particular, it would be nice to follow the argument above as closely, first "viewing R as a field over Q", then "picking a basis (via choice)", then of course constructing the function and proving it fits the requirements
2. Is there any way that does not follow ^ but also proves the result?
   Thanks in advance

[Gareth Ma]

Here's the Q version by the way: https://github.com/grhkm21/lean/blob/master/sketch/cauchy.lean#L6

[Gareth Ma]

Here is an attempt at defining f 2, but of course 2 can be replaced by any real number. How should I map the "indexing set" along with the coordinates to a function, and then "sum over the infinite set", where only finitely coordinates are non-zero, though not sure if that is included as part of the definition?

example : true :=
begin
  let real_basis := basis.of_vector_space ℚ ℝ,
  let real_repr := real_basis.repr,
  -- two_repr is the coordinates of 2 over Q
  let two_repr := real_repr 2,
  -- how should i define f 2 from here
end

[Gareth Ma]

Nevermind, I think I am very close to doing it. I will try a bit more.

[Gareth Ma]

Can't wait to share my solution though :joy: It's interesting to read the type definitions and try to figure out how they work and what I have to place my arguments. Learning quite a lot

[Gareth Ma]

Here is my current code:

example : true :=
begin
  let real_basis := basis.of_vector_space ℚ ℝ,
  let real_index_set : set ℝ := basis.of_vector_space_index ℚ ℝ,

  -- we prove that the set is nonempty
  have real_index_set_nonempty : real_index_set.nonempty,
  { rw ← set.nonempty_coe_sort, exact real_basis.index_nonempty, },
  let real_basis_vec₁ := set.nonempty.some real_index_set_nonempty,

  -- we prove that the set is infinite
  have real_index_set_infinite : real_index_set.infinite,
  { sorry, },

  -- then we can choose some basis vectors
  let real_index_nat_embedding := set.infinite.nat_embedding real_index_set real_index_set_infinite,
  let real_basis_vec₀ := real_index_nat_embedding 0,
  let real_basis_vec₁ := real_index_nat_embedding 1,

  -- they are not equal
  have real_basis_vec₀_ne_real_basis_vec₁: real_basis_vec₀ ≠ real_basis_vec₁,
  {
    by_contradiction,
    linarith [real_index_nat_embedding.injective h],
  },

  let f_map : real_index_set → ℝ := λ index,
  if index = real_basis_vec₀
  then
    real_basis real_basis_vec₁
  else
    real_basis real_basis_vec₀,

  let f : ℝ → ℝ := real_basis.constr ℝ f_map,

  -- now we verify that the two basis vectors map to different values
  let x₀ : ℝ := real_basis real_basis_vec₀,
  let x₁ : ℝ := real_basis real_basis_vec₁,
  have : f x₀ ≠ f x₁,
  {
    simp only [f, x₀, x₁],
    dsimp [basis.constr],
    -- simp only [f, basis.constr, x₀, x₁],
    simp only [basis.repr_self, finsupp.map_domain_single, finsupp.total_single, one_smul, id,
               f_map],
    simp [set_coe.ext_iff],
  }
end

It constructs the hamel basis of R over Q, then picks two basis vectors v1 and v2, and constructs a linear map that maps v1 -> v2 and every other basis vector to v1. Obviously this does not solve the cauchy's functional equation, but at least it manipulates with the basis vectors itself. Any feedback would be great! In particular, how to fill in the hole with proving that the dimension is infinite?

[Gareth Ma]

I can use the typical proof that if x is transcendental, then 1, x, x^2, ... are linearly independent? And so a basis must be infinite

[Yaël Dillies]

You can look at #12933 to get inspiration.

[Eric Wieser]

Note that for the ℚ version we have docs#add_monoid_hom.to_rat_linear_map which essentially captures the result

[Gareth Ma]

I swear I searched for “Cauchy.+functional” but got no results… Thank you both once again!

[Gareth Ma]

Yaël Dillies said:

You can look at #12933 to get inspiration.

It seems that this PR proves a lot of "assuming ..., then it's linear", of which there are like 10+ of them here, but seems to be slightly different from what I am doing, which is constructing a counterexample with no assumptions.

[Gareth Ma]

Eric Wieser said:

Note that for the ℚ version we have docs#add_monoid_hom.to_rat_linear_map which essentially captures the result

I found the add_monoid_hom structure, and I guess I should turn f : \Q \to \Q to f' : \Q \to+ \Q, which is the structure. Do you mind explaining how I should create an instance of this structure thing? I am not too familiar with the syntax

[Gareth Ma]

Docs: https://leanprover-community.github.io/mathlib_docs/algebra/hom/group.html#add_monoid_hom

[Gareth Ma]

Nevermind!

example {f : ℚ → ℚ} (h : ∀ x, ∀ y, f (x + y) = f x + f y) : ∀ x, f x = x * f 1 :=
begin
  -- setup f as linear_map from ℚ to ℚ
  have map_zero : f 0 = 0,
  { specialize h 0 0, simp at h, exact h, },
  let f_lin : ℚ →+ ℚ := { to_fun := f, map_zero' := map_zero, map_add' := h },
  let f_hom : ℚ →ₗ[ℚ] ℚ := add_monoid_hom.to_rat_linear_map f_lin,

  -- the rest is straightforward
  intro x,
  let := f_hom.map_smul' x 1,
  simp at this,
  exact this,
end

[Yakov Pechersky]

"simp at this, exact this" can also be spelled as "simpa using this"

[Yakov Pechersky]

And likely to be faster

[Yakov Pechersky]

Similarly, your map_zero tactic proof can be "simpa using h 0 0"

[Gareth Ma]

Thank you! I tried simpa at this but didn't work :P

[Gareth Ma]

Speaking of speed, do you know why dsimp seems to be a lot slower compared to simp only or other simp? Is that some known problem or just my use case? (I can make a minimal code real quick)

[Eric Wieser]

docs#add_monoid_hom.mk' will save you from having to prove map_zero

[Gareth Ma]

Now it's just

-- Quicker proof
example {f : ℚ → ℚ} (h : ∀ x, ∀ y, f (x + y) = f x + f y) : ∀ x, f x = x * f 1 :=
begin
  -- Setup f as linear_map from ℚ to ℚ
  let f_lin : ℚ →+ ℚ := add_monoid_hom.mk' f h,
  let f_hom : ℚ →ₗ[ℚ] ℚ := add_monoid_hom.to_rat_linear_map f_lin,

  -- The rest is straightforward
  intro x,
  simpa using f_hom.map_smul' x 1,
end

:thumbs_up: