Working with the inverse of diff func defined on a set

Stream: new members

[Michael Novak]

I'm working with a function ψ : ℝ → ℝ which I only really care about its values on subset I : Set ℝ. In the textbook I'm working from the function is simply defined as ψ : I → ℝ, but because I also want to work with derivatives, I was advised to define it on the entire real line, and just have meaningful values on I. Now I also want to work with it's inverse. I proved that ψ is bijective from I to ψ '' I, and I would like to use this to get that it's inverse is also bijective from ψ '' I to ψ, but the problem is that since ψ is defined on the entire real line it could be that some real numbers besides the members of I are sent by ψ to ψ '' I. How would you deal with this?

[Michael Rothgang]

You can do things "by hand" and use docs#Set.BijOn

[Michael Rothgang]

Another option is to define a docs#PartialEquiv --- which has the inverse on a set already built in.

[Michael Novak]

Michael Rothgang said:

You can do things "by hand" and use docs#Set.BijOn

I don't think it's possible because of the issue I mentioned, but maybe I'm missing something.

[Michael Novak]

Michael Rothgang said:

Another option is to define a docs#PartialEquiv --- which has the inverse on a set already built in.

Do you think that's the preferred / conventional way to do it in Mathlib for example?

[Michael Rothgang]

Michael Novak said:

Michael Rothgang said:

You can do things "by hand" and use docs#Set.BijOn

I don't think it's possible because of the issue I mentioned, but maybe I'm missing something.

It depends on how your inverse function is defined. You want the inverse function to pick not any preimage on \Psi '' I, but some preimage in I. Once you have this, things should be fine.

[Michael Rothgang]

That said, using a PartialEquiv will probably allow you to re-use work done in mathlib: my instinct is to try that.

[Michael Rothgang]

Another question for you: will you want to prove smoothness of the inverse function? (Then you need the inverse function theorem, and I would look at what that theorem hands you.)

[Michael Novak]

Do you think that's a good way to define it (using invFunOn)?

import Mathlib

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E)

/-- Auxiliary definition, this is the reversed (inverse) parameter transformation
for the arclength reparametrization. -/
def arclengthParamTransformAux (t₀ : ℝ): ℝ → ℝ := fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖

variable (I : Set ℝ) [I.OrdConnected]

--This is parameter transformation used to construct the arc-length reparametrization.
def arclengthParamTransform (t₀ : ℝ) :=
  letI ψ := arclengthParamTransformAux c t₀
  ψ.invFunOn I

--Unit speed / arclength reparametrization of a parametrized curve
def arclengthReparamFrom (t₀ : ℝ) : ℝ → E :=
  letI φ := arclengthParamTransform c I t₀
  c ∘ φ

[Michael Novak]

Because I think this will give me the properties I want from this function

[Michael Novak]

I managed to get BijOn with this definition.