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] - feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual numbers #18200

Closed
wants to merge 20 commits into from
Closed

[Merged by Bors] - feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual numbers #18200

wants to merge 20 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Jan 17, 2023 •
edited
Loading

In order for convergence to be well-defined, we put the product topology on triv_zero_sq_ext R M via its obvious internal representation as a product.

Zulip thread.

Open in Gitpod

@eric-wieser eric-wieser added help-wanted The author needs attention to resolve issues WIP Work in progress t-analysis Analysis (normed *, calculus) labels Jan 17, 2023
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 17, 2023
@adomani
Copy link
Collaborator

adomani commented Jan 17, 2023

By the way, for a general differentiable function $f$, the identity
$$f (a + b \cdot \varepsilon) = f (a) + b f' (a) \cdot \varepsilon$$
should hold. Maybe this is one of those facts that are easier to prove when generalized?

@eric-wieser eric-wieser added awaiting-review The author would like community review of the PR and removed help-wanted The author needs attention to resolve issues WIP Work in progress labels Jan 17, 2023
@eric-wieser
Copy link
Member Author

I suspect that makes things worse not better, as I can't even talk about differentiability without having the right norm structure!

@bors bors bot changed the base branch from eric-wieser/tsze-pow to master January 18, 2023 20:44
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 18, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@eric-wieser eric-wieser added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jan 18, 2023
j-loreaux
j-loreaux reviewed Jan 24, 2023
View reviewed changes
Copy link
Collaborator

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

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

A few minor comments and golfs, but otherwise looks good to me.

src/topology/instances/triv_sq_zero_ext.lean Outdated Show resolved Hide resolved
src/topology/instances/triv_sq_zero_ext.lean Show resolved Hide resolved
src/topology/instances/triv_sq_zero_ext.lean Outdated Show resolved Hide resolved
src/topology/instances/triv_sq_zero_ext.lean Show resolved Hide resolved
src/topology/instances/triv_sq_zero_ext.lean Outdated Show resolved Hide resolved
src/topology/instances/triv_sq_zero_ext.lean Outdated Show resolved Hide resolved
src/analysis/normed_space/triv_sq_zero_ext.lean Outdated Show resolved Hide resolved
@j-loreaux
Copy link
Collaborator

looks good to me now

maintainer merge

@github-actions
Copy link

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

@eric-wieser eric-wieser mentioned this pull request Feb 4, 2023
Closed
1 task
dupuisf
dupuisf reviewed Feb 10, 2023
View reviewed changes
Copy link
Collaborator

@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.

Thanks!

bors r+

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Feb 10, 2023
bors bot pushed a commit that referenced this pull request Feb 10, 2023
@eric-wieser
feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual num…
806c0bb 
…bers (#18200)

In order for convergence to be well-defined, we put the product topology on `triv_zero_sq_ext R M` via its obvious internal representation as a product.

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Exponentials.20in.20seminormed.20algebras/near/321870256).
@bors
Copy link

bors bot commented Feb 10, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual numbers [Merged by Bors] - feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual numbers Feb 10, 2023
@bors bors bot closed this Feb 10, 2023
@bors bors bot deleted the eric-wieser/tsze-norm branch February 10, 2023 22:09
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

@j-loreaux j-loreaux Awaiting requested review from j-loreaux

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-analysis Analysis (normed *, calculus) t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@eric-wieser @adomani @mathlib-dependent-issues-bot @j-loreaux @dupuisf @leanprover-community-bot-assistant