Casting natural number literals to Real

Stream: mathlib4

[Herman Chau]

This maybe a bit of a basic question, but I am working with Mathlib.RingTheory.PowerSeries and want to multiply a power series with Real coefficients. In the minimal example below, I would like 2•A to be 2 to be @OfNat.ofNat ℝ 2 instead of @OfNat.ofNat ℕ 2. I can force this by typing (2:ℝ) instead, but it is somewhat tedious. Is there a better way to ensure my natural numbers are of type ℝ when I am smul-ing them with a power series of type ℝ⟦X⟧?

Minimal example:

import Mathlib
open PowerSeries

variable (A : ℝ⟦X⟧)

-- 2 is of type ℕ
#check 2•A

-- 2 is of type ℝ
#check (2:ℝ)•A

[Notification Bot]

This topic was moved here from #lean4 > Casting natural number literals to Real by Kyle Miller.

[Vasily Ilin]

Why do you care what type 2 is in this case? Does 2•A behave differently from (2:ℝ)•A?

[Herman Chau]

Yes, for example I get confusing messages in the Lean Infoview about being unable to unify two seemingly identical terms. Consider the following example:

example : (2•A)⁻¹ * ((2:ℝ)•A) = 1 := by
  apply (PowerSeries.inv_mul_cancel ((2:ℝ)•A))

This leads to the message:

tactic 'apply' failed, failed to unify
  (2 • A)⁻¹ * 2 • A = 1
with
  (2 • A)⁻¹ * 2 • A = 1

Only by hovering on the literal "2" in the message do we see that the issue is due to the type of 2 being ℕ in one case and ℝ in the other.

[Kevin Buzzard]

I'm afraid an unadorned 2 means the natural 2. Note that you could also use C 2, which is the constant power series, and then just multiply.

[Eric Wieser]

The problem in your example arises from using a mixture of the two different 2s. Is there a reason you can't use the unadorned one everywhere?

[Kyle Miller]

Debugging tip:

import Mathlib
open PowerSeries

variable (A : ℝ⟦X⟧)

set_option pp.numericTypes true

#check 2•A
/- (2 : ℕ) • A : ℝ⟦X⟧ -/

#check (2:ℝ)•A
/- (2 : ℝ) • A : ℝ⟦X⟧ -/

[Kyle Miller]

Unfortunately this can't be done locally (@[default_instance] doesn't allow it) but here's a way to get smul to default to Real if there's an applicable instance:

@[default_instance]
abbrev instSMulRealDefault {X : Type*} [SMul ℝ X] : SMul ℝ X := inferInstance

#check 2 • A
/-
(2 : ℝ) • A : ℝ⟦X⟧
-/

[Herman Chau]

@Kyle Miller Thanks, I'm pretty happy with using that workaround!

The reason why this arose for me is that I want to prove some a result on generating functions with real coefficients so I'd like for everything to be of type ℝ⟦X⟧. Specifically, I have the lemma

lemma geometric_series (r: ℝ) : (1-r•X)⁻¹ = (rescale r (invUnitsSub 1)) := by ...

and I'd like to use it in the case of 1-2•X but I need to cast 2 to be of type ℝ.

[Kyle Miller]

So long as you're not contributing this to mathlib, it's fine. Note that it causes everything that imports the module to start having the same behavior.

[Kyle Miller]

Maybe you'd like a macro instead?

open PowerSeries
variable (A : ℝ⟦X⟧)

macro "ℝ'2" : term => `((2 : ℝ))

#check ℝ'2 • A

[Kyle Miller]

Are you using 1 - (2:ℝ)•X enough that it's a burden to write it?

[Herman Chau]

Maybe it'll help give more context if I share the entire lean file I'm working on. In the lemma A_formula I have 2 • A in many lines.
generating_function_example.lean

I'm trying to formalize some examples from the first chapter of generatingfunctionology by Herbert Wilf. Here, we start off with a sequence a_n that satisfies a_{n+1} = 2*a_n + 1 and a_0 = 0. The goal is to show that the corresponding generating function A(x) is equal to x / ((1-x) * (1-2x)). I'm fairly new to lean so I suspect there are a lot of inefficiencies in my code. I'm interested in trying to faithfully translate the lines of reasoning in the first example.

In the process of trying to formalize this example, I think I could perhaps contribute a couple lemmas regarding geometric series to mathlib. The power series for 1/(u-x) is in Mathlib.RingTheory.PowerSeries.WellKnown and is defined via its coefficients, but unless I'm mistaken, there is no theorem in mathlib that states that this power series really is the inverse of u-x.

[Ralf Stephan]

Herman Chau said:

The power series for 1/(u-x) is in Mathlib.RingTheory.PowerSeries.WellKnown and is defined via its coefficients, but unless I'm mistaken, there is no theorem in mathlib that states that this power series really is the inverse of u-x.

I think this is invUnitsSub_mul_sub.