Extending the domain of def of a continuous real function

Stream: new members

[Alex Brodbelt]

I am playing around within the continuous world and filters and I believe I have encountered my first diamond :diamonds: (edit: not a diamond)

I have a continuous function $f : \mathbb{R} \rightarrow \mathbb{R}$ that when restricted to the rationals equals $g : \mathbb{Q} \rightarrow \mathbb{R}$.

The concrete case I am working on is the following :

import Mathlib

open Polynomial

example {a b c : ℝ} (f : ℝ → ℝ) (f_cont : Continuous f) (hf : ∀ q : ℚ, f q = (C a * X^2 + C b * X + C c).eval q) : f = (C a * X^2 + C b * X + C c).eval := by
    have P_cont : Continuous ((C a * X^2 + C b * X + C c).eval) := Polynomial.continuous_eval₂ (C a * X ^ 2 + C b * X + C c) (RingHom.id ℝ)
    have := AbstractCompletion.funext rationalCauSeqPkg f_cont P_cont hf -- unhappy here
    sorry

Question 1: How does one deal with or avoid diamonds?

Question 2: How does one prove this statement in an idiomatic style for the more general setting of say extending a function from a metric space to another? (In fairness, I expect this might be easier since $\mathbb{R}$ is already a very intricate construction). I wonder the same in the case where it is a function from a topological space to another? But this is where I begin to have not thought too hard about this.

The informal way I am thinking is extract a representative cauchy sequence for an arbitrary real number, show that continuity allows to show that the equality hf is "preserved in the limit". But this seems like a lot of work (fun to do once) to do in Lean for something not very exciting.

In general, I am curious about what is the workflow or style of argument for this kind of problem in mathlib and people more familiar with this part of the library? I read the topology section of MIL (which is very nice) and did not find anything which seemed relevant.

Apologies for the rambling, I just find this quite interesting and I am trying to get a good sense for what is going on.

Thanks

[Bjørn Kjos-Hanssen]

Can you post a #mwe ? :grinning_face_with_smiling_eyes:

[Yakov Pechersky]

I think rationalCauSeqPkg is an implementation detail that isn't meant to be used directly.

[Yakov Pechersky]

Or, Rat.uniformSpace_eq can help, checking how.

[Yakov Pechersky]

IIUC, the idiomatic way is via Dense.extend

[Etienne Marion]

The issue is that rationalCauSeqPkg comes with a certain uniform space structure on Rat which is not definitionally equal to the one inferred by typeclass inference, i.e. the one declared as an instance in Mathlib (which is PseudoMetricSpace.toUniformSpace). Although they are propositionally equal as shown by Rat.uniformSpace_eq, as pointed by Yakov.

[Yakov Pechersky]

I would point out that I can't tell what your g : Rat -> Rat is, since your polynomial in the example has real coefficients, not rational ones.

[Etienne Marion]

You could use DenseRange.equalizer along with Rat.denseRange_cast.

[Etienne Marion]

Also even if we answered quickly here, please note the remark of Bjørn: your code lacks imports and namespaces so it does not compile when pasted in an editor. In this case the fix was ok but in general you are unlikely to get answers here if you don't provide a #mwe because people do not want to lose time trying to fix the example.

[Yakov Pechersky]

Thanks Etienne, that's a great pointer:

import Mathlib

open Polynomial

example {a b c : ℚ} (f : ℝ → ℝ) (f_cont : Continuous f) (hf : ∀ q : ℚ, f q = (C a * X^2 + C b * X + C c).aeval q) :
    f = fun x : ℝ ↦ (C a * X^2 + C b * X + C c).aeval x := by
  apply Rat.denseRange_cast.equalizer
  · assumption
  · exact Polynomial.continuous_aeval _
  · funext
    simp [hf]

[Alex Brodbelt]

Ah apologies for not checking if it was an #mwe and the typos.... (should not have posted late at night). Many thanks Yakov Pechersky and Etienne Marion !

I guess in hindsight I should have thought about searching for a theorem involving denseness...

Regarding what Etienne Marion said, how would you use Rat.uniformSpace_eq to resolve the typeclass inference issue? Do you feed in the theorem to some simplifier? Or has this got to do more with the elaborator? What is the name for this kind of problem (diamond?) ? Is there somewhere I can read about this?

[Etienne Marion]

What you could do for instance would be to write (Rat.uniformSpace_eq ▸ rationalCauSeqPkg) to rewrite the instance inside rationalCauSeqPkg. However this will not solve other problems, starting with the fact that AbstractCompletion.funext takes in arguments functions whose codomain is an AbstractCompletion Rat while your functions codomain is Real, which is different (although isomorphic). This is all explained in the file Mathlib.Topology.UniformSpace.CompareReals, which provides a different way of building real numbers and checks that it gives something isomorphic, but is only here as an illustration and is not meant to be used.

I am not sure if this can really be called a diamond. I think (not sure though) a diamond is rather something that appears when two non definitionally equal instances can be synthesized for the same type. What is happening here is different: the instance used in rationalCauSeqPkg is not synthesized by typeclass inference, it is simply different from the one which is synthesized. I don't know the name of this or if it is documented somewhere, but in practice it should not happen if you are careful with the instances you use because instances are supposed to be unique. However there is one case in which this problem appears: it is common in probability theory to restrict a measure to a smaller sigma-algebra, and thus we get two different MeasurableSpace structure for the same type, which causes the same issue. This is why it is now asked that if a lemma refers to a measure, the MeasurableSpace argument must not be a typeclass argument (i.e. it should not be synthesized but rather inferred from the one used by the measure).