Eventual Domination

Stream: mathlib4

[Janitha Aswedige]

Where can I find facts regarding the eventual domination of functions in Mathlib? What I mean by eventual domination is: $f$ is eventually dominated by $g$ iff $\exists k, \forall n > k, f (n) < g (n)$.

[Ruben Van de Velde]

Probably something like that is written using docs#Filter.atTop in mathlib

[Aaron Liu]

Janitha said:

Where can I find facts regarding the eventual domination of functions in Mathlib? What I mean by eventual domination is: $f$ is eventually dominated by $g$ iff $\exists k, \forall n > k, f (n) < g (n)$.

That's ∀ᶠ n in Filter.atTop, f n < g n

[Aaron Liu]

We have docs#Filter.EventuallyLE and docs#Filter.EventuallyEq but not eventually lt

[Aaron Liu]

I guess it's just le and not le so

[Matteo Cipollina]

@Janitha You might find this file relevant. It's part of a formalization of the Perron-Frobenius theorem, where the core of the proof is to establish the main prerequisite for this kind of eventual domination: a strict inequality ‖μ‖ < r between eigenvalues.
https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/LinearAlgebra/Matrix/PerronFrobenius/Dominance.lean

[Janitha Aswedige]

Thank you!

[Janitha Aswedige]

Is there a theorem in Mathlib that says eventual domination is a well-ordering?

[Edward van de Meent]

it is my understanding that well-orderings are total (linear) orders, meaning eventual domination is not a well-order?

[Edward van de Meent]

since you can take functions like fun x => if Even n then 1 else 0 and fun x => if Odd n then 1 else 0, which aren't comparable?

[Edward van de Meent]

and even then, i'm pretty sure this relation is not well-founded... since the element fun x => 2 has infinitely many functions which it dominates, i.e. pick one from fun x => if x > n then 1 else 0

[Matteo Cipollina]

indeed it is a strict partial order but not well-founded as it allows for infinite descending chains

[Edward van de Meent]

yea, so by both marks it is not a well-order

[Janitha Aswedige]

Indeed. I made a mistake. Sorry. I’m working in a special set of functions on natural numbers that contains the constant function 1, and the identity function, and which is closed under addition, multiplication, and exponentiation. Eventual domination is a well-ordering on it.

[Aaron Liu]

Janitha said:

Indeed. I made a mistake. Sorry. I’m working in a special set of functions on natural numbers that contains the constant function 1, and the identity function, and which is closed under addition, multiplication, and exponentiation. Eventual domination is a well-ordering on it.

then you have to prove that yourself