Gelfand-Tornheim theorem

Stream: Is there code for X?

[Jz Pan]

How far could we add Gelfand-Tornheim theorem to mathlib? That is, if a field K has an infinite place (i.e. an AbsoluteValue of it to Reals, which is not non-archimedean),
then there exists an embedding K →+* ℂ such that the absolute value is equivalent to
the usual absolute value | | on ℂ.

Here is the idea of proof (which I gave to Aristotle AI):

1. There exists z such that v z ≤ 1 and v (z + 1) > 1. In fact, since v is archimedean,
   there exists x and y such that v (x + y) > max (v(x), v(y)) so we may assume 0 < v(x) ≤ v(y),
   take z = x / y and we are done.

2. The v(N) is unbounded, where N is the type of natural numbers. Suppose otherwise, i.e.
   there exists C such that v(n) < C for all natural numbers n, then consider
   v(z + 1) ^ n = v((z+1)^n) for sufficiently large n where z is in the step 1.
   Consider binomial expansion of (z+1)^n.
   Then we obtain that v(z + 1) ^ n = v((z+1)^n) < (n + 1) * C which is impossible when n goes infinity.

3. In particular K is of characteristic zero, hence it is a Q-algebra, the restriction of v on
   Q gives an absolute value on Q. By Ostrowski's theorem (docs#Rat.AbsoluteValue.equiv_real_or_padic in mathlib),
   it can be deduced that the restriction of v is equivalent to the real absolute value.

4. Taking completion with respect to the absolute value on the ring homomorphism Q -> K
   we obtain R -> \widehat{K}, hence \widehat{K} is a normed field and also a normed R-algebra.
   By docs#NormedAlgebra.Real.nonempty_algEquiv_or in mathlib, we know that \widehat{K} is isomorphic to R or C,
   in particular, K can be embedded into C preserving the absolute value (up to equivalence).
   This completes the proof.

The steps 1 - 3 was already formalized in https://github.com/acmepjz/lean-iwasawa/blob/master/Iwasawalib/NumberTheory/RamificationInertia/AbsoluteValue.lean (but not provided to AI). The last step is still missing, since it's not known by mathlib the obtained map K →+* ℂ preserving absolute value.

FYI This is the formal statement of the theorem I gave to Aristotle AI:

formal statement

import Mathlib

/-- **Gelfand-Tornheim theorem**: if a field `K` has an infinite place,
then there exists an embedding `K →+* ℂ` such that the absolute value is *equivalent* to
the usual absolute value `| |` on `ℂ`. Note that it is not necessary equal to `| |` as it is
in fact equal to `| | ^ c` for some `0 < c ≤ 1`.

PROVIDED SOLUTION
1. There exists `z` such that `v z ≤ 1` and `v (z + 1) > 1`. In fact, since `v` is archimedean,
   there exists `x` and `y` such that `v (x + y) > max (v(x), v(y))` so we may assume `0 < v(x) ≤ v(y)`,
   take `z = x / y` and we are done.
2. The `v(N)` is unbounded, where `N` is the type of natural numbers. Suppose otherwise, i.e.
   there exists `C` such that `v(n) < C` for all natural numbers `n`, then consider
   `v(z + 1) ^ n = v((z+1)^n)` for sufficiently large `n` where `z` is in the step 1.
   Consider binomial expansion of `(z+1)^n`.
   Then we obtain that `v(z + 1) ^ n = v((z+1)^n) < (n + 1) * C` which is impossible when `n` goes infinity.
3. In particular `K` is of characteristic zero, hence it is a `Q`-algebra, the restriction of `v` on
   `Q` gives an absolute value on `Q`. By Ostrowski's theorem (`Rat.AbsoluteValue.equiv_real_or_padic` in mathlib),
   it can be deduced that the restriction of `v` is equivalent to the real absolute value.
4. Taking completion with respect to the absolute value on the ring homomorphism `Q -> K`
   we obtain `R -> \widehat{K}`, hence `\widehat{K}` is a normed field and also a normed `R`-algebra.
   By `NormedAlgebra.Real.nonempty_algEquiv_or` in mathlib, we know that `\widehat{K}` is isomorphic to `R` or `C`,
   in particular, `K` can be embedded into `C` preserving the absolute value (up to equivalence).
   This completes the proof.
-/
theorem AbsoluteValue.exists_ringHom_complex_of_not_isNonarchimedean
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (h1 : v.IsNontrivial) (h2 : ¬IsNonarchimedean v) :
    ∃ φ : K →+* ℂ, NumberField.place φ ≈ v := by
  sorry

After 5 days and countless time of retries, Aristotle AI returns a full formalized proof with 3300 lines (a quick scan reveals that the proof length may be reduced by 90%):

Aristotle AI output

GelfandTornheim_output.lean

[Michael Stoll]

That should not be hard to get from results in my Heights repo.
See in particular the end of Heights/Extension.lean there. You take the completion, show that it is an algebra over the reals (with compatible abs. value) and then apply Ostrowski's (other) Theorem.