Zulip Chat Archive

Stream: new members

Topic: Approximately Equal


Callum Cassidy-Nolan (Feb 23 2022 at 22:33):

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 (Feb 24 2022 at 04:28):

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

Yury G. Kudryashov (Feb 24 2022 at 04:28):

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

Callum Cassidy-Nolan (Feb 25 2022 at 23:22):

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 (Feb 25 2022 at 23:23):

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

Callum Cassidy-Nolan (Feb 25 2022 at 23:24):

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

Callum Cassidy-Nolan (Feb 25 2022 at 23:24):

up to an accuracy of d

Mario Carneiro (Feb 26 2022 at 10:33):

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 (Feb 26 2022 at 16:04):

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


Last updated: Dec 20 2023 at 11:08 UTC