Hi,

I am trying to work with `Landau_Symbols`

to argue about functions that take more than a single argument.

When doing something like

```
fun f1 :: "nat => nat" where
"f1 x = 2 * x"
lemma "f1 ∈ O(λx. x)"
(* some proof here *)
```

everything works as expected.

However, when I try:

```
fun f2 :: "nat => nat => nat" where
"f2 x y = 2 * (x + y)"
(* will not work *)
lemma "f2 ∈ O(λx y. x + y)"
```

I cannot proceed because `No type arity fun :: real_normed_field`

. I've tired uncurrying and similar workarounds but I was not

successful. After looking into the source, I am starting to fear that what I'm trying to do is not possible... :(

Thus my question: Is it possible to use `Landau_Symbols`

to argue about functions taking multiple arguments and if so, how? :sweat_smile:

I don't think Landau with arity > 1 will work with the current Isabelle setup. Nevertheless, what would be the definition of Big-O on a multivariate function?

The definition itself is not a problem, see for example: https://en.wikipedia.org/wiki/Big_O_notation#Multiple_variables

The only option I can see right now is actually uncurrying the functions and defining some ordering (`order`

) on the tuples that makes sense. I'm not sure about that atm. I'll update the topic as I get more results :)

I have a solution using tuples, (courtesy of @Manuel Eberl , thanks again) using the Product-Filter `×⇩F`

:

```
lemma "(λ(x, y). f2 x y) ∈ O[at_top ×⇩F at_top](λ(x, y). x + y)"
```

Last updated: Sep 11 2024 at 16:22 UTC