Diophantine approximation

Stream: maths

[Michael Stoll]

I have code (~ 300 lines) providing a proof of

lemma rat_approx_infinite_iff_irrational {ξ : ℝ} :
  {q : ℚ | |ξ - q| < 1 / q.denom ^ 2}.infinite ↔ irrational ξ :=

This came out of a project a student in my seminar is working on (existence of non-trivial solutions to Pell's equation; it is basically the first step towards the proof). I think this would make a good contribution to mathlib (with results on Pell equations to follow eventually). (There is also a relation to #18011 @Oliver Nash ; the result can be stated in terms of add_well_approximable 𝕊 (λ n, 1 / n ^ 2) consisting exactly of the (images of) irrational numbers.)

But before I PR this, I would like to find out if it would have a chance of being reviewed and merged within a reasonable time frame, given that most of the effort goes into porting mathlib these days. The file imports data.real.irrational and combinatorics.pigeonhole, so I imagine that it is quite a bit removed from the tide at this point.

[Kevin Buzzard]

Why don't you get the student to PR it, then you review it and approve it, and because you're now a trusted member of the community a passing maintainer might merge it?

[Michael Stoll]

That would be cheating, since I have worked myself on the code quite a bit :smile: to get it into a shape suitable for mathlib...

[Kevin Buzzard]

Oh OK. Then I would suggest that you either explicitly approach people and ask for reviews, or just make an independent Pell's equation repo and autoport it to mathlib4 in a few months.

[Oliver Nash]

Oh wow, it's great to see some connections with #18011. I also note that Dirichlet's approximation theorem is on the Freek list. I suppose the statement here would be:

@[simp] lemma unit_add_circle.mem_add_approximable_real_iff {ξ : ℝ} :
  ↑ξ ∈ add_well_approximable unit_add_circle (λ n, 1/n^2) ↔ irrational ξ :=
sorry

[Oliver Nash]

As to your question of whether to cook up a PR, I think this is up to you. There is the danger that the port consumes so much effort that such a PR might not make it into Mathlib3. I will commit review this PR but of course, not having seen the code yet, I cannot make any promises. If you're happy to carry out the work to PR this work subject to this risk then by all means, please do it.

[Oliver Nash]

Also note that it's not unusual for a PR review to generalise some results it contains. Thus even if the current version of the code does not currently touch already-ported files, this could change during review. This would mean that merging such a PR could also require changes to Mathlib4.

[Michael Stoll]

Oliver Nash said:

Oh wow, it's great to see some connections with #18011. I also note that Dirichlet's approximation theorem is on the Freek list.

I don't think it is (there is no. 48, "Dirichlet's Theorem", but this refers to primes in arithmetic progression). But this is no reason not to include it :smile:

[Michael Stoll]

Oliver Nash said:

I suppose the statement here would be:

@[simp] lemma unit_add_circle.mem_add_approximable_real_iff {ξ : ℝ} :
  ↑ξ ∈ add_well_approximable unit_add_circle (λ n, 1/n^2) ↔ irrational ξ :=
sorry

Yes.

[Michael Stoll]

OK; I think I'll go forward with the PR and see what happens. So far it would just be adding one new file and not change anything that already exists.

[Oliver Nash]

Michael Stoll said:

I don't think it is (there is no. 48, "Dirichlet's Theorem", but this refers to primes in arithmetic progression).

Oops, yes; you're right.

[Alex J. Best]

That said "Pell's equation" is on the list, and while mathlib has some aspects of this theory it could definitely do with a lot more in order to claim we've really ticked this off. So I applaud this work and the idea of PRing it! I'd also be happy to review when the time comes.

[Michael Stoll]

#18019

[Michael Stoll]

The student has already written (sorry-free) code that proves the existence of nontrivial solutions to the Pell equation (for general positive non-square $d$), but this will need some overhaul to be fit for mathlib. This is only a matter of time, though.

[Michael Stoll]

#18019 has now passed CI. Reviews are welcome!

[Oliver Nash]

I was a bit slow but I finally got to this. I've left a long-ish comment on #18019

[Michael Stoll]

@Oliver Nash has suggsted to develop everythings in terms of add_circle, but I am not convinced that this is the best way at this point (but I'm open to a later refactor along these lines; the approach certainly has its merits). However, I have taken his suggestion as a prompt to obtain a better and shorter proof of the first main lemma by working with rationals instead of pairs of integers. A review would be welcome. @Alex J. Best (after the holidays)?

[Oliver Nash]

@Michael Stoll I did see your comments on GH that you're not convinced to formalise the result in the language of add_circle. That's fine: it's a subjective point and can even be considered somewhat of an implementation detail.

The only reason I haven't replied is that seasonal socialising left me no time for Lean today. Unfortunately I also have a very busy weekend but I hope to find some time for Lean tomorrow afternoon. Failing that I'll have lots of time on Monday.

[Michael Stoll]

@Oliver Nash Take your time - no problem :smile:

[Oliver Nash]

Oh one point I can quickly mention is that I think it is worth sharpening the result from |ξ - q| < 1 / (n * q.denom) to |ξ - q| ≤ 1 / ((n + 1) * q.denom)

[Oliver Nash]

If I do get time for Lean tomorrow I'm going to experiment with the following proof that I thought of while driving earlier (I hope this is correct!): consider the n+1 closed balls of radius δ/2 where δ := 1 / (n + 1) in unit_add_circle, centred on the points j • ξ 0 ≤ j ≤ n. We need to prove these are not pairwise disjoint. Assume for contradiction that they are. Then the measure of their union is the sum of their measures which is 1. Thus their union is almost equal to the whole space. However since the union is closed and the Haar measure satisfies is_open_pos_measure, any closed set that is almost equal to the whole space is the whole space. However this contradicts the connectedness of the circle.

[Michael Stoll]

The non-circle proof is roughly as follows. We consider the fractional parts of j * ξ for 0 ≤ j ≤ n as before, but now we partition the unit interval into n+1 equal parts. If the last interval is not hit, we can argue as before. Otherwise, say the fractional part of k * ξ is in the last interval. Then |k * ξ - (⌊k * ξ⌋ + 1)| ≤ 1/(n+1).

[Michael Stoll]

But perhaps the question is whether it is worth the effort to show the slightly stronger statement. Do you know of any result that relies on having n+1 instead of n?

[Michael Stoll]

Anyway, here is a proof (without circles :smile:):

import tactic
import data.real.basic
import algebra.algebra.basic
import combinatorics.pigeonhole

open finset int

/-- *Dirichlet's approximation theorem* -/
lemma dirichlet_approx (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
  ∃ j k : ℤ, 0 < k ∧ k ≤ n ∧ |ξ * k - j| ≤ 1 / (n + 1) :=
begin
  let f : ℤ → ℤ := λ m, ⌊fract (ξ * m) * (n + 1)⌋,
  have hn : 0 < (n : ℝ) + 1 := by exact_mod_cast nat.succ_pos _,
  have hfu := λ m : ℤ, mul_lt_of_lt_one_left hn $ fract_lt_one (ξ * ↑m),
  conv in (|_| ≤ _) { rw [le_div_iff hn, ← abs_of_pos hn, ← abs_mul], },
  let D := Icc 0 (n : ℤ),
  by_cases H : ∃ m ∈ D, f m = n,
  { obtain ⟨m, hm, hf⟩ := H,
    have hf' : (n : ℝ) ≤ fract (ξ * ↑m) * (↑n + 1),
    { have : (f m : ℝ) ≤ fract (ξ * ↑m) * (↑n + 1) := floor_le (fract (ξ * ↑m) * (↑n + 1)),
      rw hf at this,
      exact_mod_cast this, },
    have hm₀ : 0 < m,
    { have hf₀ : f 0 = 0,
      { simp only [floor_eq_zero_iff, algebra_map.coe_zero, mul_zero, fract_zero, zero_mul,
                   set.left_mem_Ico, zero_lt_one], },
      refine ne.lt_of_le (λ h, n_pos.ne _) (mem_Icc.mp hm).1,
      exact_mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n), },
    refine ⟨⌊ξ * m⌋ + 1, m, hm₀, (mem_Icc.mp hm).2, _⟩,
    rw [int.cast_add, ← sub_sub, sub_mul, int.cast_one, one_mul, abs_le],
    refine ⟨le_sub_iff_add_le.mpr _, sub_le_iff_le_add.mpr $ le_of_lt $
             (hfu m).trans $ lt_one_add _⟩,
    simpa only [neg_add_cancel_comm_assoc] using hf', },
  { simp_rw [not_exists] at H,
    have hD : (Ico 0 (n : ℤ)).card < D.card,
    { rw [card_Icc, card_Ico], exact lt_add_one n, },
    have hfu' : ∀ m, f m ≤ n := λ m, lt_add_one_iff.mp (floor_lt.mpr (by exact_mod_cast hfu m)),
    have hwd : ∀ m : ℤ, m ∈ D → f m ∈ Ico 0 (n : ℤ) :=
      λ x hx, mem_Ico.mpr ⟨floor_nonneg.mpr (mul_nonneg (fract_nonneg (ξ * x)) hn.le),
                           ne.lt_of_le (H x hx) (hfu' x)⟩,
    have : ∃ (x : ℤ) (H : x ∈ D) (y : ℤ) (H : y ∈ D), x < y ∧ f x = f y,
    { obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd,
      rcases lt_trichotomy x y with h | h | h,
      exacts [⟨x, hx, y, hy, h, hxy⟩, false.elim (x_ne_y h), ⟨y, hy, x, hx, h, hxy.symm⟩], },
    obtain ⟨x, hx, y, hy, x_lt_y, hxy⟩ := this,
    refine ⟨⌊ξ * y⌋ - ⌊ξ * x⌋, y - x, sub_pos_of_lt x_lt_y,
            sub_le_iff_le_add.mpr $ le_add_of_le_of_nonneg (mem_Icc.mp hy).2 (mem_Icc.mp hx).1, _⟩,
    convert_to |fract (ξ * y) * (n + 1) - fract (ξ * x) * (n + 1)| ≤ 1,
    { congr, push_cast, simp only [fract], ring, },
    exact (abs_sub_lt_one_of_floor_eq_floor hxy.symm).le, }
end

[Kevin Buzzard]

Mathlib going that extra mile :-)

[Michael Stoll]

Should I add this? (and then, I guess, refactor the rest to use it...)

[Michael Stoll]

OK; I have just done it.

[Yury G. Kudryashov]

Can you prove one of the implications using existing code about continued fractions?

[Yury G. Kudryashov]

(or do you already use it?)

[Yaël Dillies]

Continued fractions don't seem to be used in there, from import considerations.

[Michael Stoll]

Do we have continued fractions? where?

[Michael Stoll]

docs#continued_fraction

[Michael Stoll]

I had been looking in the number_theory folder...

[Michael Stoll]

I don't think there is anything in algebra.continued_fraction.* that says something on the standard continued fraction expansion of a real number and on the (speed of) convergence of the convergence to said number.

[Michael Stoll]

I do have another proof using continued fractions (which I have been playing around with a bit using my own set-up, not being aware of the existing material), BTW. One can actually prove a slightly stronger result this way, so maybe I'll try to add that at some later point.

[Yaël Dillies]

Michael Stoll said:

I had been looking in the number_theory folder...

Always, always, keep a tab with the mathlib docs open :grinning_face_with_smiling_eyes:

[Michael Stoll]

That doesn't help if you are not even thinking cfs might be there if they are not under number_theory... :frown:

[Yaël Dillies]

Whatever I am looking for, I give a try to the docs search box. In that case, you would have found continued_fraction right away.

[Michael Stoll]

I'll try to remember that...

[Yaël Dillies]

I know it's easy after the fact to say "I do X and doing X would have helped you", but in that case I truly believe what I'm telling you and apply it to myself (in fact, I have one mathlib docs tab per Chrome window).

[Yury G. Kudryashov]

It would be nice to have a proof of the following 2 facts:

• $\frac{p_n}{q_n}\le α\le \frac{p_{n+1}}{q_{n+1}}$ (either for even or odd n);
• $|p_nq_{n+1}-p_{n+1}q_n|=1$.

@Sebastien Gouezel AFAIR, you reviewed the continued fractions PRs. Do we have either of these facts?

[Yury G. Kudryashov]

@Kevin Kappelmann, you wrote this code. Do we have either of these theorems?

[Michael Stoll]

Michael Stoll said:

I don't think there is anything in algebra.continued_fraction.* that says something on the standard continued fraction expansion of a real number and on the (speed of) convergence of the convergence to said number.

There is something, e.g., docs#generalized_continued_fraction.abs_sub_convergents_le' and docs#generalized_continued_fraction.terminates_iff_rat, from which one could construct a proof, I suppose.

[Michael Stoll]

Yury G. Kudryashov said:

It would be nice to have a proof of the following 2 facts:

• $\frac{p_n}{q_n}\le α\le \frac{p_{n+1}}{q_{n+1}}$ (either for even or odd n);
• $|p_nq_{n+1}-p_{n+1}q_n|=1$.

The second one is docs#generalized_continued_fraction.determinant (as an equality with the sign).

[Michael Stoll]

The first can probably be deduced from docs#generalized_continued_fraction.sub_convergents_eq .

[Michael Stoll]

As far as I can see, continued fractions are not used anywhere outside of algebra/continued_fractions/ in mathlib.
One thing that seems to be missing is the statement that a continued fraction (with integral entries, all positive except possibly the head) converges to a real number and that this leads to a bijection between (infinite) continued fractions and irrational real numbers.

[Yury G. Kudryashov]

Convergence immediately follows from the estimates (either docs#generalized_continued_fraction.abs_sub_convergents_le' or docs#generalized_continued_fraction.abs_sub_convergents_le).

[Yury G. Kudryashov]

Plus the fact that the denominators tend to infinity. Do we have this?

[Yury G. Kudryashov]

We have of_denom_mono but not of_denom_strict_mono (yet)

[Yury G. Kudryashov]

We have docs#generalized_continued_fraction.of_convergence

[Yury G. Kudryashov]

It uses local attribute [instance] preorder.topology. Should be changed to [topological_space K] [order_topology K]

[Yury G. Kudryashov]

I have family duties. I'll look into this later tonight or tomorrow in the morning.

[Oliver Nash]

In another direction, I think it's nice to regard Dirichlet's approximation as a special case of a result about compact, connected normed groups. I've only had brief fragments of time for the last few days but I've just managed to cobble together a sorry-free illustration.

[Oliver Nash]

First a bunch of "library code" (which needs a lot of polish). Nothing specific to Dirichlet here:

import measure_theory.group.add_circle

noncomputable theory

open set metric measure_theory measure_theory.measure

lemma measurable_set.ae_eq_univ'
  {α : Type*} [measurable_space α] {μ : measure α} [is_finite_measure μ]
  {s : set α} (hs : measurable_set s) :
  s =ᵐ[μ] univ ↔ μ s = μ univ :=
begin
  rw [ae_eq_univ, measure_compl hs (measure_ne_top μ s), tsub_eq_zero_iff_le],
  refine ⟨λ h, le_antisymm (measure_mono $ subset_univ s) h, λ h, _⟩,
  rw h,
  exact le_refl _,
end

-- namespace measure_theory.measure.is_open_pos_measure
namespace is_open_pos_measure

variables {X : Type*} [topological_space X] {m : measurable_space X} {μ : measure X}
  [is_open_pos_measure μ] [opens_measurable_space X]

lemma closed_lt_measure_univ [is_finite_measure μ]
  (F : set X) (hF : is_closed F) (hF' : F ≠ univ) : μ F < μ univ :=
begin
  suffices : μ Fᶜ ≠ 0, { simpa [measure_compl hF.measurable_set (measure_ne_top μ F)] using this, },
  exact is_open_pos_measure.open_pos Fᶜ hF.is_open_compl (nonempty_compl.mpr hF'),
end

variables (μ)

lemma eq_univ_of_ae_eq_univ [is_finite_measure μ]
  {F : set X} (hF : is_closed F) (hF' : F =ᵐ[μ] univ) : F = univ :=
begin
  by_contra contra,
  replace contra : μ F ≠ μ univ := (closed_lt_measure_univ F hF contra).ne,
  apply contra,
  simpa only [hF.measurable_set.ae_eq_univ'] using hF',
end

end is_open_pos_measure

lemma card_le_one_of_closed_disjoint_Union_eq_univ
  {ι α : Type*} [topological_space α] [preconnected_space α] [finite ι] {s : ι → set α}
  (h_nonempty : ∀ i, (s i).nonempty)
  (h_closed : ∀ i, is_closed (s i))
  (h_disj : pairwise (disjoint on s))
  (h_Union : (⋃ i, s i) = univ) :
  nat.card ι ≤ 1 :=
begin
  replace h_nonempty : ∀ i, s i ≠ ∅, { intros i, rw ← nonempty_iff_ne_empty, exact h_nonempty i, },
  have h_clop : ∀ i, is_clopen (s i),
  { intros i,
    refine ⟨_, h_closed i⟩,
    rw [← is_closed_compl_iff, compl_eq_univ_diff, ← h_Union, Union_diff],
    refine is_closed_Union (λ j, _),
    rcases eq_or_ne i j with rfl | h_ne, { simp, },
    rw (h_disj h_ne.symm).sdiff_eq_left,
    exact h_closed j, },
  by_contra h_card,
  haveI : fintype ι := fintype.of_finite ι,
  rw [not_le, nat.card_eq_fintype_card] at h_card,
  obtain ⟨i, -, j, -, h_ne⟩ := finset.one_lt_card.mp h_card,
  replace h_ne : s i ∩ s j = ∅, { erw [eq_bot_iff, ← disjoint_iff_inf_le], exact h_disj h_ne, },
  cases is_clopen_iff.mp (h_clop i) with hi hi, { exact h_nonempty i hi, },
  rw [hi, univ_inter] at h_ne,
  exact h_nonempty j h_ne,
end

lemma set.exists_ne_mem_inter_of_not_pairwise_disjoint
  {ι α : Type*} {s : ι → set α} (hs : ¬ pairwise (disjoint on s)) :
  ∃ i j (h : i ≠ j) x, x ∈ s i ∩ s j :=
begin
  change ¬ ∀ ⦃i j⦄, i ≠ j → ∀ ⦃t⦄, t ≤ s i → t ≤ s j → t ≤ ⊥ at hs,
  simp only [not_forall] at hs,
  obtain ⟨i, j, h_ne, t, hi, hj, ht⟩ := hs,
  replace ht : t.nonempty,
  { rwa [le_bot_iff, bot_eq_empty, ← ne.def, ← nonempty_iff_ne_empty] at ht, },
  obtain ⟨x, hx⟩ := ht,
  exact ⟨i, j, h_ne, x, hi hx, hj hx⟩,
end

lemma set.exists_ne_mem_inter_of_not_pairwise_disjoint'
  {ι α : Type*} [linear_order ι] {s : ι → set α} (hs : ¬ pairwise (disjoint on s)) :
  ∃ i j (h : i < j) x, x ∈ s i ∩ s j :=
begin
  obtain ⟨i, j, hne, x, hx₁, hx₂⟩ := set.exists_ne_mem_inter_of_not_pairwise_disjoint hs,
  cases lt_or_lt_iff_ne.mpr hne with h_lt h_lt,
  { exact ⟨i, j, h_lt, x, hx₁, hx₂⟩, },
  { exact ⟨j, i, h_lt, x, hx₂, hx₁⟩, },
end

@[to_additive] instance seminormed_group.measurable_space
  (A : Type*) [seminormed_group A] : measurable_space A :=
borel A

@[to_additive] instance seminormed_group.borel_space
  (A : Type*) [seminormed_group A] : borel_space A :=
⟨rfl⟩

[Oliver Nash]

However given the above we can prove:

/-- *Dirichlet's approximation theorem*.

TODO:
 * Drop the redundant hypothesis `hδ'`,
 * `to_additive`-ize (currently missing additive version of `add_haar_closed_ball_center`). -/
lemma exists_norm_nsmul_le (A : Type*) (ξ : A) (n : ℕ)
  [normed_add_comm_group A] [connected_space A] [compact_space A]
  {μ : measure A} [is_add_haar_measure μ]
  (hn : 0 < n) (δ : ℝ) (hδ : (n + 1) • μ (closed_ball (0 : A) (δ/2)) = μ univ) (hδ' : 0 ≤ δ) :
  ∃ (j ∈ Ioc 0 n), ‖j • ξ‖ ≤ δ :=
begin
  haveI : is_finite_measure μ := compact_space.is_finite_measure,
  let B : Icc 0 n → set A := λ j, closed_ball ((j : ℕ) • ξ) (δ / 2),
  have hB : ∀ j, is_closed (B j) := λ j, is_closed_ball,
  suffices : ¬ pairwise (disjoint on B),
  { obtain ⟨i, j, hij, x, hx⟩ := set.exists_ne_mem_inter_of_not_pairwise_disjoint' this,
    refine ⟨j - i, ⟨by rwa [tsub_pos_iff_lt, subtype.coe_lt_coe], _⟩, _⟩,
      { simpa only [tsub_le_iff_right] using j.property.2.trans le_self_add, },
      { rw [sub_nsmul _ (subtype.coe_le_coe.mpr hij.le), ← sub_eq_add_neg, ← dist_eq_norm],
        refine (dist_triangle (↑j • ξ) x (↑i • ξ)).trans _,
        linarith [mem_closed_ball.mp hx.1, mem_closed_ball'.mp hx.2], }, },
  by_contra h,
  have h' : (⋃ j, B j) = univ,
  { refine is_open_pos_measure.eq_univ_of_ae_eq_univ μ (is_closed_Union hB) _,
    have h_meas : measurable_set (⋃ j, B j) :=
      measurable_set.Union (λ j, is_closed_ball.measurable_set),
    simp_rw [h_meas.ae_eq_univ', measure_Union h (λ j, measurable_set_closed_ball), tsum_fintype,
      add_haar_closed_ball_center μ, finset.sum_const, finset.card_univ, nat.card_fintype_Icc,
      tsub_zero, hδ], },
  have h'' : ∀ j, (B j).nonempty, { intros j, rw nonempty_closed_ball, positivity, },
  simpa [nat.card_eq_fintype_card, nat.card_fintype_Icc, hn.ne'] using
    card_le_one_of_closed_disjoint_Union_eq_univ h'' hB h h',
end

[Oliver Nash]

Which I think is quite nice, partly because it's very conceptual and partly because it holds more generally. I admit I can't think of compact commutative normed groups other than tori, but still.

[Oliver Nash]

I have now run out of fragments of time but I will review #18019 tomorrow.

[Michael Stoll]

Even if it applies only to tori (and products of such with finite abelian groups, I guess), this would be a good result to have, I think.

[Oliver Nash]

Thanks, I am tempted to polish this result up and make a PR. (I'm happy to do this if a reviewer requests it.) However I think in good conscience I should stop contributing to Mathlib3 and start helping out with the port to Mathlib4.

[Michael Stoll]

@Oliver Nash suggests moving the results in #18019 into the real namespace (instead of dioph_approx, which is the namespace that is currently used). I'd lilke to have some more input on that before I change it.

[Michael Stoll]

/poll Which namespace should the material of #18019 be in?
dioph_approx
real

[Yury G. Kudryashov]

Why not use continued fractions? This would make the proof much shorter.

[Junyan Xu]

This looks like a nice summary of results about approximation by continued fraction.

[Michael Stoll]

Yury G. Kudryashov said:

Why not use continued fractions? This would make the proof much shorter.

Given Dirichlet's approximation theorem (which is good to have independently and which I don't see how to get using continued fractions), "the proof" (that there are infinitely many rational q s.t. |ξ - q| < 1/q.denom^2) is only lines 267-304 in the file. Most of the remaining code is about showing that for rational ξ, there are only finitely many (which, I think, also cannot be done using continued fractions) and the equivalence between the pairs of integers version and the rational numbers version.

But of course, you can prove somewhat stronger results regarding infinitely many "good" approximations with continued fractions (the best one being Hurwitz's theorem), so it would be nice if somebody did it. But I guess it will need more than about 40 lines of code to get there. It would also be nice to have what is called Legendre's theorem in the link proved by @Junyan Xu.

[Michael Stoll]

Following a suggestion by @Oliver Nash and @Riccardo Brasca, I have now cut down #18019 to the part that proves various versions of Dirichlet's approximation theorem and the part that deduces the infinitude of good rational approximations to irrational real numbers. I think it makes sense to also merge that last part (about 30 lines) now instead of waiting for someone to do it using continued fractions (which will require some more work, for which I don't have time right now).

[Michael Stoll]

#18193 now adds the converse statement (rational numbers have only finitely many good rational approximations) and the "iff" version.

[Michael Stoll]

Thanks @Oliver Nash @Riccardo Brasca! I have made the suggested changes and pushed it on the merge queue.

[Oliver Nash]

Thank you and Michael Geißer for doing this. It's a useful result!

[Michael Stoll]

I have now formalized a proof of a theorem of Legendre on continued fractions:

If $\xi \in \mathbb R$ and $q \in \mathbb Q$ are such that $|\xi - q| < 1 /2q^2$, then $q$ is a convergent of the continued fraction expansion of $\xi$:

Given

open int

noncomputable def convergent : ℝ → ℕ → ℚ
| ξ 0 := ⌊ξ⌋
| ξ (n + 1) := ⌊ξ⌋ + 1 / convergent (1 / fract ξ) n

we have

lemma ex_rat_eq_convergent {ξ : ℝ} {q : ℚ} (h : |ξ - q| < 1 / (2 * q.denom ^ 2)) :
  ∃ n, q = convergent ξ n := ...

I have managed to condense this to about 230 lines of code.

Would it make sense to turn this into a PR now? (If so, I'll hook this up with the existing continued_fractions in mathlib first.)

[Kevin Buzzard]

Do you need to touch any ported files? If not then I would be tempted to go for it

[Michael Stoll]

There is one lemma,

lemma fract_pos {ξ : ℝ} (hξ : ξ ≠ ⌊ξ⌋) : 0 < fract ξ :=
self_sub_floor ξ ▸ sub_pos.mpr $ hξ.lt_of_le' $ floor_le ξ

which (suitably generalized to linearly ordered floor rings) could in principle go into algebra.order.floor. Everything else would go into a new file.
I would suggest to put this lemma also in the new file and add a note that it should be moved when the new file gets ported (which I may perhaps do myself when the time comes).

[Yaël Dillies]

I think that's better to forward port than to place it in the wrong place purposefully.

[Michael Stoll]

I can PR the lemma (perhaps including an iff version) to mathlib3. Could you @Yaël Dillies perhaps take care of the mathlib4 side? I have to admit that at this point I'm a bit scared by everything lean 4 and mathlib4. But my plan is to look into lean 4 (and then medium-term also help with porting) after the teaching period here has finished (a few weeks from now) and I have more bandwidth for learning new stuff...

[Johan Commelin]

The port has reached a point where a whole bunch of annoying basics have been done, and the tooling is also steadily improving. So 2 weeks from now, I'm sure we'll have some nice entry point for you (-;

[Michael Stoll]

That's what I'm hoping for :smile:

[Yaël Dillies]

Sure, why not. Just tag me on the PR you want a forward port of.

[Michael Stoll]

OK, will do.

[Michael Stoll]

#18317

[Oliver Nash]

Michael Stoll said:

I have now formalized a proof of a theorem of Legendre on continued fractions:

If $\xi \in \mathbb R$ and $q \in \mathbb Q$ are such that $|\xi - q| < 1 /2q^2$, then $q$ is a convergent of the continued fraction expansion of $\xi$:

This is nice, I'm delighted this result is on its way.

I can't resist using this as an opportunity to advertise a nice lemma of Cassels which shows that corresponding rational approximations are true up to sets of measure zero for any positive constant:

import number_theory.well_approximable

open set filter measure_theory
open_locale topological_space

local notation `𝕊` := unit_add_circle

lemma foo : (add_well_approximable 𝕊 (λ n, 1 / n^2) : set 𝕊) =ᵐ[volume] univ :=
sorry -- Corollary of Dirichlet.

lemma bar {M : ℝ} (hM : 0 < M) :
  (add_well_approximable 𝕊 (λ n, M * (1 / n^2)) : set 𝕊) =ᵐ[volume] univ :=
begin
  have hr : tendsto (λ (n : ℕ), (1 : ℝ) / n^2) at_top (𝓝 0),
  { -- Seems lots of missing API for these limits!?
    simp only [one_div, sq],
    exact tendsto_inv_at_top_zero.comp (tendsto.at_top_mul_at_top
      tendsto_coe_nat_at_top_at_top tendsto_coe_nat_at_top_at_top), },
  exact ae_eq_trans (blimsup_thickening_mul_ae_eq _ _ _ hM _ hr) foo,
end

[Michael Stoll]

Nice.

It would be good to have API lemmas like

lemma unit_add_circle.infinite_order_iff_irrational {a : ℝ} : ¬ is_of_fin_add_order (a : 𝕊) ↔ irrational a

lemma unit_add_circle.infinite_order_full_measure : {a : 𝕊 | ¬ is_of_fin_add_order a} =ᵐ[volume] univ

lemma unit_add_circle.add_well_approximable_iff {a : ℝ} {f : ℕ → ℝ) :
  add_well_approximable 𝕊 f (a : 𝕊) ↔ {q : ℚ | (|a - q| : ℝ) < f q.denom}.infinite

to derive foo easily.

[Michael Stoll]

Michael Stoll said:

I can PR the lemma (perhaps including an iff version) to mathlib3. Could you Yaël Dillies perhaps take care of the mathlib4 side? (...)

Yaël Dillies said:

Sure, why not. Just tag me on the PR you want a forward port of.

@Yaël Dillies I've requested a review of #18317 from you. Should I also do something else?

[Yaël Dillies]

Sorry, I was away from my computer all of yesterday!

[Michael Stoll]

No problem. Thanks for the reivew!

[Michael Stoll]

I have now wrangled my way sufficiently through the continued_fraction API to be able to show that

variables {K : Type*} [linear_ordered_field K] [floor_ring K]

lemma generalized_continued_fraction.convergents'_succ (ξ : K) (n : ℕ) :
  (generalized_continued_fraction.of ξ).convergents' (n + 1) =
  ⌊ξ⌋ + 1 / (generalized_continued_fraction.of (fract ξ)⁻¹).convergents' n :=

But it needed some 150 lines of additional API to be written first...

[Michael Stoll]

Generally speaking, I find the implementation of continued fractions in mathlib a bit heavy. What is particularly annoying is that you have to write generalized_continued_fraction.of ξ, since this is protected, and dot notation does not work. (For real ξ, one could define real.gcf (ξ : real) : ... := ... and then write ξ.gcf.) Since any linear_ordered_field that is also a floor_ring has a unique order-preserving embedding into the reals, it would not really be a loss of generality to just work with reals.

[Michael Stoll]

What I also do not like so much is that the convergents etc. that you get will have the type of ξ, even though the convergents are canonically rational numbers. So I have decided that for my purposes it is best to keep the definition

noncomputable def real.convergent : ℝ → ℕ → ℚ
| ξ 0 := ⌊ξ⌋
| ξ (n + 1) := ⌊ξ⌋ + 1 / convergent (1 / fract ξ) n

(which is nice and clean, allows dot notation ξ.convergent n and produces rational numbers) and work with it in the proof (of Legendre's theorem).

[Michael Stoll]

I propose the following:

• Make one PR that adds the proof based on real.convergent as above (I think this can go into number_theory.diophantine_approximation)
• Make another independent PR adding API lemmas for continued fractions
• Once both are merged, make a third PR with a proof that both definitions of convergents agree and a version of the theorem using (generalized_continued_fraction.of ξ).convergents

Does this sound reasonable?

[Yaël Dillies]

Re generalized_continued_fraction.of, what about introducing localized notation, akin to docs#cardinal.mk?

[Michael Stoll]

Any suggestions as to what would be sensible notation?

[Junyan Xu]

Well, it could just be a regular name like gcf_of

[Michael Stoll]

OK; presumably this would be part of the second PR and go where generalized_continued_fraction.of is defined.

[Michael Stoll]

Any thoughts about the proposal above?

[Michael Stoll]

After being busy for a week, I now found the time to make the PR adding the API lemmas to the various continued_fractions files that are necessary to prove the recurrence relation for the convergents. This is #18434, and it has passed CI. Reviews are welcome!

[Michael Stoll]

Since the only thing that seems to prevent porting the continued_fraction files is data.seq.seq, which is currently in progress, it would be nice to get the added API lemmas in soon. I would think all of this is pretty straight-forward and so should not be hard to review.

[Michael Stoll]

Thanks, @Johan Commelin ! (LaTeX formatting of the continued fractions in the docs will hit mathlib soon - #18459 .)

[Michael Stoll]

I have now added the proof of Legendre's Theorem to number_theory.diophantine_approximation: #18460

[Oliver Nash]

Oliver Nash said:

Thanks, I am tempted to polish this result up and make a PR. (I'm happy to do this if a reviewer requests it.) However I think in good conscience I should stop contributing to Mathlib3 and start helping out with the port to Mathlib4.

With the port complete, I finally did this in #6033