Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(analysis/calculus/deriv): add iff versions of differentiable_const_add etc #5390

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore(analysis/calculus/deriv): add iff versions of differentiable_const_add etc #5390

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
332220a
chore(analysis/calculus/deriv): add `iff` versions of `differentiable…
urkud Dec 16, 2020
71cc212
Fix lint
urkud Dec 16, 2020
a84bc55
Add `_iff`s, fix a typo
urkud Dec 16, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
51 changes: 19 additions & 32 deletions src/analysis/calculus/deriv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -574,14 +574,12 @@ theorem has_deriv_at.add_const
has_deriv_at (λ x, f x + c) f' x :=
hf.add_const c

lemma deriv_within_add_const (hxs : unique_diff_within_at 𝕜 s x)
(hf : differentiable_within_at 𝕜 f s x) (c : F) :
lemma deriv_within_add_const (hxs : unique_diff_within_at 𝕜 s x) (c : F) :
deriv_within (λy, f y + c) s x = deriv_within f s x :=
(hf.has_deriv_within_at.add_const c).deriv_within hxs
by simp only [deriv_within, fderiv_within_add_const hxs]

lemma deriv_add_const (hf : differentiable_at 𝕜 f x) (c : F) :
deriv (λy, f y + c) x = deriv f x :=
(hf.has_deriv_at.add_const c).deriv
lemma deriv_add_const (c : F) : deriv (λy, f y + c) x = deriv f x :=
by simp only [deriv, fderiv_add_const]

theorem has_deriv_at_filter.const_add (c : F) (hf : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (λ y, c + f y) f' x L :=
Expand All @@ -595,18 +593,15 @@ theorem has_deriv_at.const_add (c : F) (hf : has_deriv_at f f' x) :
has_deriv_at (λ x, c + f x) f' x :=
hf.const_add c

lemma deriv_within_const_add (hxs : unique_diff_within_at 𝕜 s x)
(c : F) (hf : differentiable_within_at 𝕜 f s x) :
lemma deriv_within_const_add (hxs : unique_diff_within_at 𝕜 s x) (c : F) :
deriv_within (λy, c + f y) s x = deriv_within f s x :=
(hf.has_deriv_within_at.const_add c).deriv_within hxs
by simp only [deriv_within, fderiv_within_const_add hxs]

lemma deriv_const_add (c : F) (hf : differentiable_at 𝕜 f x) :
deriv (λy, c + f y) x = deriv f x :=
(hf.has_deriv_at.const_add c).deriv
lemma deriv_const_add (c : F) : deriv (λy, c + f y) x = deriv f x :=
by simp only [deriv, fderiv_const_add]

end add


section sum
/-! ### Derivative of a finite sum of functions -/

Expand Down Expand Up @@ -741,16 +736,12 @@ theorem has_strict_deriv_at.neg (h : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ x, -f x) (-f') x :=
by simpa using h.neg.has_strict_deriv_at

lemma deriv_within.neg (hxs : unique_diff_within_at 𝕜 s x)
(h : differentiable_within_at 𝕜 f s x) :
lemma deriv_within.neg (hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λy, -f y) s x = - deriv_within f s x :=
h.has_deriv_within_at.neg.deriv_within hxs
by simp only [deriv_within, fderiv_within_neg hxs, continuous_linear_map.neg_apply]

lemma deriv.neg : deriv (λy, -f y) x = - deriv f x :=
if h : differentiable_at 𝕜 f x then h.has_deriv_at.neg.deriv else
have ¬differentiable_at 𝕜 (λ y, -f y) x, from λ h', by simpa only [neg_neg] using h'.neg,
by simp only [deriv_zero_of_not_differentiable_at h,
deriv_zero_of_not_differentiable_at this, neg_zero]
by simp only [deriv, fderiv_neg, continuous_linear_map.neg_apply]

@[simp] lemma deriv.neg' : deriv (λy, -f y) = (λ x, - deriv f x) :=
funext $ λ x, deriv.neg
Expand Down Expand Up @@ -849,14 +840,12 @@ theorem has_deriv_at.sub_const
has_deriv_at (λ x, f x - c) f' x :=
hf.sub_const c

lemma deriv_within_sub_const (hxs : unique_diff_within_at 𝕜 s x)
(hf : differentiable_within_at 𝕜 f s x) (c : F) :
lemma deriv_within_sub_const (hxs : unique_diff_within_at 𝕜 s x) (c : F) :
deriv_within (λy, f y - c) s x = deriv_within f s x :=
(hf.has_deriv_within_at.sub_const c).deriv_within hxs
by simp only [deriv_within, fderiv_within_sub_const hxs]

lemma deriv_sub_const (c : F) (hf : differentiable_at 𝕜 f x) :
deriv (λ y, f y - c) x = deriv f x :=
(hf.has_deriv_at.sub_const c).deriv
lemma deriv_sub_const (c : F) : deriv (λ y, f y - c) x = deriv f x :=
by simp only [deriv, fderiv_sub_const]

theorem has_deriv_at_filter.const_sub (c : F) (hf : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (λ x, c - f x) (-f') x L :=
Expand All @@ -870,14 +859,12 @@ theorem has_deriv_at.const_sub (c : F) (hf : has_deriv_at f f' x) :
has_deriv_at (λ x, c - f x) (-f') x :=
hf.const_sub c

lemma deriv_within_const_sub (hxs : unique_diff_within_at 𝕜 s x)
(c : F) (hf : differentiable_within_at 𝕜 f s x) :
lemma deriv_within_const_sub (hxs : unique_diff_within_at 𝕜 s x) (c : F) :
deriv_within (λy, c - f y) s x = -deriv_within f s x :=
(hf.has_deriv_within_at.const_sub c).deriv_within hxs
by simp [deriv_within, fderiv_within_const_sub hxs]

lemma deriv_const_sub (c : F) (hf : differentiable_at 𝕜 f x) :
deriv (λ y, c - f y) x = -deriv f x :=
(hf.has_deriv_at.const_sub c).deriv
lemma deriv_const_sub (c : F) : deriv (λ y, c - f y) x = -deriv f x :=
by simp only [← deriv_within_univ, deriv_within_const_sub unique_diff_within_at_univ]

end sub

Expand Down
168 changes: 115 additions & 53 deletions src/analysis/calculus/fderiv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1486,8 +1486,7 @@ theorem has_fderiv_within_at.add_const
has_fderiv_within_at (λ y, f y + c) f' s x :=
hf.add_const c

theorem has_fderiv_at.add_const
(hf : has_fderiv_at f f' x) (c : F):
theorem has_fderiv_at.add_const (hf : has_fderiv_at f f' x) (c : F):
has_fderiv_at (λ x, f x + c) f' x :=
hf.add_const c

Expand All @@ -1496,30 +1495,46 @@ lemma differentiable_within_at.add_const
differentiable_within_at 𝕜 (λ y, f y + c) s x :=
(hf.has_fderiv_within_at.add_const c).differentiable_within_at

@[simp] lemma differentiable_within_at_add_const_iff (c : F) :
differentiable_within_at 𝕜 (λ y, f y + c) s x ↔ differentiable_within_at 𝕜 f s x :=
⟨λ h, by simpa using h.add_const (-c), λ h, h.add_const c⟩

lemma differentiable_at.add_const
(hf : differentiable_at 𝕜 f x) (c : F) :
differentiable_at 𝕜 (λ y, f y + c) x :=
(hf.has_fderiv_at.add_const c).differentiable_at

@[simp] lemma differentiable_at_add_const_iff (c : F) :
differentiable_at 𝕜 (λ y, f y + c) x ↔ differentiable_at 𝕜 f x :=
⟨λ h, by simpa using h.add_const (-c), λ h, h.add_const c⟩

lemma differentiable_on.add_const
(hf : differentiable_on 𝕜 f s) (c : F) :
differentiable_on 𝕜 (λy, f y + c) s :=
λx hx, (hf x hx).add_const c

@[simp] lemma differentiable_on_add_const_iff (c : F) :
differentiable_on 𝕜 (λ y, f y + c) s ↔ differentiable_on 𝕜 f s :=
⟨λ h, by simpa using h.add_const (-c), λ h, h.add_const c⟩

lemma differentiable.add_const
(hf : differentiable 𝕜 f) (c : F) :
differentiable 𝕜 (λy, f y + c) :=
λx, (hf x).add_const c

lemma fderiv_within_add_const (hxs : unique_diff_within_at 𝕜 s x)
(hf : differentiable_within_at 𝕜 f s x) (c : F) :
@[simp] lemma differentiable_add_const_iff (c : F) :
differentiable 𝕜 (λ y, f y + c) ↔ differentiable 𝕜 f :=
⟨λ h, by simpa using h.add_const (-c), λ h, h.add_const c⟩

lemma fderiv_within_add_const (hxs : unique_diff_within_at 𝕜 s x) (c : F) :
fderiv_within 𝕜 (λy, f y + c) s x = fderiv_within 𝕜 f s x :=
(hf.has_fderiv_within_at.add_const c).fderiv_within hxs
if hf : differentiable_within_at 𝕜 f s x
then (hf.has_fderiv_within_at.add_const c).fderiv_within hxs
else by { rw [fderiv_within_zero_of_not_differentiable_within_at hf,
fderiv_within_zero_of_not_differentiable_within_at], simpa }

lemma fderiv_add_const
(hf : differentiable_at 𝕜 f x) (c : F) :
fderiv 𝕜 (λy, f y + c) x = fderiv 𝕜 f x :=
(hf.has_fderiv_at.add_const c).fderiv
lemma fderiv_add_const (c : F) : fderiv 𝕜 (λy, f y + c) x = fderiv 𝕜 f x :=
by simp only [← fderiv_within_univ, fderiv_within_add_const unique_diff_within_at_univ]

theorem has_strict_fderiv_at.const_add (hf : has_strict_fderiv_at f f' x) (c : F) :
has_strict_fderiv_at (λ y, c + f y) f' x :=
Expand All @@ -1545,34 +1560,44 @@ lemma differentiable_within_at.const_add
differentiable_within_at 𝕜 (λ y, c + f y) s x :=
(hf.has_fderiv_within_at.const_add c).differentiable_within_at

@[simp] lemma differentiable_within_at_const_add_iff (c : F) :
differentiable_within_at 𝕜 (λ y, c + f y) s x ↔ differentiable_within_at 𝕜 f s x :=
⟨λ h, by simpa using h.const_add (-c), λ h, h.const_add c⟩

lemma differentiable_at.const_add
(hf : differentiable_at 𝕜 f x) (c : F) :
differentiable_at 𝕜 (λ y, c + f y) x :=
(hf.has_fderiv_at.const_add c).differentiable_at

lemma differentiable_on.const_add
(hf : differentiable_on 𝕜 f s) (c : F) :
@[simp] lemma differentiable_at_const_add_iff (c : F) :
differentiable_at 𝕜 (λ y, c + f y) x ↔ differentiable_at 𝕜 f x :=
⟨λ h, by simpa using h.const_add (-c), λ h, h.const_add c⟩

lemma differentiable_on.const_add (hf : differentiable_on 𝕜 f s) (c : F) :
differentiable_on 𝕜 (λy, c + f y) s :=
λx hx, (hf x hx).const_add c

lemma differentiable.const_add
(hf : differentiable 𝕜 f) (c : F) :
@[simp] lemma differentiable_on_const_add_iff (c : F) :
differentiable_on 𝕜 (λ y, c + f y) s ↔ differentiable_on 𝕜 f s :=
⟨λ h, by simpa using h.const_add (-c), λ h, h.const_add c⟩

lemma differentiable.const_add (hf : differentiable 𝕜 f) (c : F) :
differentiable 𝕜 (λy, c + f y) :=
λx, (hf x).const_add c

lemma fderiv_within_const_add (hxs : unique_diff_within_at 𝕜 s x)
(hf : differentiable_within_at 𝕜 f s x) (c : F) :
@[simp] lemma differentiable_const_add_iff (c : F) :
differentiable 𝕜 (λ y, c + f y) ↔ differentiable 𝕜 f :=
⟨λ h, by simpa using h.const_add (-c), λ h, h.const_add c⟩

lemma fderiv_within_const_add (hxs : unique_diff_within_at 𝕜 s x) (c : F) :
fderiv_within 𝕜 (λy, c + f y) s x = fderiv_within 𝕜 f s x :=
(hf.has_fderiv_within_at.const_add c).fderiv_within hxs
by simpa only [add_comm] using fderiv_within_add_const hxs c

lemma fderiv_const_add
(hf : differentiable_at 𝕜 f x) (c : F) :
fderiv 𝕜 (λy, c + f y) x = fderiv 𝕜 f x :=
(hf.has_fderiv_at.const_add c).fderiv
lemma fderiv_const_add (c : F) : fderiv 𝕜 (λy, c + f y) x = fderiv 𝕜 f x :=
by simp only [add_comm c, fderiv_add_const]

end add


section sum
/-! ### Derivative of a finite sum of functions -/

Expand Down Expand Up @@ -1655,26 +1680,42 @@ lemma differentiable_within_at.neg (h : differentiable_within_at 𝕜 f s x) :
differentiable_within_at 𝕜 (λy, -f y) s x :=
h.has_fderiv_within_at.neg.differentiable_within_at

@[simp] lemma differentiable_at.neg (h : differentiable_at 𝕜 f x) :
@[simp] lemma differentiable_within_at_neg_iff :
differentiable_within_at 𝕜 (λy, -f y) s x ↔ differentiable_within_at 𝕜 f s x :=
⟨λ h, by simpa only [neg_neg] using h.neg, λ h, h.neg⟩

lemma differentiable_at.neg (h : differentiable_at 𝕜 f x) :
differentiable_at 𝕜 (λy, -f y) x :=
h.has_fderiv_at.neg.differentiable_at

@[simp] lemma differentiable_at_neg_iff :
differentiable_at 𝕜 (λy, -f y) x ↔ differentiable_at 𝕜 f x :=
⟨λ h, by simpa only [neg_neg] using h.neg, λ h, h.neg⟩

lemma differentiable_on.neg (h : differentiable_on 𝕜 f s) :
differentiable_on 𝕜 (λy, -f y) s :=
λx hx, (h x hx).neg

@[simp] lemma differentiable.neg (h : differentiable 𝕜 f) :
@[simp] lemma differentiable_on_neg_iff :
differentiable_on 𝕜 (λy, -f y) s ↔ differentiable_on 𝕜 f s :=
⟨λ h, by simpa only [neg_neg] using h.neg, λ h, h.neg⟩

lemma differentiable.neg (h : differentiable 𝕜 f) :
differentiable 𝕜 (λy, -f y) :=
λx, (h x).neg

lemma fderiv_within_neg (hxs : unique_diff_within_at 𝕜 s x)
(h : differentiable_within_at 𝕜 f s x) :
@[simp] lemma differentiable_neg_iff : differentiable 𝕜 (λy, -f y) ↔ differentiable 𝕜 f :=
⟨λ h, by simpa only [neg_neg] using h.neg, λ h, h.neg⟩

lemma fderiv_within_neg (hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λy, -f y) s x = - fderiv_within 𝕜 f s x :=
h.has_fderiv_within_at.neg.fderiv_within hxs
if h : differentiable_within_at 𝕜 f s x
then h.has_fderiv_within_at.neg.fderiv_within hxs
else by { rw [fderiv_within_zero_of_not_differentiable_within_at h,
fderiv_within_zero_of_not_differentiable_within_at, neg_zero], simpa }

lemma fderiv_neg (h : differentiable_at 𝕜 f x) :
fderiv 𝕜 (λy, -f y) x = - fderiv 𝕜 f x :=
h.has_fderiv_at.neg.fderiv
@[simp] lemma fderiv_neg : fderiv 𝕜 (λy, -f y) x = - fderiv 𝕜 f x :=
by simp only [← fderiv_within_univ, fderiv_within_neg unique_diff_within_at_univ]

end neg

Expand Down Expand Up @@ -1756,30 +1797,40 @@ lemma differentiable_within_at.sub_const
differentiable_within_at 𝕜 (λ y, f y - c) s x :=
(hf.has_fderiv_within_at.sub_const c).differentiable_within_at

lemma differentiable_at.sub_const
(hf : differentiable_at 𝕜 f x) (c : F) :
@[simp] lemma differentiable_within_at_sub_const_iff (c : F) :
differentiable_within_at 𝕜 (λ y, f y - c) s x ↔ differentiable_within_at 𝕜 f s x :=
by simp only [sub_eq_add_neg, differentiable_within_at_add_const_iff]

lemma differentiable_at.sub_const (hf : differentiable_at 𝕜 f x) (c : F) :
differentiable_at 𝕜 (λ y, f y - c) x :=
(hf.has_fderiv_at.sub_const c).differentiable_at

lemma differentiable_on.sub_const
(hf : differentiable_on 𝕜 f s) (c : F) :
@[simp] lemma differentiable_at_sub_const_iff (c : F) :
differentiable_at 𝕜 (λ y, f y - c) x ↔ differentiable_at 𝕜 f x :=
by simp only [sub_eq_add_neg, differentiable_at_add_const_iff]

lemma differentiable_on.sub_const (hf : differentiable_on 𝕜 f s) (c : F) :
differentiable_on 𝕜 (λy, f y - c) s :=
λx hx, (hf x hx).sub_const c

lemma differentiable.sub_const
(hf : differentiable 𝕜 f) (c : F) :
@[simp] lemma differentiable_on_sub_const_iff (c : F) :
differentiable_on 𝕜 (λ y, f y - c) s ↔ differentiable_on 𝕜 f s :=
by simp only [sub_eq_add_neg, differentiable_on_add_const_iff]

lemma differentiable.sub_const (hf : differentiable 𝕜 f) (c : F) :
differentiable 𝕜 (λy, f y - c) :=
λx, (hf x).sub_const c

lemma fderiv_within_sub_const (hxs : unique_diff_within_at 𝕜 s x)
(hf : differentiable_within_at 𝕜 f s x) (c : F) :
@[simp] lemma differentiable_sub_const_iff (c : F) :
differentiable 𝕜 (λ y, f y - c) ↔ differentiable 𝕜 f :=
by simp only [sub_eq_add_neg, differentiable_add_const_iff]

lemma fderiv_within_sub_const (hxs : unique_diff_within_at 𝕜 s x) (c : F) :
fderiv_within 𝕜 (λy, f y - c) s x = fderiv_within 𝕜 f s x :=
(hf.has_fderiv_within_at.sub_const c).fderiv_within hxs
by simp only [sub_eq_add_neg, fderiv_within_add_const hxs]

lemma fderiv_sub_const
(hf : differentiable_at 𝕜 f x) (c : F) :
fderiv 𝕜 (λy, f y - c) x = fderiv 𝕜 f x :=
(hf.has_fderiv_at.sub_const c).fderiv
lemma fderiv_sub_const (c : F) : fderiv 𝕜 (λy, f y - c) x = fderiv 𝕜 f x :=
by simp only [sub_eq_add_neg, fderiv_add_const]

theorem has_strict_fderiv_at.const_sub
(hf : has_strict_fderiv_at f f' x) (c : F) :
Expand All @@ -1806,30 +1857,41 @@ lemma differentiable_within_at.const_sub
differentiable_within_at 𝕜 (λ y, c - f y) s x :=
(hf.has_fderiv_within_at.const_sub c).differentiable_within_at

@[simp] lemma differentiable_within_at_const_sub_iff (c : F) :
differentiable_within_at 𝕜 (λ y, c - f y) s x ↔ differentiable_within_at 𝕜 f s x :=
by simp [sub_eq_add_neg]

lemma differentiable_at.const_sub
(hf : differentiable_at 𝕜 f x) (c : F) :
differentiable_at 𝕜 (λ y, c - f y) x :=
(hf.has_fderiv_at.const_sub c).differentiable_at

lemma differentiable_on.const_sub
(hf : differentiable_on 𝕜 f s) (c : F) :
@[simp] lemma differentiable_at_const_sub_iff (c : F) :
differentiable_at 𝕜 (λ y, c - f y) x ↔ differentiable_at 𝕜 f x :=
by simp [sub_eq_add_neg]

lemma differentiable_on.const_sub (hf : differentiable_on 𝕜 f s) (c : F) :
differentiable_on 𝕜 (λy, c - f y) s :=
λx hx, (hf x hx).const_sub c

lemma differentiable.const_sub
(hf : differentiable 𝕜 f) (c : F) :
@[simp] lemma differentiable_on_const_sub_iff (c : F) :
differentiable_on 𝕜 (λ y, c - f y) s ↔ differentiable_on 𝕜 f s :=
by simp [sub_eq_add_neg]

lemma differentiable.const_sub (hf : differentiable 𝕜 f) (c : F) :
differentiable 𝕜 (λy, c - f y) :=
λx, (hf x).const_sub c

lemma fderiv_within_const_sub (hxs : unique_diff_within_at 𝕜 s x)
(hf : differentiable_within_at 𝕜 f s x) (c : F) :
@[simp] lemma differentiable_const_sub_iff (c : F) :
differentiable 𝕜 (λ y, c - f y) ↔ differentiable 𝕜 f :=
by simp [sub_eq_add_neg]

lemma fderiv_within_const_sub (hxs : unique_diff_within_at 𝕜 s x) (c : F) :
fderiv_within 𝕜 (λy, c - f y) s x = -fderiv_within 𝕜 f s x :=
(hf.has_fderiv_within_at.const_sub c).fderiv_within hxs
by simp only [sub_eq_add_neg, fderiv_within_const_add, fderiv_within_neg, hxs]

lemma fderiv_const_sub
(hf : differentiable_at 𝕜 f x) (c : F) :
fderiv 𝕜 (λy, c - f y) x = -fderiv 𝕜 f x :=
(hf.has_fderiv_at.const_sub c).fderiv
lemma fderiv_const_sub (c : F) : fderiv 𝕜 (λy, c - f y) x = -fderiv 𝕜 f x :=
by simp only [← fderiv_within_univ, fderiv_within_const_sub unique_diff_within_at_univ]

end sub

Expand Down