Skip to content

[Merged by Bors] - feat: Generalize statements about deriv of MulLog#14594

Closed
adomasbaliuka wants to merge 8 commits intomasterfrom
adomas_generalize_deriv_NegMulLog
Closed

[Merged by Bors] - feat: Generalize statements about deriv of MulLog#14594
adomasbaliuka wants to merge 8 commits intomasterfrom
adomas_generalize_deriv_NegMulLog

Conversation

@adomasbaliuka
Copy link
Copy Markdown
Collaborator

@adomasbaliuka adomasbaliuka commented Jul 9, 2024

Uses non-differentiability to generalize statements about deriv of MulLog

Moved over from PR #9734.

Open in Gitpod

@adomasbaliuka
Adds lemmas, removes assumption
45f5363 
Moved over from PR #9734. Uses non-differentiability to generalize statements about deriv of MulLog
@github-actions 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
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 9, 2024 •
edited
Loading

PR summary 311e28459f

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ deriv_mul_log_zero
+ differentiableAt_negMulLog_iff
+ not_DifferentiableAt_log_mul_zero
+ not_continuousAt_deriv_mul_log_zero
+ not_continuousAt_of_tendsto

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

@adomasbaliuka adomasbaliuka added t-analysis Analysis (normed *, calculus) awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 9, 2024
@adomasbaliuka adomasbaliuka marked this pull request as draft July 9, 2024 23:33
@adomasbaliuka adomasbaliuka mentioned this pull request Jul 9, 2024
Closed
3 tasks
adomasbaliuka
adomasbaliuka commented Jul 9, 2024
View reviewed changes
adomasbaliuka
adomasbaliuka commented Jul 9, 2024
View reviewed changes
llllvvuu
llllvvuu reviewed Jul 10, 2024
View reviewed changes
@adomasbaliuka adomasbaliuka marked this pull request as ready for review August 9, 2024 11:37
dupuisf
dupuisf reviewed Aug 9, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@dupuisf dupuisf left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, thanks a lot for your patience! I just have a few final comments but otherwise let's merge this.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 9, 2024

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

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 9, 2024
adomasbaliuka and others added 2 commits August 10, 2024 09:32
@adomasbaliuka @dupuisf
Improves docstring in Mathlib/Analysis/SpecialFunctions/Log/NegMulLog…
a099b11 
….lean

Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
@adomasbaliuka
Updates docstrings
311e284
@adomasbaliuka
Copy link
Copy Markdown
Collaborator Author

adomasbaliuka commented Aug 10, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Aug 10, 2024
@adomasbaliuka
feat: Generalize statements about deriv of MulLog (#14594)
a43394c 
Uses non-differentiability to generalize statements about deriv of MulLog
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 10, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Generalize statements about deriv of MulLog [Merged by Bors] - feat: Generalize statements about deriv of MulLog Aug 10, 2024
@mathlib-bors mathlib-bors bot closed this Aug 10, 2024
@mathlib-bors mathlib-bors bot deleted the adomas_generalize_deriv_NegMulLog branch August 10, 2024 08:44
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@adomasbaliuka @bjoernkjoshanssen
feat: Generalize statements about deriv of MulLog (#14594)
53d6833 
Uses non-differentiability to generalize statements about deriv of MulLog
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@adomasbaliuka @bjoernkjoshanssen
feat: Generalize statements about deriv of MulLog (#14594)
0918c13 
Uses non-differentiability to generalize statements about deriv of MulLog
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@adomasbaliuka @bjoernkjoshanssen
feat: Generalize statements about deriv of MulLog (#14594)
8da3e19 
Uses non-differentiability to generalize statements about deriv of MulLog
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dupuisf dupuisf dupuisf left review comments

+1 more reviewer

@llllvvuu llllvvuu llllvvuu left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@adomasbaliuka @llllvvuu @dupuisf