Piecewise-Linear Functions

Stream: new members

[Junjie Bai]

(deleted)

[Junjie Bai]

I notice that the piecewise-linear function has not been defined in Mathlib yet(or please tell me if I just ignore it), and I have to use some properties of it to do some proofs, I found this but it's not enough.
I'm dealing with a function which is singular at every positive integer, and I want to proof it is monotone , bijective, and equal to the other forms(in math I will proof it by deriv on them), and I think I want to realize the following：

1. definition of piecewise-linear function(not only on R)
2. how to show they are continuous or not?
3. how to show they are surjective or not?
4. how to compare them with the other piecewise-linear function?
   Does anyone have any ideas of how to realize all of this? please offer some advises, thanks a lot.

[Matt Diamond]

What's wrong with using if ... then ... else statements, like in the example you linked to?

[Junjie Bai]

I have to dealing with the condition that the function have infinite singular points, so I can't use if ...then ...else statements.

[Matt Diamond]

Could you share a mathematical definition of the function?

[Junjie Bai]

Sure, it's $\int_0^u dt/[G_0：G_t]$ , where $G_i$ is the lower numbering ramification group.

[Matt Diamond]

Thanks... unfortunately I can't help with this, but I'm sure there are others here who can point you in the right direction

[Matt Diamond]

this recent thread might be relevant: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Formalizing.20Ramification.20Groups

[Junjie Bai]

Thank you!

[Kevin Buzzard]

Are you sure you need an API for this? What is a concrete example of a theorem you need to prove about this function? Don't you just need to bound the integrand below by 1/#G_0 and show it's continuous to prove surjectivity, for example?

[Junjie Bai]

I think this can solve my problem, thanks a lot!

[Junjie Bai]

Kevin Buzzard said:

Are you sure you need an API for this? What is a concrete example of a theorem you need to prove about this function? Don't you just need to bound the integrand below by 1/#G_0 and show it's continuous to prove surjectivity, for example?

I solve most of my problems, but I can't solve the surjectivity since I'm not familar with the functions about continuous and integration, can you be more specific please? Such as where can I found the functions I need to use, or which one should I use? Thanks a lot!

[Kevin Buzzard]

I don't know this myself. I'm hoping that the integral will be continuous (you're integrating a step function constant on (n,n+1) for all n) and strictly increasing (because the integrand is always at least 1/#G0>0) and its value at 0 will be 0 and the integrand is always at least 1/#G0 so the integral will be at least u/#G0 so will tend to infinity and now surely the analysts will take over and show you how to prove it's a bijection from [0,infty) to itself :-)

[Junjie Bai]

Thanks! I'll try again.

[Kevin Buzzard]

If you can't do the basic analysis goals yourself, maybe make some MWE which doesn't mention ramification groups and ask the analysts how to do it :-) (e.g. just have some arbitrary f : Nat -> Real with the hypothesis that a <= b implies f(a) >= f(b) and that there exists some c > 0 such that f(n)>=c for all n, and then integrate x mapsto f(floor x) etc etc) (I should say that I don't have a clue how to prove or even state most of the things in my previous post, I've not used integration at all in mathlib)

[Junjie Bai]

That's useful, I'll try to make some MWE first.
I've not used integration either, I'm learning it.