[Merged by Bors] - feat: Lemmas `DifferentiableAt.add_iff_left`, `DifferentiableAt.add_iff_right` by adomasbaliuka · Pull Request #14593 · leanprover-community/mathlib4

adomasbaliuka · 2024-07-09T23:03:30Z

Given a function differentiable at a point, the result of adding a second function is differentiable (there) iff the second function is differentiable (there).

The part that's new is: at a point, the sum of a differentiable and a non-differentiable function is non-differentiable.
The other direction of the iff is already covered by DifferentiableAt.add.

Lemmas are marked @[simp] because other iff lemmas in that file are marked as such.

Needed for #9734

Lemmas say: at a point, the sum of a differentiable and a non-differentiable function is non-differentiable

github-actions · 2024-07-09T23:04:10Z

PR summary a5922d1d7b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Differentiable.add_iff_left
+ Differentiable.add_iff_right
+ Differentiable.sub_iff_left
+ Differentiable.sub_iff_right
+ DifferentiableAt.add_iff_left
+ DifferentiableAt.add_iff_right
+ DifferentiableAt.sub_iff_left
+ DifferentiableAt.sub_iff_right
+ DifferentiableOn.add_iff_left
+ DifferentiableOn.add_iff_right
+ DifferentiableOn.sub_iff_left
+ DifferentiableOn.sub_iff_right

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

urkud · 2024-07-10T00:05:54Z

Let's test if @[simp] causes troubles.

urkud · 2024-07-10T00:05:59Z

!bench

Mathlib/Analysis/Calculus/FDeriv/Add.lean

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

urkud · 2024-07-10T00:14:48Z

@YaelDillies Could you please remind me what's our convention about left/right in lemmas like these?

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

leanprover-bot · 2024-07-10T01:13:41Z

Here are the benchmark results for commit a839b02.
There were no significant changes against commit 5e75b54.

urkud · 2024-07-10T01:45:04Z

LGTM but I don't remember what's our convention about left/right here, so delegating to Yael who probably remembers it.
bors d=@YaelDillies

mathlib-bors · 2024-07-10T01:45:06Z

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

YaelDillies

binOp_iff_left should be of the form P (binOp f g) \iff P f, and binOp_iff_right should be of the form P (binOp f g) \iff P g.

Can you add the corresponding sub lemmas?

Also replaces simp by simp only. Those simps were terminal, so maybe OK, but I still like seeing what lemmas get used when reading a proof.

adomasbaliuka · 2024-07-10T16:58:15Z

Can you add the corresponding sub lemmas?

Now the linter complains that old lemmas (which concern the special case of subtracting constant) can be proved by simp. What to do?

Do not mark sub_iff_* as @[simp]
Remove the @[simp] mark from the old lemmas
?

YaelDillies · 2024-07-10T18:59:08Z

Remove the simp from the old lemmas (/deprecate the old lemmas since they are superseded?)

Can you also add the DifferentiableOn version of your new lemmas?

Because, e.g., differentiableAt_const also has it.

…ff and differentiable*_const_(sub|add)_iff Because simp can prove these now using the more general lemmas

Mathlib/Analysis/Calculus/FDeriv/Add.lean

YaelDillies

Thanks!

maintainer merge

github-actions · 2024-07-12T11:47:21Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

jcommelin

bors merge

…ff_right` (#14593) Given a function differentiable at a point, the result of adding a second function is differentiable (there) iff the second function is differentiable (there).

mathlib-bors · 2024-07-12T13:14:48Z

This PR was included in a batch that was canceled, it will be automatically retried

…ff_right` (#14593) Given a function differentiable at a point, the result of adding a second function is differentiable (there) iff the second function is differentiable (there).

mathlib-bors · 2024-07-12T15:30:36Z

Pull request successfully merged into master.

Build succeeded:

Adds lemmas

a839b02

Lemmas say: at a point, the sum of a differentiable and a non-differentiable function is non-differentiable

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 9, 2024

adomasbaliuka added the t-analysis Analysis (normed *, calculus) label Jul 9, 2024

adomasbaliuka mentioned this pull request Jul 9, 2024

[Merged by Bors] - feat: Binary entropy #9734

Closed

3 tasks

adomasbaliuka requested a review from YaelDillies July 9, 2024 23:21

urkud reviewed Jul 10, 2024

View reviewed changes

Mathlib/Analysis/Calculus/FDeriv/Add.lean Outdated Show resolved Hide resolved

urkud reviewed Jul 10, 2024

View reviewed changes

Mathlib/Analysis/Calculus/FDeriv/Add.lean Outdated Show resolved Hide resolved

Shortens proof

20c0a9c

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Shortens proof

6eaf202

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 10, 2024

YaelDillies reviewed Jul 10, 2024

View reviewed changes

Adds DifferentiableAt.sub_iff_left and sub_iff_right.

1832211

Also replaces simp by simp only. Those simps were terminal, so maybe OK, but I still like seeing what lemmas get used when reading a proof.

adomasbaliuka added 5 commits July 11, 2024 17:43

Adds the same lemmas for DifferentiableOn

91a2255

Adds same lemmas also for Differentiable

d86cbe4

Adds @[simp] to differentiableOn_const

26c3a4b

Because, e.g., differentiableAt_const also has it.

Deprecates and removes @[simp] from differentiable*_(sub|add)_const_i…

22a550e

…ff and differentiable*_const_(sub|add)_iff Because simp can prove these now using the more general lemmas

Fixes line length limit

166991e

YaelDillies reviewed Jul 11, 2024

View reviewed changes

Mathlib/Analysis/Calculus/FDeriv/Add.lean Outdated Show resolved Hide resolved

adomasbaliuka added 2 commits July 11, 2024 18:19

Adds dates for deprecations and explicit proof terms to replace by

19b2b9f

Replace useage of deprecated lemma

6b28261

YaelDillies reviewed Jul 11, 2024

View reviewed changes

Mathlib/Analysis/Calculus/FDeriv/Add.lean Outdated Show resolved Hide resolved

Nicer proof terms using dot notation

267c820

YaelDillies reviewed Jul 11, 2024

View reviewed changes

Mathlib/Analysis/Calculus/FDeriv/Add.lean Outdated Show resolved Hide resolved

Shortens proofs

a5922d1

YaelDillies approved these changes Jul 12, 2024

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 12, 2024

jcommelin reviewed Jul 12, 2024

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Jul 12, 2024

mathlib-bors bot changed the title ~~feat: Lemmas DifferentiableAt.add_iff_left, DifferentiableAt.add_iff_right~~ [Merged by Bors] - feat: Lemmas DifferentiableAt.add_iff_left, DifferentiableAt.add_iff_right Jul 12, 2024

mathlib-bors bot closed this Jul 12, 2024

mathlib-bors bot deleted the adomas_feat_DifferentiableAt_add_iff branch July 12, 2024 15:30

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Conversation

adomasbaliuka commented Jul 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary a5922d1d7b

Import changes for modified files

Declarations diff

Uh oh!

urkud commented Jul 10, 2024

Uh oh!

urkud commented Jul 10, 2024

Uh oh!

Uh oh!

Uh oh!

urkud commented Jul 10, 2024

Uh oh!

leanprover-bot commented Jul 10, 2024

Uh oh!

urkud commented Jul 10, 2024

Uh oh!

mathlib-bors bot commented Jul 10, 2024

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

adomasbaliuka commented Jul 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies commented Jul 10, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jul 12, 2024

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jul 12, 2024

Uh oh!

mathlib-bors bot commented Jul 12, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

adomasbaliuka commented Jul 9, 2024 •

edited

Loading

github-actions bot commented Jul 9, 2024 •

edited

Loading

adomasbaliuka commented Jul 10, 2024 •

edited

Loading