Add Functions!Pointwise

[lemmy]

I propose to add a Pointwise operator to Functions that applies a (binary) operator T to two functions f and g that share the same domain:

Pointwise(f, g, T(_,_)) ==
    [ e \in DOMAIN f |-> T(f[e], g[e]) ]

We can compose, e.g., addition over functions out of Naturals!+ and Pointwise:

Plus(f,g) == Pointwise(f,g,+)

Obviously, Pointwise is not the greatest name. Suggestions welcome!

[muenchnerkindl]

The analogous operator is called map2 in OCaml. Not sure the name is any better, though.

[lemmy]

Damn, naming is hard! AFAICT map2 in Ocaml is zipWith in Haskell, which collides name-wise with our SequencesExt!Zip. Also, map2 and zipWith both operate on lists and not what TLA+ calls functions. Here is what ChatGPT says about Pointwise:

In mathematics, the term "pointwise" is typically used in the context of pointwise operations, especially in functions. The "pointwise" operation refers to applying an operation to corresponding elements of one or more functions at each point in their domain. This is commonly seen in pointwise addition, multiplication, or other operations involving functions.

Here are a couple of examples to illustrate pointwise operations:

1. Pointwise Addition: Suppose you have two functions, ( f(x) ) and ( g(x) ). The pointwise sum of these functions, denoted as ( (f + g)(x) ), is a new function where each element is the sum of the corresponding elements in ( f ) and ( g ). Mathematically, it's defined as ( (f + g)(x) = f(x) + g(x) ) for all ( x ) in the domain.

2. Pointwise Multiplication: Similarly, the pointwise product of ( f(x) ) and ( g(x) ), denoted as ( (f \cdot g)(x) ), is a function where each element is the product of the corresponding elements in ( f ) and ( g ). It's defined as ( (f \cdot g)(x) = f(x) \cdot g(x) ).

The concept of pointwise operations is important in many areas of mathematics, including analysis and functional analysis. It allows for the manipulation and combination of functions in a straightforward and intuitive way.

[lemmy]

Thanks @muenchnerkindl