[Merged by Bors] - feat(data/real/liouville, topology/metric_space/basic): further preparations for Liouville

[adomani]

These lemmas are used to show that a Liouville number is transcendental.

The statement that Liouville numbers are transcendental is the next PR in this sequence!

Co-authored-by: Jujian Zhang jujian.zhang1998@outlook.com

---

[eric-wieser]

I think this belongs in ordered_group.lean. Importing data.set.intervals.basic there is unlikely to cause problems.

[adomani]

Ok, I will wait to see if someone has strong opinion about where to move this file or about adding imports, and will go with the final suggestion.

[eric-wieser]

Sorry, I'm wrong - these need to go in data.set.intervals.basic, since that imports ordered_group

[eric-wieser]

Note that sub_mem_Icc_iff_right is now almost the right lemma here, but you then need to rewrite x - -z into x + z.

Of course, you could just drop this lemma and use the pieces directly now.

[adomani]

Below is my very clumsy attempt at using lemma sub_mem_Icc_iff_right: it is not simpler than what you initially found.

I really think that symmetric intervals are at least as important as random intervals, since they are the ones that arise from balls centred at a point. For this reason, I would prefer to maintain the lemma above.

begin
  rw [← neg_neg z] { occs := occurrences.pos [3] },
  rw [← sub_eq_add_neg x (- z)],
  exact (abs_le.trans mem_Icc.symm).trans sub_mem_Icc_iff_right,
end

[sgouezel]

When reading the docstring, I have no clue about the content of the lemma. The docstring should explain the content of the lemma (this is missing) and explain the context and motivation (it is there, and very nicely).

[adomani]

I have tried (in my head) explaining the content of this lemma, but I find it hard to formulate a "wordy" version that is not directly a transcription of the statement. The main reason for formulating this lemma is that it helps formalizing the next one. It avoids coercions kicking in, simplifies the manipulation of terms in the algebraic expressions and replaces certain steps with hypotheses which are direct consequences of lemmas in mathlib.

Here is a very verbose attempt at an explanation: what do you think?

"Let Z, N be types, let R be a metric space, let α : R be a point and let
j : Z → N → R be a function. We aim to estimate how close we can get to α, while staying
in the image of j. The points j z a of R in the image of j come with a "cost" equal to
d a. As we get closer to α while staying in the image of j, we are interested in bounding
the quantity d a * dist α (j z a) from below by a strictly positive amount 1 / M: the intuition
is that approximating well α with the points in the image of j should come at a high cost. The
hypotheses on the function f : R → R provide us with sufficient conditions to ensure our goal.
The first hypothesis is that f is Lipschitz at α: this yields a bound on the distance.
The second hypothesis is specific to the Liouville argument and provides the missing bound
involving the cost function d.

This lemma collects the properties needed to prove exists_pos_real_of_irrational_root.
It is stated in more general form than needed: in the intended application, Z = ℤ, N = ℕ,
R = ℝ, d a = a ^ f.nat_degree, j z a = z / (a + 1), f ∈ ℤ[x], α is an irrational
root of f, ε is small, M is a bound on the Lipschitz constant of f near α, n is
the degree of the polynomial f."

[sgouezel]

Just minor nitpicking left. You can merge yourself once this is done.
bors d+

[bors]

✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[adomani]

I am very happy that finally Liouville is creeping into mathlib! Thank you all!

bors r+

[bors]

Canceled.

[adomani]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests