Schwarzian derivative: notation?

Stream: mathlib4

[Yury G. Kudryashov]

I'm going to define

import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

noncomputable def schwarzianWithin (f : 𝕜 → 𝕜) (s : Set 𝕜) (x : 𝕜) : 𝕜 :=
  (2 * iteratedDerivWithin 3 f s x * derivWithin f s x -
    3 * iteratedDerivWithin 2 f s x ^ 2) / (2 * derivWithin f s x ^ 2)

noncomputable def schwarzian (f : 𝕜 → 𝕜) (x : 𝕜) : 𝕜 :=
  schwarzianWithin f Set.univ x

In literature, the Schwarzian derivative is usually denoted by S f. I think about introducing scoped notation 𝓢 f for schwarzian f and 𝓢[s] f s for schwarzianWithin f s x.

• Do you think it's reasonable?
• My naive approach scoped[Schwarzian] notation3 "𝓢[" s "] " f => schwarzianWithin f s makes 𝓢[s] f s parse as schwarzianWithin (f s), not schwarzianWithin f s. How do I fix it?

[Yury G. Kudryashov]

#24161 is the current draft

[Edward van de Meent]

i think you'd need to specify f:arg in your notation then?

[Edward van de Meent]

yea, i think that fixes it?

[Edward van de Meent]

the following seems to work for me:

import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

noncomputable def schwarzianWithin (f : 𝕜 → 𝕜) (s : Set 𝕜) (x : 𝕜) : 𝕜 :=
  (2 * iteratedDerivWithin 3 f s x * derivWithin f s x -
    3 * iteratedDerivWithin 2 f s x ^ 2) / (2 * derivWithin f s x ^ 2)

noncomputable def schwarzian (f : 𝕜 → 𝕜) (x : 𝕜) : 𝕜 :=
  schwarzianWithin f Set.univ x

scoped[Schwarzian] notation3:(arg+1) "𝓢[" s "] " f:arg => (schwarzianWithin f) s
scoped[Schwarzian] prefix:(arg+1) "𝓢" => schwarzian

open scoped Schwarzian
variable (f : 𝕜 → 𝕜) (s : Set 𝕜) (x : 𝕜)

#check 𝓢[s] f x
#check 𝓢 f

[Edward van de Meent]

also TIL that notation3 adds a delaborator/prettyprinter, while notation does not

[Yaël Dillies]

(this is basically the whole point of notation3)

[Edward van de Meent]

i was under the impression that the point was to allow you to use variables?

[Edward van de Meent]

that's what the docstring leads me to believe, at least...

[Edward van de Meent]

i guess this is a bit of a gripe of mine: the docstring refers to how things were in lean3, but what that means is not clear to someone who never used lean3 (like me)

[Yury G. Kudryashov]

Thanks! I should learn more about notation some day.