!4#4653 Trigonometric.Deriv

Stream: PR reviews

[Scott Morrison]

This is the last of the files @Patrick Massot wants ready for the MSRI summer school. It is ready for review.

[Eric Wieser]

Mind if I push a rebase to clean up the history so the diff is easier to see?

[Eric Wieser]

Ah, a merge was enough (see this diff)

[Eric Wieser]

@Mario Carneiro, it's pretty annoying how many times we seem to have to replace h.DifferentiableAt with h.differentiableAt in these PRs; is this an easy mathport fix, or a really hard one?

[Mario Carneiro]

a relatively hard one, it involves lean 3 fixes

[Eric Wieser]

Can we do a heuristic fix of "if dot notation translates to CamelCase and there is no Foo.CamelCase for any Foo, use .camelCase instead?"

[Mario Carneiro]

my understanding is that the reason for the camel case translation is because there is some Foo.CamelCase

[Patrick Massot]

Thanks a lot @Scott Morrison ! I just landed in SFO and it's great to see all this ported! I'll update MIL as soon as I'll reach my hotel.

[Patrick Massot]

I'm now settled in Berkeley and trying those brand new calculus files. Unfortunately the discussion of calculus in MIL started with showing how simp could do easy differentiation and it seems a lot less true in Lean 4.

[Patrick Massot]

Specifically, the following worked in Lean 3:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

open  Real

example (x₀ : ℝ) (h₀ : x₀ ≠ 0) : deriv (fun x : ℝ ↦ 1 / x) x₀ = -(x₀ ^ 2)⁻¹ := by simp

example (x₀ : ℝ) (h : x₀ ≠ 0) :
    deriv (fun x : ℝ ↦ exp (x ^ 2) / x ^ 5) x₀ = (2 * x₀ ^ 2 - 5) * exp (x₀ ^ 2) / x₀ ^ 6 := by
  have : x₀ ^ 5 ≠ 0 := pow_ne_zero 5 h
  field_simp
  ring

example (y : ℝ) : deriv (fun x : ℝ ↦ 2 * x + 5) y = 2 := by simp

[Patrick Massot]

The Lean 3 code was:

import analysis.special_functions.trigonometric.deriv
import tactic.field_simp

open real

example (x₀ : ℝ) (h₀ : x₀ ≠ 0) : deriv (fun x : ℝ, 1 / x) x₀ = -(x₀ ^ 2)⁻¹ := by simp

example (x₀ : ℝ) (h : x₀ ≠ 0) :
    deriv (fun x : ℝ, exp (x ^ 2) / x ^ 5) x₀ = (2 * x₀ ^ 2 - 5) * exp (x₀ ^ 2) / x₀ ^ 6 :=
begin
  have : x₀ ^ 5 ≠ 0 := pow_ne_zero 5 h,
  field_simp,
  ring
end

example (y : ℝ) : deriv (fun x : ℝ, 2 * x + 5) y = 2 := by simp

[Scott Morrison]

Presumably related: https://github.com/leanprover-community/mathlib4/pull/4669/files#diff-053757072a2ee1ebf0332832076b953a360d7977b76c6f82885b630ec0d16cadR236

[Eric Wieser]

Mario Carneiro said:

my understanding is that the reason for the camel case translation is because there is some Foo.CamelCase

I don't think that's true in this case except for Foo = _root_