How to prove the equality of two functions?

Questions
1

There are two functions

f[x_] := Which[0 <= Mod[x, 2 \[Pi]] < \[Pi], Mod[x, \[Pi]], \[Pi] <= Mod[x, 2 \[Pi]] < 2 \[Pi], -Mod[x, \[Pi]] + \[Pi]]

and

g[x_] := \[Pi] (1 - (-1)^Quotient[x, \[Pi]])/2 + (-1)^Quotient[x, \[Pi]] Mod[x, \[Pi]]

They are equal, as can be seen from their graphs.
But how can this be proved with Wolfram tools?
In other words, how can Wolfram get g from f and vice versa?

Isn’t it a challenge to the Wolfram expert to compare two fundamentally different definitions of the same mathematical entity and prove in a given system their equivalence?

As you can see from the name of the attached file, there is a third equivalent function: arccocos[x_]:=ArcCos[Cos[x]]. So the task becomes more complicated. We need to justify the equality of the three functions in Wolfram.

ArcCosCos.nb (65.2 KB)

2

Table[{q, f[q]==g[q]},{q, -7 Pi, 7 Pi, 2 Pi}]

returns

{{-7 Pi,False},{-5 Pi,False},{-3 Pi,False},{-Pi,False},{Pi,False},{3 Pi,False},{5 Pi,False},{7 Pi,False}
3

You’re right! Thank you. But my question is still valid about the function f in the form of

f[x_] := Which[0 <= Mod[x, 2 \[Pi]] < \[Pi], Mod[x, \[Pi]], \[Pi] <= Mod[x, 2 \[Pi]] < 2 \[Pi], -Mod[x, \[Pi]] +  \Pi]]
4

First, let me corrected the syntax error of enclosing Pi in square brackets:

f[x_] := Which[
  0 <= Mod[x, 2 Pi] < Pi, Mod[x, Pi], 
  Pi <= Mod[x, 2 Pi] < 2 Pi, Mod[-x, Pi]
]
g[x_] := Pi (1 - (-1)^Quotient[x, Pi])/2 + (-1)^Quotient[x, Pi] Mod[x, Pi]

Then, checking equality of f[x] and g[x] over a range of values for x:

Table[f[x], {x, -10, 10, 1/10}] == Table[g[x], {x, -10, 10, 1/10}]
(* True *)
5

You’re right! Thank you. But my question is still valid about the function f in the form of

f[x_] := Which[0 <= Mod[x, 2 \[Pi]] < \[Pi], Mod[x, \[Pi]], \[Pi] <= Mod[x, 2 \[Pi]] < 2 \[Pi], -Mod[x, \[Pi]] +  \Pi]]
6

It is not a question of making sure that the functions are equal: this is already evident from the graph. I am interested in how Wolfram can get g from f and vice versa.

7

I think Bill’s point is that if f[Pi] == g[Pi] is False, then f[x] and g[x} are not equivalent. Therefore one cannot to get from f[x] to g[x] or vice versa. Typically, Plot fails to show differences between function when they occur only at isolated points. It does discrete sampling and does not check all possible points (obviously, since there would be infinitely many values to check).

8

As they say in my language: It was a long time ago and not true. I have long since corrected it. Check the attached file ArcCosCos, please. Copying to text causes errors.

And I remember your trick with ArcTan[1/x] + ArcTan[x]. Bravo! I’ve never seen that before anywhere. If there is any literature on this subject, please tell me.

9

You can use PiecewiseExpand:

h[x_] := Which[0 <= Mod[x, 2 Pi] < Pi, Mod[x, Pi],
   Pi <= Mod[x, 2 Pi] < 2 Pi, Mod[-x, Pi]];
g[x_] := 
  Pi (1 - (-1)^Quotient[x, Pi])/2 + (-1)^Quotient[x, Pi] Mod[x, Pi];
PiecewiseExpand[h[x] - g[x], 0 <= x < 4 Pi]
10

IMHO A function in Wolfram is nothing more than its definition. Therefore, proving the equality of two functions is nothing more than establishing the equivalence of their definitions.

11

You keep on modifiying the original post. Makes it hard to keep up a coherent discussion. However, your new version of f[x] is equal to g[x], if one applies Gianluca’s suggestion of using PiecewiseExpand:

f[x_] := Which[
  0 <= Mod[x, 2 Pi] < Pi, Mod[x, Pi], 
  Pi <= Mod[x, 2 Pi] < 2 Pi,-Mod[x,Pi]+Pi
]
g[x_] := Pi (1 - (-1)^Quotient[x, Pi])/2 + (-1)^Quotient[x, Pi] Mod[x, Pi]

PiecewiseExpand[f[x] - g[x], 0 <= x < 4 Pi]
(* 0 *)

That should answer your question:

But how can this be proved with Wolfram tools?

12

Please take the definitions from the attached ArcCosCos file. Errors occur when copying into a text window.