deriv neg lemmas

Stream: mathlib4

[Eric Wieser]

The names of docs#deriv_neg vs docs#deriv_neg' vs docs#deriv_neg'' vs docs#deriv.neg vs docs#deriv.neg' seem pretty subobtimal, especially given that the prime means something different to what it means for docs#fderiv_neg and docs#fderiv_neg', where again the prime means something different to what it means for docs#fderiv_mul vs docs#fderiv_mul'. What names do we want here?

[Eric Wieser]

(context: in #24351 I want to add some lemmas about deriv_pow, but want to claim the ' to mean "noncommutative" to match mul')

[Eric Wieser]

To save you some clicks, the neg lemmas are:

deriv_neg               (x : 𝕜) : deriv Neg.neg x = -1
deriv_neg'                      : deriv Neg.neg = fun x => -1
deriv_neg''             (x : 𝕜) : deriv (fun x => -x) x = -1
deriv.neg   {f : 𝕜 → F} {x : 𝕜} : deriv (fun y => -f y) x = -deriv f x
deriv.neg'  {f : 𝕜 → F}         : deriv (fun y => -f y) = fun x => -deriv f x
fderiv_neg  {f : E → F} {x : E} : fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f x
fderiv_neg' {f : E → F} {x : E} : fderiv 𝕜 (-f) x = -fderiv 𝕜 f x

[Ruben Van de Velde]

Did we not just have a discussion about naming foo f vs foo (fun x => f x)?

[Eric Wieser]

Yes, but that doesn't help with naming foo (fun x => -x) vs foo (fun x => - f x)

[Yury G. Kudryashov]

Related question from the other topic: #mathlib4 > Delete or rename AEMeasurable.fst and AEMeasurable.snd @ 💬

[Yury G. Kudryashov]

Yury G. Kudryashov said:

How should we name lemmas like docs#MeasureTheory.integral_prod_swap docs#MeasureTheory.integral_fun_fst docs#MeasureTheory.integral_fn_integral_add ?

[Eric Wieser]

Eric Wieser said:

(context: in #24351 I want to add some lemmas about deriv_pow, but want to claim the ' to mean "noncommutative" to match mul')

Should we rename mul' to mul_noncomm or mul_nc?

[Tomas Skrivan]

Eric Wieser said:

Yes, but that doesn't help with naming foo (fun x => -x) vs foo (fun x => - f x)

I think deriv.neg should be deriv_neg_comp because applying deriv_neg_comp hf should be the same as applying deriv_comp deriv_neg hf.

(Could be also deriv_comp_neg but I'm thinking of comp as "infix")

(Ah this is the same as @Yaël Dillies suggested in the other thread)

[Tomas Skrivan]

Not sure what rule should we have for deriv_neg vs deriv_neg'. Ideally such a convention would make it clear for fderiv as well where you can potentially apply x and dx.