Real as limit of sequence of rationals

Stream: Is there code for X?

[Xavier Roblot]

I am having a hard time working with limits in mathlib. For example, how would I write the fact that a real number $r$ is a limit of a sequence of rationals?

[Adam Topaz]

This is true by definition ;)

import data.real.basic

example (a : ℝ) : ∃ s : cau_seq ℚ abs, real.mk s = a :=
begin
  rcases a with ⟨⟨a⟩⟩, use a, refl,
end

[Adam Topaz]

I don't know if we have such a lemma though

[Adam Topaz]

Besides, one should probably use filters as opposed to sequences

[Xavier Roblot]

Yes, I realised that my question was a bit stupid since it is actually how the reals are defined in mathlib...

Ok, so what I have in mind is: how to prove the following lemma using the fact that reals are limits of sequence of rationals?

import topology.metric_space.basic

example (f : ℝ → ℝ) (h1 : continuous f) (h2 : ∀ q : ℚ, f q = q) : ∀ x : ℝ, f x = x := sorry

[Junyan Xu]

I found docs#dense_inducing.extend_unique the other day

[Junyan Xu]

Oh and we have docs#rational_cau_seq_pkg and docs#abstract_completion.dense_inducing ! See below for a better solution using docs#rat.dense_embedding_coe_real directly.

[Jireh Loreaux]

There's also docs#dense_inducing.extend_eq (for the first approach)

[Jireh Loreaux]

But was your point that you want to do this explicitly via limits of sequences of rational for pedagogical reasons?

[Junyan Xu]

Sorry? extend_eq seems just asserting the constructed extend is actually an extension. I can't see how it helps...

[Xavier Roblot]

These results looks great but still very powerful for the purpose. Surely, there is a way to use docs#continuous.lim_eq and the fact that x is a limit a sequence of rationals? And, as suggested by @Jireh Loreaux , I certainly need to know more about using limits in mathlib so having a proof using limits would make me even more happy :grinning:

In fact, I don't know even how to simply state the fact that the real x is the limit of rational numbers using filters.

[Jireh Loreaux]

@Junyan Xu If you use docs#dense_inducing.extend_unique you get that extension of some function (in this case, the identity) on the rationals is equal to some other function (in our case, f), but then you need to know that the extension of the identity on rationals is the identity on the reals. Hence docs#dense_inducing.extend_eq.

[Junyan Xu]

The identity function on the reals is also a continuous function that is identity on the rationals. So both it and f equals extend, so they're equal.

[Jireh Loreaux]

This says the real number x is the limit of some sequence of rational numbers.

example (x : ℝ) : ∃ (seq : ℕ → ℚ), filter.tendsto (λ n, (seq n : ℝ)) filter.at_top (𝓝 x) := sorry

[Junyan Xu]

I admit I didn't think of this argument and thought something is missing when I saw docs#dense_inducing.extend_unique the first time ...

[Jireh Loreaux]

But do you need this for pedagogical purposes? That is, are you trying to teach something to students with this? If not, I would encourage going the abstract route; it's frequently the way to go.

[Xavier Roblot]

Jireh Loreaux said:

This says the real number x is the limit of some sequence of rational numbers.

example (x : ℝ) : ∃ (seq : ℕ → ℚ), filter.tendsto (λ n, (seq n : ℝ)) filter.at_top (𝓝 x) := sorry

Thanks. Do you need some special code to make the 𝓝 works? I get unknown identifier '𝓝' on my side.

[Xavier Roblot]

Jireh Loreaux said:

But do you need this for pedagogical purposes? That is, are you trying to teach something to students with this? If not, I would encourage going the abstract route; it's frequently the way to go.

Indeed. Let's say I'll do both :grinning_face_with_smiling_eyes:

[Patrick Massot]

Guys, you should stop frightening Xavier now.

[Patrick Massot]

import topology.instances.rat

example (f : ℝ → ℝ) (h1 : continuous f) (h2 : ∀ q : ℚ, f q = q) : ∀ x : ℝ, f x = x :=
by simp [rat.dense_embedding_coe_real.dense.equalizer h1 continuous_id (by ext q ; simpa using h2 q)]

[Jireh Loreaux]

For 𝓝, use open_locale topological_space

[Xavier Roblot]

Well, I guess that answer the question but I am still going to need a little time to process that answer.

Anyway, thanks everybody. I think I have enough to produce three different proofs of the lemma now.

[Adam Topaz]

BTW, this fails for some reason...

import topology.uniform_space.compare_reals

example (f : ℝ → ℝ) (h1 : continuous f) (h2 : ∀ q : ℚ, f q = q) :
  ∀ x : ℝ, f x = x :=
begin
  intros x,
  have := rational_cau_seq_pkg.induction_on x,
  sorry
end

[Adam Topaz]

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  pseudo_metric_space.to_uniform_space
inferred
  is_absolute_value.uniform_space abs

[Patrick Massot]

Xavier, you can make it easier to decipher by stating both the assumption and the conclusion in a more convenient way:

example (f : ℝ → ℝ) (h1 : continuous f) (h2 : f ∘ (coe : ℚ → ℝ) = id ∘ coe) : f = id :=
rat.dense_embedding_coe_real.dense.equalizer h1 continuous_id h2

[Patrick Massot]

This means that simp and simpa in my first snippet are only used to bridge that gap.

[Patrick Massot]

Adam, this sounds pretty bad. It means then when we refactored to introduce pseudo_metric_space we created some bad diamond. But it should move to another thread.

[Adam Topaz]

I'll repost in general

[Xavier Roblot]

@Patrick Massot, in rat.dense_embedding_coe_real.dense.equalizer, I think I see where the part rat.dense_embedding_coe_real comes from, but I cannot find to which function the part dense.equalizer relates to.

[Jireh Loreaux]

It's docs#dense_range.equalizer

[Jireh Loreaux]

If you have it open in VS Code, you should be able to hover over the pieces to see what the declaration is.

[Jireh Loreaux]

It's also using the fact that docs#dense_embedding extends docs#dense_inducing, which has a field dense that says the map has docs#dense_range. Do you know about dot notation in Lean, and how that works?

[Xavier Roblot]

Thanks for the explanation.

Jireh Loreaux said:

Do you know about dot notation in Lean, and how that works?

Well, I thought I did. Maybe I'll have to think about it a bit more to understand what happens here.

[Jireh Loreaux]

This is the dot notation unfolded:

dense_range.equalizer (dense_inducing.dense (dense_embedding.to_dense_inducing rat.dense_embedding_coe_real)) h1 continuous_id h2

Note that with dot notation, the explicit map dense_embedding.to_dense_inducing can be omitted because the structure dense_embedding extends dense_inducing and dense_inducing.dense is one of the fields of the latter.

[Jireh Loreaux]

So, rat.dense_embedding_coe_real is a dense_embedding which we can plug into dense_inducing.dense (because Lean sees this .dense as a field of dense_embedding also, as described above). This results in rat.dense_embedding_coe_real.dense : dense_range (coe : ℚ → ℝ), which we can then plug into dense_range.equalizer.

[Jireh Loreaux]

Does that make sense?

[Xavier Roblot]

It does. Thanks a lot :tada:

[Matt Diamond]

FYI you can use docs#rat.dense_range_cast to get your dense_range proof without needing to go through the embedding