refactor(fderiv): redefine fderivWithin and fderiv (#19694)

Prefer `0` answer whenever it's possible.
This way, `fderivWithin_const` is true without extra assumptions.

Author: urkud

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -54,21 +54,26 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 
 /-! ### Constants -/
 
+theorem iteratedFDerivWithin_succ_const (n : ℕ) (c : F) :
+    iteratedFDerivWithin 𝕜 (n + 1) (fun _ : E ↦ c) s = 0 := by
+  induction n  with
+  | zero =>
+    ext1
+    simp [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, comp_def]
+  | succ n IH =>
+    rw [iteratedFDerivWithin_succ_eq_comp_left, IH]
+    simp only [Pi.zero_def, comp_def, fderivWithin_const, map_zero]
+
 @[simp]
-theorem iteratedFDerivWithin_zero_fun (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {i : ℕ} :
-    iteratedFDerivWithin 𝕜 i (fun _ : E ↦ (0 : F)) s x = 0 := by
-  induction i generalizing x with
+theorem iteratedFDerivWithin_zero_fun {i : ℕ} :
+    iteratedFDerivWithin 𝕜 i (fun _ : E ↦ (0 : F)) s = 0 := by
+  cases i with
   | zero => ext; simp
-  | succ i IH =>
-    ext m
-    rw [iteratedFDerivWithin_succ_apply_left, fderivWithin_congr (fun _ ↦ IH) (IH hx)]
-    rw [fderivWithin_const_apply _ (hs x hx)]
-    rfl
+  | succ i => apply iteratedFDerivWithin_succ_const
 
 @[simp]
 theorem iteratedFDeriv_zero_fun {n : ℕ} : (iteratedFDeriv 𝕜 n fun _ : E ↦ (0 : F)) = 0 :=
-  funext fun x ↦ by simpa [← iteratedFDerivWithin_univ] using
-    iteratedFDerivWithin_zero_fun uniqueDiffOn_univ (mem_univ x)
+  funext fun x ↦ by simp only [← iteratedFDerivWithin_univ, iteratedFDerivWithin_zero_fun]
 
 theorem contDiff_zero_fun : ContDiff 𝕜 n fun _ : E => (0 : F) :=
   analyticOnNhd_const.contDiff
@@ -103,30 +108,19 @@ theorem contDiffWithinAt_of_subsingleton [Subsingleton F] : ContDiffWithinAt 
 theorem contDiffOn_of_subsingleton [Subsingleton F] : ContDiffOn 𝕜 n f s := by
   rw [Subsingleton.elim f fun _ => 0]; exact contDiffOn_const
 
-theorem iteratedFDerivWithin_succ_const (n : ℕ) (c : F) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
-    iteratedFDerivWithin 𝕜 (n + 1) (fun _ : E ↦ c) s x = 0 := by
-  ext m
-  rw [iteratedFDerivWithin_succ_apply_right hs hx]
-  rw [iteratedFDerivWithin_congr (fun y hy ↦ fderivWithin_const_apply c (hs y hy)) hx]
-  rw [iteratedFDerivWithin_zero_fun hs hx]
-  simp [ContinuousMultilinearMap.zero_apply (R := 𝕜)]
-
-theorem iteratedFDeriv_succ_const (n : ℕ) (c : F) :
-    (iteratedFDeriv 𝕜 (n + 1) fun _ : E ↦ c) = 0 :=
-  funext fun x ↦ by simpa [← iteratedFDerivWithin_univ] using
-    iteratedFDerivWithin_succ_const n c uniqueDiffOn_univ (mem_univ x)
-
-theorem iteratedFDerivWithin_const_of_ne {n : ℕ} (hn : n ≠ 0) (c : F)
-    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
-    iteratedFDerivWithin 𝕜 n (fun _ : E ↦ c) s x = 0 := by
+theorem iteratedFDerivWithin_const_of_ne {n : ℕ} (hn : n ≠ 0) (c : F) (s : Set E) :
+    iteratedFDerivWithin 𝕜 n (fun _ : E ↦ c) s = 0 := by
   cases n with
   | zero => contradiction
-  | succ n => exact iteratedFDerivWithin_succ_const n c hs hx
+  | succ n => exact iteratedFDerivWithin_succ_const n c
 
 theorem iteratedFDeriv_const_of_ne {n : ℕ} (hn : n ≠ 0) (c : F) :
-    (iteratedFDeriv 𝕜 n fun _ : E ↦ c) = 0 :=
-  funext fun x ↦ by simpa [← iteratedFDerivWithin_univ] using
-    iteratedFDerivWithin_const_of_ne hn c uniqueDiffOn_univ (mem_univ x)
+    (iteratedFDeriv 𝕜 n fun _ : E ↦ c) = 0 := by
+  simp only [← iteratedFDerivWithin_univ, iteratedFDerivWithin_const_of_ne hn]
+
+theorem iteratedFDeriv_succ_const (n : ℕ) (c : F) :
+    (iteratedFDeriv 𝕜 (n + 1) fun _ : E ↦ c) = 0 :=
+  iteratedFDeriv_const_of_ne (by simp) _
 
 theorem contDiffWithinAt_singleton : ContDiffWithinAt 𝕜 n f {x} x :=
   (contDiffWithinAt_const (c := f x)).congr (by simp) rfl
@@ -946,7 +940,7 @@ theorem iteratedFDerivWithin_clm_apply_const_apply
     rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]
     rw [fderivWithin_clm_apply (hs x hx) (h_deriv.continuousMultilinear_apply_const _ x hx)
       (differentiableWithinAt_const u)]
-    rw [fderivWithin_const_apply _ (hs x hx)]
+    rw [fderivWithin_const_apply]
     simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.comp_zero, zero_add]
     rw [fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv x hx)]
 

Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

@@ -296,7 +296,7 @@ theorem norm_iteratedFDerivWithin_prod_le [DecidableEq ι] [NormOneClass A'] {u
   | empty =>
     cases n with
     | zero => simp [Sym.eq_nil_of_card_zero]
-    | succ n => simp [iteratedFDerivWithin_succ_const _ _ hs hx]
+    | succ n => simp [iteratedFDerivWithin_succ_const]
   | @insert i u hi IH =>
     conv => lhs; simp only [Finset.prod_insert hi]
     simp only [Finset.mem_insert, forall_eq_or_imp] at hf

Mathlib/Analysis/Calculus/Deriv/Basic.lean

@@ -630,8 +630,9 @@ theorem deriv_const : deriv (fun _ => c) x = 0 :=
 theorem deriv_const' : (deriv fun _ : 𝕜 => c) = fun _ => 0 :=
   funext fun x => deriv_const x c
 
-theorem derivWithin_const (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin (fun _ => c) s x = 0 :=
-  (hasDerivWithinAt_const _ _ _).derivWithin hxs
+@[simp]
+theorem derivWithin_const : derivWithin (fun _ => c) s = 0 := by
+  ext; simp [derivWithin]
 
 end Const
 

Mathlib/Analysis/Calculus/Deriv/Slope.lean

@@ -92,7 +92,7 @@ theorem range_derivWithin_subset_closure_span_image
     range (derivWithin f s) ⊆ closure (Submodule.span 𝕜 (f '' t)) := by
   rintro - ⟨x, rfl⟩
   rcases eq_or_neBot (𝓝[s \ {x}] x) with H|H
-  · simpa [derivWithin, fderivWithin, H] using subset_closure (zero_mem _)
+  · simpa [derivWithin_zero_of_isolated H] using subset_closure (zero_mem _)
   by_cases H' : DifferentiableWithinAt 𝕜 f s x; swap
   · rw [derivWithin_zero_of_not_differentiableWithinAt H']
     exact subset_closure (zero_mem _)

Mathlib/Analysis/Calculus/FDeriv/Add.lean

@@ -739,31 +739,7 @@ theorem differentiableWithinAt_comp_add_right (a : E) :
 
 theorem fderivWithin_comp_add_right (a : E) :
     fderivWithin 𝕜 (fun x ↦ f (x + a)) s x = fderivWithin 𝕜 f (a +ᵥ s) (x + a) := by
-  simp only [fderivWithin, hasFDerivWithinAt_comp_add_right]
-  by_cases h : 𝓝[s \ {x}] x = ⊥
-  · have h' : 𝓝[(a +ᵥ s) \ {x + a}] (x + a) = ⊥ := by
-      let e := Homeomorph.addRight a
-      have : 𝓝[(a +ᵥ s) \ {x + a}] (x + a) = map e (𝓝[s \ {x}] x) := by
-        rw [e.isEmbedding.map_nhdsWithin_eq]
-        congr
-        ext y
-        rw [← e.preimage_symm]
-        simp [e, Homeomorph.addRight, Set.mem_vadd_set_iff_neg_vadd_mem, add_comm]
-      rw [this, h, Filter.map_bot]
-    simp [h, h']
-  · have h' : 𝓝[(a +ᵥ s) \ {x + a}] (x + a) ≠ ⊥ := by
-      intro h''
-      let e := Homeomorph.addRight (-a)
-      have : 𝓝[s \ {x}] x = map e (𝓝[(a +ᵥ s) \ {x + a}] (x + a)) := by
-        rw [e.isEmbedding.map_nhdsWithin_eq]
-        congr
-        · simp [e]
-        ext y
-        rw [← e.preimage_symm]
-        simp [e, Homeomorph.addRight, Set.mem_vadd_set_iff_neg_vadd_mem, add_comm]
-      apply h
-      rw [this, h'', Filter.map_bot]
-    simp [h, h']
+  simp only [fderivWithin, hasFDerivWithinAt_comp_add_right, DifferentiableWithinAt]
 
 theorem hasFDerivWithinAt_comp_add_left (a : E) :
     HasFDerivWithinAt (fun x ↦ f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x) := by

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -171,16 +171,18 @@ def DifferentiableAt (f : E → F) (x : E) :=
   ∃ f' : E →L[𝕜] F, HasFDerivAt f f' x
 
 /-- If `f` has a derivative at `x` within `s`, then `fderivWithin 𝕜 f s x` is such a derivative.
-Otherwise, it is set to `0`. If `x` is isolated in `s`, we take the derivative within `s` to
-be zero for convenience. -/
+Otherwise, it is set to `0`. We also set it to be zero, if zero is one of possible derivatives. -/
 irreducible_def fderivWithin (f : E → F) (s : Set E) (x : E) : E →L[𝕜] F :=
-  if 𝓝[s \ {x}] x = ⊥ then 0 else
-  if h : ∃ f', HasFDerivWithinAt f f' s x then Classical.choose h else 0
+  if HasFDerivWithinAt f (0 : E →L[𝕜] F) s x
+    then 0
+  else if h : DifferentiableWithinAt 𝕜 f s x
+    then Classical.choose h
+  else 0
 
 /-- If `f` has a derivative at `x`, then `fderiv 𝕜 f x` is such a derivative. Otherwise, it is
 set to `0`. -/
 irreducible_def fderiv (f : E → F) (x : E) : E →L[𝕜] F :=
-  if h : ∃ f', HasFDerivAt f f' x then Classical.choose h else 0
+  fderivWithin 𝕜 f univ x
 
 /-- `DifferentiableOn 𝕜 f s` means that `f` is differentiable within `s` at any point of `s`. -/
 @[fun_prop]
@@ -199,23 +201,14 @@ variable {x : E}
 variable {s t : Set E}
 variable {L L₁ L₂ : Filter E}
 
-theorem fderivWithin_zero_of_isolated (h : 𝓝[s \ {x}] x = ⊥) : fderivWithin 𝕜 f s x = 0 := by
-  rw [fderivWithin, if_pos h]
-
-theorem fderivWithin_zero_of_nmem_closure (h : x ∉ closure s) : fderivWithin 𝕜 f s x = 0 := by
-  apply fderivWithin_zero_of_isolated
-  simp only [mem_closure_iff_nhdsWithin_neBot, neBot_iff, Ne, Classical.not_not] at h
-  rw [eq_bot_iff, ← h]
-  exact nhdsWithin_mono _ diff_subset
-
 theorem fderivWithin_zero_of_not_differentiableWithinAt (h : ¬DifferentiableWithinAt 𝕜 f s x) :
     fderivWithin 𝕜 f s x = 0 := by
-  have : ¬∃ f', HasFDerivWithinAt f f' s x := h
-  simp [fderivWithin, this]
+  simp [fderivWithin, h]
 
-theorem fderiv_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : fderiv 𝕜 f x = 0 := by
-  have : ¬∃ f', HasFDerivAt f f' x := h
-  simp [fderiv, this]
+@[simp]
+theorem fderivWithin_univ : fderivWithin 𝕜 f univ = fderiv 𝕜 f := by
+  ext
+  rw [fderiv]
 
 section DerivativeUniqueness
 
@@ -375,6 +368,14 @@ theorem hasFDerivWithinAt_univ : HasFDerivWithinAt f f' univ x ↔ HasFDerivAt f
 
 alias ⟨HasFDerivWithinAt.hasFDerivAt_of_univ, _⟩ := hasFDerivWithinAt_univ
 
+theorem differentiableWithinAt_univ :
+    DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableAt 𝕜 f x := by
+  simp only [DifferentiableWithinAt, hasFDerivWithinAt_univ, DifferentiableAt]
+
+theorem fderiv_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : fderiv 𝕜 f x = 0 := by
+  rw [fderiv, fderivWithin_zero_of_not_differentiableWithinAt]
+  rwa [differentiableWithinAt_univ]
+
 theorem hasFDerivWithinAt_of_mem_nhds (h : s ∈ 𝓝 x) :
     HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x := by
   rw [HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.mpr h]
@@ -486,19 +487,23 @@ theorem hasFDerivWithinAt_of_nmem_closure (h : x ∉ closure s) : HasFDerivWithi
   .of_nhdsWithin_eq_bot <| eq_bot_mono (nhdsWithin_mono _ diff_subset) <| by
     rwa [mem_closure_iff_nhdsWithin_neBot, not_neBot] at h
 
+theorem fderivWithin_zero_of_isolated (h : 𝓝[s \ {x}] x = ⊥) : fderivWithin 𝕜 f s x = 0 := by
+  rw [fderivWithin, if_pos (.of_nhdsWithin_eq_bot h)]
+
+theorem fderivWithin_zero_of_nmem_closure (h : x ∉ closure s) : fderivWithin 𝕜 f s x = 0 := by
+  rw [fderivWithin, if_pos (hasFDerivWithinAt_of_nmem_closure h)]
+
 theorem DifferentiableWithinAt.hasFDerivWithinAt (h : DifferentiableWithinAt 𝕜 f s x) :
     HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x := by
-  by_cases H : 𝓝[s \ {x}] x = ⊥
-  · exact .of_nhdsWithin_eq_bot H
-  · unfold DifferentiableWithinAt at h
-    rw [fderivWithin, if_neg H, dif_pos h]
-    exact Classical.choose_spec h
+  simp only [fderivWithin, dif_pos h]
+  split_ifs with h₀
+  exacts [h₀, Classical.choose_spec h]
 
 theorem DifferentiableAt.hasFDerivAt (h : DifferentiableAt 𝕜 f x) :
     HasFDerivAt f (fderiv 𝕜 f x) x := by
-  dsimp only [DifferentiableAt] at h
-  rw [fderiv, dif_pos h]
-  exact Classical.choose_spec h
+  rw [fderiv, ← hasFDerivWithinAt_univ]
+  rw [← differentiableWithinAt_univ] at h
+  exact h.hasFDerivWithinAt
 
 theorem DifferentiableOn.hasFDerivAt (h : DifferentiableOn 𝕜 f s) (hs : s ∈ 𝓝 x) :
     HasFDerivAt f (fderiv 𝕜 f x) x :=
@@ -575,10 +580,6 @@ theorem differentiableWithinAt_congr_nhds {t : Set E} (hst : 𝓝[s] x = 𝓝[t]
     DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x :=
   ⟨fun h => h.congr_nhds hst, fun h => h.congr_nhds hst.symm⟩
 
-theorem differentiableWithinAt_univ :
-    DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableAt 𝕜 f x := by
-  simp only [DifferentiableWithinAt, hasFDerivWithinAt_univ, DifferentiableAt]
-
 theorem differentiableWithinAt_inter (ht : t ∈ 𝓝 x) :
     DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x := by
   simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter ht]
@@ -647,19 +648,7 @@ theorem fderivWithin_subset (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x)
   fderivWithin_of_mem_nhdsWithin (nhdsWithin_mono _ st self_mem_nhdsWithin) ht h
 
 theorem fderivWithin_inter (ht : t ∈ 𝓝 x) : fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x := by
-  have A : 𝓝[(s ∩ t) \ {x}] x = 𝓝[s \ {x}] x := by
-    have : (s ∩ t) \ {x} = (s \ {x}) ∩ t := by rw [inter_comm, inter_diff_assoc, inter_comm]
-    rw [this, ← nhdsWithin_restrict' _ ht]
-  simp [fderivWithin, A, hasFDerivWithinAt_inter ht]
-
-@[simp]
-theorem fderivWithin_univ : fderivWithin 𝕜 f univ = fderiv 𝕜 f := by
-  ext1 x
-  nontriviality E
-  have H : 𝓝[univ \ {x}] x ≠ ⊥ := by
-    rw [← compl_eq_univ_diff, ← neBot_iff]
-    exact Module.punctured_nhds_neBot 𝕜 E x
-  simp [fderivWithin, fderiv, H]
+  simp [fderivWithin, hasFDerivWithinAt_inter ht, DifferentiableWithinAt]
 
 theorem fderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x := by
   rw [← fderivWithin_univ, ← univ_inter s, fderivWithin_inter h]
@@ -803,11 +792,7 @@ theorem differentiableWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
 
 theorem fderivWithin_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
     fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x := by
-  have : s =ᶠ[𝓝[{x}ᶜ] x] t := nhdsWithin_compl_singleton_le x y h
-  have : 𝓝[s \ {x}] x = 𝓝[t \ {x}] x := by
-    simpa only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter', diff_eq,
-      inter_comm] using this
-  simp only [fderivWithin, hasFDerivWithinAt_congr_set' y h, this]
+  simp only [fderivWithin, differentiableWithinAt_congr_set' _ h, hasFDerivWithinAt_congr_set' _ h]
 
 theorem fderivWithin_congr_set (h : s =ᶠ[𝓝 x] t) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x :=
   fderivWithin_congr_set' x <| h.filter_mono inf_le_left
@@ -937,7 +922,7 @@ theorem DifferentiableWithinAt.fderivWithin_congr_mono (h : DifferentiableWithin
 
 theorem Filter.EventuallyEq.fderivWithin_eq (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
     fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := by
-  simp only [fderivWithin, hs.hasFDerivWithinAt_iff hx]
+  simp only [fderivWithin, DifferentiableWithinAt, hs.hasFDerivWithinAt_iff hx]
 
 theorem Filter.EventuallyEq.fderivWithin_eq_of_mem (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) :
     fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
@@ -1068,19 +1053,21 @@ theorem differentiableAt_const (c : F) : DifferentiableAt 𝕜 (fun _ => c) x :=
 theorem differentiableWithinAt_const (c : F) : DifferentiableWithinAt 𝕜 (fun _ => c) s x :=
   DifferentiableAt.differentiableWithinAt (differentiableAt_const _)
 
+theorem fderivWithin_const_apply (c : F) : fderivWithin 𝕜 (fun _ => c) s x = 0 := by
+  rw [fderivWithin, if_pos]
+  apply hasFDerivWithinAt_const
+
+@[simp]
+theorem fderivWithin_const (c : F) : fderivWithin 𝕜 (fun _ ↦ c) s = 0 := by
+  ext
+  rw [fderivWithin_const_apply, Pi.zero_apply]
+
 theorem fderiv_const_apply (c : F) : fderiv 𝕜 (fun _ => c) x = 0 :=
-  HasFDerivAt.fderiv (hasFDerivAt_const c x)
+  (hasFDerivAt_const c x).fderiv
 
 @[simp]
 theorem fderiv_const (c : F) : (fderiv 𝕜 fun _ : E => c) = 0 := by
-  ext m
-  rw [fderiv_const_apply]
-  rfl
-
-theorem fderivWithin_const_apply (c : F) (hxs : UniqueDiffWithinAt 𝕜 s x) :
-    fderivWithin 𝕜 (fun _ => c) s x = 0 := by
-  rw [DifferentiableAt.fderivWithin (differentiableAt_const _) hxs]
-  exact fderiv_const_apply _
+  rw [← fderivWithin_univ, fderivWithin_const]
 
 @[simp, fun_prop]
 theorem differentiable_const (c : F) : Differentiable 𝕜 fun _ : E => c := fun _ =>