Skip to content

[Merged by Bors] - feat: the norm raised to a power is C^1#14124

Closed
fpvandoorn wants to merge 7 commits intomasterfrom
marginal-lemmas2
Closed

[Merged by Bors] - feat: the norm raised to a power is C^1#14124
fpvandoorn wants to merge 7 commits intomasterfrom
marginal-lemmas2

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Jun 25, 2024 •
edited
Loading

  • From the Sobolev inequality project
  • Generalize continuousAt_rpow_const

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com

Open in Gitpod

@fpvandoorn fpvandoorn added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 25, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 25, 2024 •
edited
Loading

PR summary 3d4c88398f

Import changes

No significant changes to the import graph

Declarations diff

+ ContDiff.norm_rpow
+ Differentiable.fderiv_norm_rpow
+ Differentiable.norm_rpow
+ _root_.Real.nnnorm_rpow_of_nonneg
+ contDiff_norm_rpow
+ contDiff_one_iff_hasFDerivAt
+ continuous_rpow_const
+ differentiable_norm_rpow
+ fderiv_norm_rpow
+ hasDerivAt_abs_rpow
+ hasDerivAt_norm_rpow
+ hasFDerivAt_norm_rpow
+ nnnorm_fderiv_norm_rpow_le
+ norm_fderiv_norm_id_rpow
+ norm_fderiv_norm_rpow_le
++ rpow_add_of_nonneg

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

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

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 25, 2024
@fpvandoorn fpvandoorn changed the title feat: the norm to a power is C^1 feat: the norm raised to a power is C^1 Jun 26, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 26, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jun 26, 2024

This PR/issue depends on:

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 26, 2024
@fpvandoorn fpvandoorn mentioned this pull request Jun 26, 2024
Closed
2 tasks
sgouezel
sgouezel reviewed Jun 26, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

bors d+
Thanks!

Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean Outdated
#align real.continuous_at_rpow_const Real.continuousAt_rpow_const

@[fun_prop]
theorem continuous_rpow_const {q : ℝ} (h : 0 < q) : Continuous (fun x : ℝ => x ^ q) :=
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel Jun 26, 2024

Choose a reason for hiding this comment

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

Could you assume that q is nonnegative instead? (Should be trivial for q = 0).

Copy link
Copy Markdown
Member Author

@fpvandoorn fpvandoorn Jun 26, 2024

Choose a reason for hiding this comment

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

Thanks! I also generalized the previous lemma.

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 26, 2024

✌️ fpvandoorn 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 delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 26, 2024
@fpvandoorn
Copy link
Copy Markdown
Member Author

fpvandoorn commented Jun 26, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jun 26, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 26, 2024
@fpvandoorn
feat: the norm raised to a power is C^1 (#14124)
66c9c68 
* From the Sobolev inequality project
* Generalize `continuousAt_rpow_const`

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 26, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: the norm raised to a power is C^1 [Merged by Bors] - feat: the norm raised to a power is C^1 Jun 26, 2024
@mathlib-bors mathlib-bors bot closed this Jun 26, 2024
@mathlib-bors mathlib-bors bot deleted the marginal-lemmas2 branch June 26, 2024 22:10
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@fpvandoorn @dagurtomas
feat: the norm raised to a power is C^1 (#14124)
1af7a5f 
* From the Sobolev inequality project
* Generalize `continuousAt_rpow_const`

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@fpvandoorn @sgouezel