ratfunc composition

Stream: new members

[Callum Cassidy-Nolan]

I've been working with f : R -> R and using f^[n] to represent f ( f ( f ( ... f ( x ) ) ) ), I want to do this with ratfunc R but it doesn't work since nat.iterate R doesn't seem to work on type R -> R, does anyone have any tips on how to represent this with ratfunc R ?

[Callum Cassidy-Nolan]

(deleted)

[Kevin Buzzard]

The first thing to figure out is how to compose two rational functions and get a rational function. Then you can just fold I guess.

[Callum Cassidy-Nolan]

I think I have to use ratfunc.eval #ratfunc.eval but I don't really understand it too well :

Evaluate a rational function p given a ring hom f from the scalar field to the target and a value x for the variable in the target.

Don't I just need to pass the rational function and the value I want to evaluate at ? What is the ring hom thing?

[Eric Wieser]

(docs#ratfunc.eval)

[Eric Wieser]

The implementation of docs#polynomial.comp might give some ideas

[Eric Wieser]

I would guess you pick the ring_hom as algebra_map _ _

[Kevin Buzzard]

docs#ratfunc

[Kevin Buzzard]

I don't think you can use evaluation. If the ground field is finite then not even a polynomial is determined by its values. A rational function can take infinity as a value so I don't think ring homomorphisms are relevant either. I guess you need to evaluate on the other rational function itself

[Kevin Buzzard]

Aah I see, yes this is the point, you don't eval at an element of K, you eval at an element of ratfunc.

[Callum Cassidy-Nolan]

Kevin Buzzard said:

Aah I see, yes this is the point, you don't eval at an element of K, you eval at an element of ratfunc.

Trying to understand that more, so far I've experimented with this example:

import field_theory.ratfunc

#check ratfunc.eval id 1 (ratfunc.X + 1) = 2

but it errors with :

type mismatch at application
  ratfunc.eval id
term
  id
has type
  ?m_1 → ?m_1 : Sort ?
but is expected to have type
  ?m_1 →+* ?m_2 : Type (max ? ?)

[Kevin Buzzard]

yep that error makes perfect sense. Maybe you want ring_hom.id or something?

[Callum Cassidy-Nolan]

Ok, I tried that :

import field_theory.ratfunc

#check ratfunc.eval ring_hom.id 1 (ratfunc.X + 1) = 2

but with:

type mismatch at application
  ratfunc.eval ring_hom.id
term
  ring_hom.id
has type
  Π (α : Type ?) [_inst_1 : non_assoc_semiring α], α →+* α : Type (?+1)
but is expected to have type
  ?m_1 →+* ?m_2 : Type (max ? ?)

[Callum Cassidy-Nolan]

Can you explain the point of evaluating a ratfunc with another ratfunc ? Why not evaluate it with a value in R ?

[Antoine Labelle]

I think that ratfunc.eval ratfunc.C q p should give the expected composition p ∘ q. The idea is that the ring homomorphism ratfunc.C let you see the coefficients of pas elements of ratfunc R, and this rational function with coefficients in ratfunc R can then be evaluated at q.

[Alex J. Best]

I think something like this is what you want:

import field_theory.ratfunc

noncomputable theory

variables {K : Type*} [field K] (f g : ratfunc K)
def comp : ratfunc K :=
f.eval (algebra_map K (ratfunc K)) g


variables {n : ℕ}
#check (comp f)^[n] ratfunc.X -- should be f (f (f (X))) n times

the point is to define composition of rational functions as a rational function, rather than as a plain function so we remember more information

Edit: Oops this is basically what @Antoine Labelle said :wink:

[Reid Barton]

Is comp associative?

[Antoine Labelle]

It should be, yes

[Antoine Labelle]

Actually, one problem is that, mathematically, the composition of rational functions is not quite well-defined everywhere : for example there is no good way to compose 1/X with constant rational function 0. In these cases, the definition I gave above should probably evaluate to 0 : ratfunc R, just as in lean a/0 is defined (somewhat arbitrarily) to be 0.

[Reid Barton]

I think there would be some problem with composing (in standard order) the rational functions X + 1, 1 / (X - 1), 1.

[Antoine Labelle]

You're right, it might be associative only when it's well-defined

[Alex J. Best]

Interesting! Looks to me like this only happens when one of the functions involved is constant, which would imply that this operation is still power associative, and the above iterated function is well defined despite this, do we need a new typeclass for power associative monoids :wink:?