abs with constant

Stream: Is there code for X?

[Henrik Böving]

I'm currently trying to solve a goal of the form:

c : ℝ,
f : ℝ → ℝ,
n : ℝ
⊢ abs (c * f n) ≤ c * abs (f n)

but neither the tactics i tried managed to automatically solve this, nor library_search were able to solve this for me although it seems quite trivially true to me?

[Eric Wieser]

It's false if c = -1

[Eric Wieser]

You need the hypothesis 0 ≤ c. If you add that, then library_search might be able to help you

[Henrik Böving]

Ohh right it would have to be positive c, still no luck with library search even with that hypothesis though :/

[Yaël Dillies]

abs_mul will get you closer.

[Eric Wieser]

docs#abs_mul

[Heather Macbeth]

The new lemma docs#abs_cases is designed precisely to automate this kind of thing.

import data.real.basic

variables (c : ℝ) (f : ℝ → ℝ) (n : ℝ)

example (h: 0 ≤ c) : abs (c * f n) ≤ c * abs (f n) :=
by cases abs_cases (c * f n); cases abs_cases (f n); nlinarith

[Heather Macbeth]

(new in #8124, so it won't work in the web editor yet)

[Eric Wieser]

(but it will work in gitpod!)

[Henrik Böving]

Very cool, thanks!

[Heather Macbeth]

(cc @Alex Kontorovich)