Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Refactor operator norm#919

Closed
jlpaca wants to merge 11 commits intoleanprover-community:masterfrom
jlpaca:refactor-op-norm
Closed

Refactor operator norm#919
jlpaca wants to merge 11 commits intoleanprover-community:masterfrom
jlpaca:refactor-op-norm

Conversation

@jlpaca
Copy link
Copy Markdown
Collaborator

@jlpaca jlpaca commented Apr 10, 2019 •
edited
Loading

First part of a process towards restating deriv.lean in terms of bundled bounded linear maps. Supersedes #726 : @sgouezel has kindly pointed out that much of the work there has become outdated and/or duplicated; this is an attempt at cleaning up the mess I made.

Some names for theorems and definitions have been altered for adherence to conventions, or for brevity. Please see comments on #726 and commit messages in this PR for detailed accounts of changes.

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • for tactics:
  • make sure definitions and lemmas are put in the right files
  • make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

jlpaca added 3 commits April 10, 2019 19:23
@jlpaca
style(analysis/normed_space/bounded_linear_map): minor edits
85bb2c2 
- extract some variables
- use consistent notation for hypotheses & use `let` instead of invoking equation compiler
- remove spurious imports
@jlpaca
refactor(analysis/normed_space/operator_norm): refactor operator norm
d8bf7f4 
- rename `bounded_linear_maps` to `bounded_linear_map`.

- make some straightforward lemmas available to `simp`.

- change the definition of `operator_norm` to be the inf of all the bounds
  (prove that the image of the unit ball is bounded as a lemma).

- change the names of some theorems to be consistent with conventions elsewhere
  in mathlib: replace `bounded_by_*` with `le_*`, `operator_norm_homogeneous` with
  `operator_norm_smul`.

- remove some implicit arguments.

- additional miscellaneous lemmas: that the operator norm is submultiplicative, also
  lipschitz continuity.
@jlpaca
chore(analysis/normed_space/operator_norm): add attribution
363f75c
@jlpaca jlpaca requested a review from a team as a code owner April 10, 2019 18:26
@jlpaca jlpaca changed the title Refactor op norm Refactor operator_norm.lean Apr 10, 2019
@jlpaca jlpaca changed the title Refactor operator_norm.lean Refactor operator norm Apr 10, 2019
sgouezel
sgouezel previously requested changes Apr 11, 2019
View reviewed changes
Copy link
Copy Markdown
Collaborator

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

You always indent your proofs by at least two spaces with respect to the left margin. Normally, the left-most lines of a proof should not be indented.

@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Apr 11, 2019

I forgot: if you want the travis tests to pass, you should PR from a branch on mathlib-community.

@mergify mergify bot dismissed sgouezel’s stale review April 11, 2019 12:43

Pull request has been modified.

@jlpaca
style(analysis/normed_space/operator_norm): style fixes
2f18f44 
- use curly brackets for one-line tactic proofs without multiple goals.
- fix error in statement of `coe_zero`.
- adjust indentation.
@jlpaca
Copy link
Copy Markdown
Collaborator Author

jlpaca commented Apr 11, 2019

made all the requested changes to the code. Thanks for the pointers.

@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Apr 11, 2019

Almost good for me, thanks for the update. I just realized that you stop the bounded_linear_map namespace in the middle of the file. This means that statements like bounds_nonempty or lipschitz are in the root namespace. Instead, I would put the line end bounded_linear_map at the very end of the file (and change the name of the instance bounded_linear_map.to_normed_space).

@jlpaca
Copy link
Copy Markdown
Collaborator Author

jlpaca commented Apr 11, 2019 •
edited
Loading

I did? That's very silly, thanks for pointing it out.

I also suspect bounds_nonempty should really be called something like exists_bound instead, but I'm not sure how confusing that would be, considering especially that the only difference from f.property.bound is a less-than-or-equals-to sign. I don't expect the statements that the set of bounds is nonempty and bounded below are very useful anywhere else other than for inf/sup manipulation in this file, anyway, though, so I don't know. I'm leaving it as is for the time being.

I've made the edit for the namespace thing, and am just making sure my copy of mathlib compiles. I'll be committing the changes in a moment.

jlpaca added 2 commits April 11, 2019 14:59
@jlpaca
fix(analysis/normed_space/operator_norm): fix namespace scope
26c8664 
- place several theorems under the `bounded_linear_map` namespace.
- remove spurious `noncomputable`.
@jlpaca
Merge branch 'master' of https://github.com/leanprover-community/mathlib
3f285a5 
 into refactor-op-norm
@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Apr 11, 2019

Looks good to me.

@jlpaca
Copy link
Copy Markdown
Collaborator Author

jlpaca commented Apr 13, 2019

closing this and PR-ing the same content from a refactor-op-norm branch of community mathlib so that the Travis checks can work.

@jlpaca jlpaca closed this Apr 13, 2019
@jlpaca jlpaca mentioned this pull request Apr 13, 2019
Merged
6 tasks
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@sgouezel sgouezel sgouezel left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@jlpaca @sgouezel