Is there a way to simplify the proof of differentiable?

Stream: new members

[Yicheng Tao]

import Mathlib
open BigOperators

open Nat
example : ∀ i : ℕ , DifferentiableAt ℝ (fun y => ↑i * Real.sin (↑i * y) * ∏ j ∈ (Finset.range (n + 1)).erase i, Real.cos (↑j * y)) 0 := by
  intro i
  apply Differentiable.mul
  apply Differentiable.mul
  apply differentiable_const
  apply Differentiable.sin
  apply Differentiable.mul
  apply differentiable_const
  apply differentiable_id
  apply Differentiable.finset_prod
  intro j _
  apply Differentiable.cos
  apply Differentiable.mul
  apply differentiable_const
  apply differentiable_id

Here is a small mwe extracted from my proof. As you can see, it looks awful. I think there should be some tactic to simplify the proof. Maybe some tactic that can automatically solve these common differentiable problems.

By the way, I was using version 4.10.0. simp made little progress most of the time in this kind of problem.

[Daniel Weber]

I think that tactic is fun_prop

[Sébastien Gouëzel]

import Mathlib
open BigOperators

attribute [fun_prop] Real.differentiable_sin Differentiable.finset_prod Real.differentiable_cos

open Nat
example : ∀ i : ℕ , DifferentiableAt ℝ (fun y => ↑i * Real.sin (↑i * y) * ∏ j ∈ (Finset.range (n + 1)).erase i, Real.cos (↑j * y)) 0 := by
  fun_prop

[Sébastien Gouëzel]

As you can see, there as some missing fun_prop attributes, which is why the tactic does not work out of the box. Thanks to your report, I'm gonna PR them right away to mathlib!

[Yicheng Tao]

I was just trying the tactic and saw the following errors:

Issues:
  No theorems found for `Real.sin` in order to prove `Differentiable ℝ fun y0 => Real.sin y0`
  No theorems found for `Real.sin` in order to prove `Differentiable ℝ fun y => Real.sin (↑i * y)`

I was just about to report it.

[Yicheng Tao]

Sébastien Gouëzel said:

import Mathlib
open BigOperators

attribute [fun_prop] Real.differentiable_sin Differentiable.finset_prod Real.differentiable_cos

open Nat
example : ∀ i : ℕ , DifferentiableAt ℝ (fun y => ↑i * Real.sin (↑i * y) * ∏ j ∈ (Finset.range (n + 1)).erase i, Real.cos (↑j * y)) 0 := by
  fun_prop

Thanks! That's really helpful.

[Yicheng Tao]

By the way, DifferentiableAt theorems should also be added. @Sébastien Gouëzel
In my case, these theorems solve my problem.

attribute [fun_prop] Real.differentiable_sin Differentiable.finset_prod Real.differentiable_cos DifferentiableAt.finset_prod DifferentiableAt.cos DifferentiableAt.sin

[Sébastien Gouëzel]

Normally, the ones I have added should be enough -- the snippet I have posted works for me. But in the PR I will also add the DifferentiableAt versions, for sure.

[Yicheng Tao]

You are right for the mwe. But my whole proof needs DifferentiableAt. These two often come together in the proof. That's why I mentioned it.