Approximately Equal

Stream: new members

[Callum Cassidy-Nolan]

I've been wanting to have statements which say something is approximately equal to something else, thus far I've been using ∃ (ε : ℝ), v = x + ε when I wanted to state that, but I know it's not that good since then any two numbers are approximately equal... Is there something in mathlib that already exists for this (maybe it already includes what accuracy level the approximation is) ?

[Yury G. Kudryashov]

There are too many ways to formalize this. What exactly do you want to say?

[Yury G. Kudryashov]

E.g., you can say that the distance is less than a given number.

[Callum Cassidy-Nolan]

True - well I was reading a textbook and they were using ≈ for approximations of pi and e and there esitmations were like 3.1415 ≈ pi

[Callum Cassidy-Nolan]

So guess in that case we would be saying there is an epsilon which is less than 0.0001

[Callum Cassidy-Nolan]

Ok, so looks like ∃ (ε : ℝ), (ε < d) ∧ (v = a + ε) might be a good way to say that a is an approximation of a...

[Callum Cassidy-Nolan]

up to an accuracy of d

[Mario Carneiro]

The way it is done in mathlib is typically using variations on abs (x - 1.234) < 0.001, for example docs#real.exp_one_near_10

[Yury G. Kudryashov]

Your ∃ (ε : ℝ), (ε < d) ∧ (v = a + ε) allows v = -1000, a = 0. ∃ (ε : ℝ), (abs ε < d) ∧ (v = a + ε) is equivalent to abs (v - a) < d.