Elementary `HasDerivAt` results

Stream: mathlib4

[Paul Lezeau]

Would the following two results be worth adding to Mathlib?

theorem hasDerivAtFilter_zero {𝕜 : Type u}
    [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F]
    [NormedSpace 𝕜 F] (x : 𝕜) (L : Filter 𝕜) :
    HasDerivAtFilter (0 : 𝕜 → F) 0 x L where
  isLittleOTVS := by
    simp [Asymptotics.isLittleOTVS_iff_isLittleO]

theorem hasDerivAt_zero {𝕜 : Type u}
    [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F]
    [NormedSpace 𝕜 F] (x : 𝕜) :
    HasDerivAt (0 : 𝕜 → F) 0 x := by
  apply hasDerivAtFilter_zero

These have come up relatively naturally in what I'm doing, but I'm not sure how useful they would be given that there are already very similar results, e.g. docs#hasDerivWithinAt_const

[Eric Wieser]

I think this comes down to the same thing as whether to write Continuous (f * g) or Continuous (fun x => f x * g x), and what to name them if we have both

[Eric Wieser]

Indeed, if we decide we only want the one with fun, then there is no need for your lemma as it's a syntactic specialization of the const one you mention

[Paul Lezeau]

Both conventions seem to be used here, since there is also docs#derivWithin_zero

[Eric Wieser]

I guess following every _const result with _zero, _one, and _ofNat would be reasonable then

[Paul Lezeau]

#23310

[Eric Wieser]

Turns out this adds a lot of lemmas. Would we prefer to just write them all manually as

theorem hasDerivAtFilter_zero : HasDerivAtFilter (0 : 𝕜 → F) 0 x L :=
  hasDerivAtFilter_const _ _ _

theorem hasDerivAtFilter_one [One F] : HasDerivAtFilter (1 : 𝕜 → F) 0 x L :=
  hasDerivAtFilter_const _ _ _

theorem hasDerivAtFilter_natCast [NatCast F] (n : ℕ) : HasDerivAtFilter (n : 𝕜 → F) 0 x L :=
  hasDerivAtFilter_const _ _ _

theorem hasDerivAtFilter_intCast [IntCast F] (z : ℤ) : HasDerivAtFilter (z : 𝕜 → F) 0 x L :=
  hasDerivAtFilter_const _ _ _

theorem hasDerivAtFilter_ofNat (n : ℕ) [OfNat F n] : HasDerivAtFilter (ofNat(n) : 𝕜 → F) 0 x L :=
  hasDerivAtFilter_const _ _ _

or have something more mechanical like

run_cmd do
  for (name, args, val) in [
    (`hasDerivAtFilter_zero,
      #[], ← `(0)),
    (`hasDerivAtFilter_one,
      #[← `(bracketedBinderF| [One F])], ← `(1)),
    (`hasDerivAtFilter_natCast,
      #[← `(bracketedBinderF| [NatCast F]), ← `(bracketedBinderF| (n : ℕ))], ← `(n)),
    (`hasDerivAtFilter_intCast,
      #[← `(bracketedBinderF| [IntCast F]), ← `(bracketedBinderF| (z : ℤ))], ← `(z)),
    (`hasDerivAtFilter_ofNat,
      #[← `(bracketedBinderF| (n : ℕ)), ← `(bracketedBinderF| [OfNat F n])], ← `(ofNat(n)))
  ] do
    Lean.Elab.Command.elabCommandTopLevel <|
      ← `(command|
      theorem $(Lean.mkIdent name) $args* :
        HasDerivAtFilter ($(val) : 𝕜 → F) 0 x L :=
          hasDerivAtFilter_const _ _ _)

[Ruben Van de Velde]

If the mechanical code is longer than the copy/pasted code... :)

[Yury G. Kudryashov]

I think that we should have a tactic that specializes "const" results to

• OfNat.ofNat;
• zero and one
• Nat.cast;
• Int.cast.

[Yury G. Kudryashov]

This appears in many contexts, not only HasDerivAt.

[Paul Lezeau]

I can have a go at writing that:)

[Eric Wieser]

Not a tactic, but an attribute / command, right?

[Yury G. Kudryashov]

Yes, I meant "meta program".

[Eric Wieser]

Is the proposal that we write this before merging #23310, or that we attempt it as a follow up?

[Paul Lezeau]

I was thinking of doing this as a follow up

[Yury G. Kudryashov]

Another related proposal is to have an attribute and/or command that turns a Nat.cast lemma into zero, one, and ofNat lemmas.

[Eric Wieser]

I think that for zero and one that probably ends up discarding generality

[Eric Wieser]

For ofNat we could certainly make lots use of that, but I wouldn't work for the PR mentioned above.