Zulip Chat Archive

Stream: triage

Topic: PR #4301: feat(liouville_theorem): lemmas of Liouville th...


view this post on Zulip Random Issue Bot (Nov 12 2020 at 14:17):

Today I chose PR 4301 for discussion!

feat(liouville_theorem): lemmas of Liouville theorem
Created by @Jujian Zhang (@jjaassoonn) on 2020-09-28
Labels: awaiting-review

Is this PR still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Random Issue Bot (Nov 27 2020 at 14:20):

Today I chose PR 4301 for discussion!

feat(liouville_theorem): lemmas of Liouville theorem
Created by @Jujian Zhang (@jjaassoonn) on 2020-09-28
Labels: awaiting-review

Is this PR still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 14:31):

I hope to find the time to look at this PR soon. Jujian was an MSc student of mine.

view this post on Zulip Random Issue Bot (Mar 16 2021 at 14:26):

Today I chose PR 4301 for discussion!

feat(liouville_theorem): lemmas of Liouville theorem
Created by @Jujian Zhang (@jjaassoonn) on 2020-09-28
Labels: WIP, awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Damiano Testa (Mar 16 2021 at 14:47):

I still have one (or maybe two) PRs in this thread: there is the proof that Liouville number exist that is still missing in mathlib. I have an almost-ready-for-mathlib-review file on this, but I have not been able to get it through the system before I got swamped on other stuff! I plan to make further progress with this, within a couple of weeks.

view this post on Zulip Damiano Testa (Mar 16 2021 at 14:47):

Also, when I say "I", I really mean that my contribution has been to massage Jujian's files, to adapt them to mathlib!

view this post on Zulip Ruben Van de Velde (Mar 16 2021 at 15:03):

Does the work you've done include the proof that transcendental implies irrational?

view this post on Zulip Damiano Testa (Mar 16 2021 at 15:05):

If I remember correctly, transcendental => irrational is already there. There is certainly a proof that Liouville => transcendental, using Liouville => irrational. I cannot remember about the implication transcendental => irrational, but I assume that it is there!

view this post on Zulip Damiano Testa (Mar 16 2021 at 15:07):

I checked the file data/real/irrational.

Transcendental is defined as non-algebraic and I am pretty sure that rational => algebraic is there. So, "transcendental => irrational" may not be stated, but should not be hard!

view this post on Zulip Damiano Testa (Mar 16 2021 at 15:45):

There are certainly better proofs, but this works:

import data.real.irrational
import ring_theory.algebraic

open polynomial

lemma transcendental.irrational {r : } (tr : transcendental  r) : irrational r :=
begin
  rintro a, rfl⟩,
  refine tr X - C a, X_sub_C_ne_zero a, _⟩,
  rw [alg_hom.map_sub, sub_eq_zero, aeval_X, aeval_C],
  refl,
end

view this post on Zulip Damiano Testa (Mar 16 2021 at 15:54):

I updated the name, so that it would work with dot.notation, I believe. If people think that this might be useful, I can PR it to mathlib.

view this post on Zulip Damiano Testa (Mar 17 2021 at 05:50):

PR #6721

I split the proof into two parts.

  • is_algebraic_of_mem: if A is an R-algebra and r : R, then algebra_map R A r is algebraic over R.
  • transcendental.irrational: the "contrapositive" of is_algebraic_of_mem, in the case of a transcendental R\mathbb{R} viewed as a Q\mathbb{Q}-algebra.

view this post on Zulip Damiano Testa (Mar 17 2021 at 08:16):

This is just to give visibility to a name-change: are people happy with the name of the lemma below? (Suggested by Eric)

/-- An element of `R` is algebraic, when viewed as an element of the `R`-algebra `A`. -/
lemma is_algebraic_algebra_map (a : R) : is_algebraic R (algebra_map R A a) :=
X - C a, X_sub_C_ne_zero a, by simp only [aeval_C, aeval_X, alg_hom.map_sub, sub_self]⟩

view this post on Zulip Johan Commelin (Mar 17 2021 at 08:17):

LGTM


Last updated: May 09 2021 at 15:11 UTC