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
lemma "(λ(x, y). f2 x y) ∈ O[at_top ×⇩F at_top](λ(x, y). x + y)"
Last updated: Dec 07 2023 at 20:16 UTC