rational functions

Stream: new members

[Callum Cassidy-Nolan]

Hi, I was wondering if we have the definition for rational function in mathlib.

For my purposes I have been using:

  ∃ (P Q : polynomial ℝ), f = (λ x, P.eval x / Q.eval x) ∧ Q.degree ≠ 0

[Yaël Dillies]

docs#ratfunc

[Callum Cassidy-Nolan]

Since f : R to R then if I try to say ∃ (r : ratfunc ℝ), f = r it doesn't work out since r has type ratfunc R. What's a good way of stating that they are in fact equal?

[Yaël Dillies]

You want docs#ratfunc.eval

[Callum Cassidy-Nolan]

theorem dumbtest
  (f : ℕ → (ℝ → ℝ)) :
  ∃ (r : ratfunc ℝ), r.eval = f 28 := sorry

But lean says:

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

[Yaël Dillies]

Yeah, you need λ x, f.eval (ring_hom.refl _) x

[Kyle Miller]

Caveat: when you evaluate a rational function at a pole, it's going to be junk data (0 I believe), and this will be saying f has the exact same behavior at these points.

[Callum Cassidy-Nolan]

I tried modifying dumbtest to use that but It didn't work for me, can you give a MWE version of dumbtest?

[Kevin Buzzard]

can you make a MWE of the question first (ie post code with the right imports etc?)

[Callum Cassidy-Nolan]

Yes:

import data.real.basic
import field_theory.ratfunc

theorem dumbtest
  (f : ℕ → (ℝ → ℝ)) :
  ∃ (r : ratfunc ℝ), r.eval = f 28 := sorry

[Kevin Buzzard]

import data.real.basic
import field_theory.ratfunc

theorem dumbtest
  (f : ℕ → (ℝ → ℝ)) :
  ∃ (r : ratfunc ℝ), ∀ x, r.eval (ring_hom.id _) x = f 28 x := sorry