Increasing function which is linear or rationals is linear

Stream: new members

[Martin Dvořák]

I am trying to formalize a solution from a mathematical competition and, as a part of the proof, I need the following lemma:

If f is an increasing function on positive reals and f is linear on positive rationals, then f must be linear on positive reals.

MWE:

import data.real.basic

lemma lin_on_real {f : ℝ → ℝ}
  (increasing : ∀ x y : ℝ,  0 < x  →  x < y  →  f x < f y)
  (lin_on_rat : ∀ x : ℚ,  0 < x  →  f x = f 1 + (x - 1) * (f 2 - f 1)
  ) :           ∀ x : ℝ,  0 < x  →  f x = f 1 + (x - 1) * (f 2 - f 1)  :=
begin
  sorry,
end

[Ruben Van de Velde]

Any reason you're not using \Q?

[Martin Dvořák]

Thanks, I'll edit it!

[Ruben Van de Velde]

Just guessing vaguely: is there anything relevant in https://leanprover-community.github.io/mathlib_docs/topology/dense_embedding.html ?

[Martin Dvořák]

Unfortunately, the link didn't help me. I don't understand this abstract math, which is obviously a big problem for me if I want to work with mathlib, since almost all mathematical results that are relevant for me are special cases of some more abstract results, and these abstract results are in mathlib.

So, before I give up, does anybody have a beginner-friendly advice on how to prove my lemma?

[Kevin Buzzard]

Do you know a maths proof?

[Kevin Buzzard]

If so, just write that proof down.

[Martin Dvořák]

Informal proof starts with a well-known property:

∀ x y : ℝ, (∀ ε : ℝ, ε > 0 → |y - f x| < ε) → f x = y

For every real number x and every ε > 0 there exists a rational numbers x₁ and x₂ such that x₁ < x < x₂ and x - x₁, x₂ - x < ε / (f 2 - f 1). From increasing we have f x₁ < f x < f x₂. From lin_on_rat we have f x₁ = f 1 + (x₁ - 1) * (f 2 - f 1) and f x₂ = f 1 + (x₂ - 1) * (f 2 - f 1). We observe f x - f x₁, f x₂ - f x < ε. Hence | (f 1 + (x - 1) * (f 2 - f 1)) - f x | < ε. The property above gives us f x = f 1 + (x - 1) * (f 2 - f 1).

[Martin Dvořák]

Now back to Lean! How can I say x₁ < x when x₁ : ℚ but x : ℝ please?

[Yakov Pechersky]

docs#rat_dense_cast should help

[Yakov Pechersky]

(x₁ : ℝ) < x is the proposition

[Yakov Pechersky]

and the lemma I shared is that the coercion is has dense range.

[Andrew Yang]

I guess docs#continuous_at_of_monotone_on_of_exists_between and docs#continuous.ext_on could help?

[Yakov Pechersky]

docs#exists_rat_btwn

[Yakov Pechersky]

I found that lemma by looking at the proof of src#rat_dense_cast

[Arthur Paulino]

offtopic: I read those like "exists rat by the way" and "rat dense cat" :rat: :cat:

[Martin Dvořák]

I have another awkward technical moment.

import data.real.basic

example (a : ℚ) (a_pos : 0 < (a : ℝ)) : 0 < a :=
begin
  sorry,
end

[Ruben Van de Velde]

assumption_mod_cast

[Martin Dvořák]

Thanks a lot! Can I somehow add this tactic to the list of tactics tried by hint please?

[Matt Diamond]

I assume you guys meant docs#rat.dense_range_cast above, right?

[Martin Dvořák]

I have finally proved the lemma!
https://github.com/madvorak/math-competition/blob/77eaa2132d82792a22ae29976a8805ff436ce802/src/functional_equation.lean#L69

[Martin Dvořák]

Is there a two-line proof of lin_on_real with a help of something powerful from mathlib?