LaurentSeries C with nonneg indices equal to HahnSeries C

Stream: new members

[Daniel Eriksson]

Can I show/attest that a more general type with a hypothesis is equal to a more restricted type?
I want to say that a Laurent series on C (HahnSeries Z C) with zero coefficients on negative indices is equal to Hahnseries on N, so that the following code goes through. I want do this to be able split a Laurent series into two LS and show uniform convergence on each (need $\Z$ in sum and $\N$ for uniform convergence).

import Mathlib.RingTheory.LaurentSeries
import Mathlib.RingTheory.HahnSeries.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

def negint: Set ℤ := {a|a<0}

 lemma LSposisHNN  (L : LaurentSeries ℂ)

(M : HahnSeries ℕ ℂ)

(hb1: ∀ n , M.coeff n = L.coeff n)

(he1:∀ n:negint, L.coeff (n:ℤ) = 0): L=M := by sorry

I was thinking to use Coe or an instance but don’t see how. Or I show the set of LaurentSeries C with zero coefficients on negative indices and HahnSeries C are in bijection and show if a property holds for one set it also holds for the other?

[Luigi Massacci]

Could you make this into a #mwe?

[Luigi Massacci]

In any case, equality between terms of different types is meaningless. What you can have is coercions between types, you should promote either L or M to the other type

[Kenny Lau]

@Daniel Eriksson think about how you would want to use it in practice. in maths you don't really care about the equality of two sets either, and that's not how you use the statement anyway.

At the end of your first paragraph you said:

I want do this to be able split a Laurent series into two LS and show uniform convergence on each (need $\Z$ in sum and $\N$ for uniform convergence).

and that's the actual statement you want to make

[Kenny Lau]

it would be better if you could provide an example (in maths)

[Daniel Eriksson]

So, given $$L_n:\N\to \C, r,R\in \R$$, I want to show if $\sum_{n\in \Z} L_ny^n<\infty$, then $\sum_{n=-N}^{N} L_ny^n$ converges uniformly on $r'≤|y|≤R'$ where $r<r'<R'<R$. My idea was to use that $\sum_{n\in \N} L_ny^n$ converges uniformly on $|y|≤R'$ and $\sum_{n\in \N} L_{-n}y^n$ converges uniformly on $|y|≤1/r'$.

[Daniel Eriksson]

So, I could use a Coe from HahnSeries \N \C as a LaurentSeries \C and transfer properties to the right. I am a bit confused if I should have hypotheses on indices in the second set. Something like this (doesn't compile)?

import Mathlib.RingTheory.LaurentSeries
import Mathlib.RingTheory.HahnSeries.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

instance HahnSeriesN.coetoLaurentSeries  :
Coe (HahnSeries ℕ ℂ) (LaurentSeries ℂ)

[Daniel Eriksson]

Luigi Massacci said:

Could you make this into a #mwe?

Added a line, compiles for me

[Kenny Lau]

Daniel Eriksson said:

So, given $$L_n:\N\to \C, r,R\in \R$$, I want to show if $\sum_{n\in \Z} L_ny^n<\infty$, then $\sum_{n=-N}^{N} L_ny^n$ converges uniformly on $r'≤|y|≤R'$ where $r<r'<R'<R$. My idea was to use that $\sum_{n\in \N} L_ny^n$ converges uniformly on $|y|≤R'$ and $\sum_{n\in \N} L_{-n}y^n$ converges uniformly on $|y|≤1/r'$.

So just by this mathematical statement, for a given Laurent series L, you would already want to define three other objects. This means that you would want to define three separate functions.

[Kenny Lau]

The Lean philosophy is that you always want to define total functions, i.e. functions defined on the entirety of a type, (this is why 1 / 0 = 0 in Lean)

[Kenny Lau]

and, as soon as you define a function, you want to immediately prove the lemmas that characterise the function, which mathematically corresponds to how you would actually use the function; this set of the most basic properties is called the "API"

[Kenny Lau]

for example, say you defined a squaring function sq : Nat -> Nat that sends n to n^2.

[Kenny Lau]

then the API philosophy says that you should immediately prove the lemma that characterises the function. in this case, since it's a simpler function, the property just says sq n = n * n or sq n = n ^ 2 (already there's a difference here)

[Kenny Lau]

basically, just having a correct definition is not enough, you need to actually be able to use it

[Kenny Lau]

for example, if you define "min of something", it isn't enough that just the code compiles, you want to state and prove the statements that it's actually the minimum, i.e. it's smaller than any other stuff, and it's the unique one, etc.

[Daniel Eriksson]

Kenny Lau said:

Daniel Eriksson said:

So, given $$L_n:\N\to \C, r,R\in \R$$, I want to show if $\sum_{n\in \Z} L_ny^n<\infty$, then $\sum_{n=-N}^{N} L_ny^n$ converges uniformly on $r'≤|y|≤R'$ where $r<r'<R'<R$. My idea was to use that $\sum_{n\in \N} L_ny^n$ converges uniformly on $|y|≤R'$ and $\sum_{n\in \N} L_{-n}y^n$ converges uniformly on $|y|≤1/r'$.

So just by this mathematical statement, for a given Laurent series L, you would already want to define three other objects. This means that you would want to define three separate functions.

Hm, these three functions being the LS series and series with only the positive/negative indices? I used a structure hasLaurentSeriesonAnnulus , similarly as in HasFPowerSeriesOnBall in Analysis/Analytic/Basic.

import Mathlib.RingTheory.LaurentSeries
import Mathlib.RingTheory.HahnSeries.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
open NNReal

structure HasLaurentSeriesOnAnnulus4 (f : ℂ → ℂ) (x:ℂ) (r R: ℝ≥0)
(L: LaurentSeries ℂ) : Prop where
r_pos : 0 < r
R_pos: 0 < R
rlR:r<R
hasSum :
∀ {y}, y ∈ (Metric.ball (0 : ℂ) (R))\ (Metric.closedBall (0 : ℂ) (r))
→ HasSum ( fun n : ℤ =>(L.coeff n)*y^n) ( f (x + y))