feat(analysis/normed_space) bundled bounded linear maps by jlpaca · Pull Request #726 · leanprover-community/mathlib3

jlpaca · 2019-02-14T20:28:56Z

bounded_linear_map as a structure.
some elementary properties of the operator norm.

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
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

PatrickMassot

I left some minor comments

src/analysis/normed_space/bounded_linear_maps.lean

src/analysis/normed_space/operator_norm.lean

- bounded_linear_map is a k-vector space - bounded_linear_map together with op_norm are a normed space

… endomorphism algebra

…uous

into operator-norm

jcommelin

Some minor comments about comments

src/analysis/normed_space/bounded_linear_maps.lean

src/analysis/normed_space/operator_norm.lean

src/analysis/normed_space/bounded_linear_maps.lean

…perator-norm - also some notation for bounded_linear_map

jlpaca · 2019-03-29T16:46:27Z

@jcommelin Thanks for the pointers. a0369fd removes some spurious comments and adds docstrings.

jcommelin

Some more comments.

jcommelin · 2019-03-29T17:40:00Z

src/analysis/normed_space/bounded_linear_maps.lean

+import ring_theory.algebra
 import analysis.normed_space.basic
-import analysis.asymptotics
+import ..asymptotics


I think this is not conform mathlib style.

jcommelin · 2019-03-29T17:42:17Z

src/analysis/normed_space/bounded_linear_maps.lean

+def of_linear_map_of_bounded {f : E →ₗ[k] F}
+  (h : ∃ M, ∀ x, ∥f x∥ ≤ M * ∥x∥) : E →L[k] F := ⟨f, h⟩
+
+/-- the zero map is bounded.     -/


Suggested change

/-- the zero map is bounded. -/

/-- The bounded map that is constantly zero. -/

jcommelin · 2019-03-29T17:42:42Z

src/analysis/normed_space/bounded_linear_maps.lean

+/-- the identity map is bounded. -/
+def id   : E →L[k] E := ⟨linear_map.id, 1, λ x, le_of_eq (one_mul _).symm⟩
+
+/-- the composition of two bounded linear maps is bounded. -/


Suggested change

/-- the composition of two bounded linear maps is bounded. -/

/-- Composition of bounded linear maps. -/

jcommelin · 2019-03-29T17:43:11Z

src/analysis/normed_space/bounded_linear_maps.lean

+  commutes' := λ _ _, ext $ λ _, map_smul _ _ _,
+}
+
+/-- bounded linear maps are continuous. -/


Suggested change

/-- bounded linear maps are continuous. -/

/-- Bounded linear maps are continuous. -/

jcommelin · 2019-03-29T17:43:53Z

src/analysis/normed_space/operator_norm.lean

+
+noncomputable instance : has_norm (bounded_linear_map k E F) := ⟨op_norm⟩
+
+-- so that invocations of real.Inf_le make sense: the set of


This comment seems to start halfway a sentence.

jcommelin · 2019-03-29T17:44:12Z

src/analysis/normed_space/operator_norm.lean

+  (λ hlt, div_le_of_le_mul hlt (by rw mul_comm; exact le_op_norm _))
+  (λ heq, by rw [←heq, div_zero]; exact op_norm_nonneg _))
+
+/-- the image of the unit ball under a bounded linear map is bounded. -/


Suggested change

/-- the image of the unit ball under a bounded linear map is bounded. -/

/-- The image of the unit ball under a bounded linear map is bounded. -/

jcommelin · 2019-03-29T17:44:50Z

src/analysis/normed_space/operator_norm.lean

+  (λ heq, by rw [←heq, div_zero]; exact op_norm_nonneg _))
+
+/-- the image of the unit ball under a bounded linear map is bounded. -/
+lemma unit_le_op_norm : ∥x∥ ≤ 1 → ∥f x∥ ≤ ∥f∥ :=


I think you might as well move hx : ||x|| <= 1 to the assumptions.

jcommelin · 2019-03-29T17:46:00Z

src/analysis/normed_space/operator_norm.lean

+            (by rw [ mul_comm, ←norm_smul ]; exact hc _))⟩))
+        (λ heq, by rw [←heq, zero_mul]; exact hn))))
+
+/-- bounded linear maps themselves form a normed space w/ the op norm -/


Suggested change

/-- bounded linear maps themselves form a normed space w/ the op norm -/

/-- Bounded linear maps form a normed space with respect to the operator norm -/

jcommelin · 2019-03-29T17:46:13Z

src/analysis/normed_space/operator_norm.lean

+noncomputable instance : normed_space k (bounded_linear_map k E F) :=
+  normed_space.of_core _ _ ⟨op_norm_eq_zero, op_norm_smul, op_norm_triangle⟩
+
+/-- operator norm is submultiplicative. -/


Suggested change

/-- operator norm is submultiplicative. -/

/-- The operator norm is submultiplicative. -/

jcommelin · 2019-03-29T17:46:25Z

src/analysis/normed_space/operator_norm.lean

+  λ x, by rw mul_assoc; calc _ ≤ ∥h∥ * ∥f x∥: le_op_norm _
+  ... ≤ _ : mul_le_mul_of_nonneg_left (le_op_norm _) (op_norm_nonneg _)⟩)
+
+/-- bounded linear maps are lipschitz continuous. -/


Suggested change

/-- bounded linear maps are lipschitz continuous. -/

/-- Bounded linear maps are lipschitz continuous. -/

…ear maps - chain rule lemma & two results about real normed spaces work in progress

…perator-norm

sgouezel · 2019-04-09T10:16:33Z

What is the status of this pull request? If I understand correctly, there are two things in there:

remove is_bounded_linear_map, and replace it by a bundled version.
use the bundled version for the differential.

I don't really understand the point of the first item: it is certainly better to have both unbundled and bundled versions, and both versions are already there (the bundled version is in the current version of operator_norm.lean -- it is called bounded_linear_maps currently, it would probably be a good idea to rename it bounded_linear_map). And all the properties you prove for your bundled version and the operator norm are already there.

On the other hand, I think the second item (using bundled version for the differential) is a good move. What about :

closing this PR
opening a PR where you refactor what you want to refactor in operator_norm.lean (changing the name of bounded_linear_maps, adding the lemmas that you think are missing, but without erasing everything and starting from scratch)
and once this PR is merged opening another PR in which you would refactor the derivative, to make it use the bundled version

Does it sound reasonable to you?

jlpaca · 2019-04-09T14:56:31Z

@sgouezel most of this is admittedly my fault for not spending as much time as consistently as I'd like on this, and mathlib moves forward fast.

So about the content of the PR: at the time I started working on this, the state of normed_space/ was roughly:

bounded_linear_maps.lean contained is_bounded_linear_map, which returned a Prop.
operator_norm.lean contained bounded_linear_maps.lean, which was 'bundled' in the sense that it implements bounded linear maps as a subspace of the vector space of linear maps, with a carrier made up of all the linear maps satisfying is_bounded_linear_map, and a normed_space instance was constructed for that subspace in the case where the base field is the reals.

The changes that are/were part of this PR:

added bounded_linear_map, which is 'bundled' in the sense that it is a structure consisting of a linear_map and a proof of the existence of a bound. Reproduced all of the results about is_bounded_linear_map for bounded_linear_map. (So I suspect this is where much of the confusion comes from.)
refactored the proofs for certain properties of the operator norm to be more straightforward, and constructed the normed_space instance of the type bounded_linear_map over arbitrary normed fields, together with some additional lemmas and instances such as Lipschitz continuity, the endomorphism algebra, and asymptotics.
refactored the derivative to use bounded_linear_map. Currently all the theorems in deriv.lean have been restated, and the sole incomplete proof is a lemma that's invoked for the chain rule.
the prospective removal of is_bounded_linear_map and bounded_linear_maps, once all that is done.

I think closing this and opening separate PRs for the refactor and the derivative is a sensible thing to do, and I'll probably do that in the coming couple of days. I imagine it'd make the changes much easier to review. The only thing that would probably need figuring out is whether to keep both implementations of the normed space of bounded linear maps (the subtype bounded_linear_maps in mathlib master, and the normed_space instance for bounded_linear_map in this PR.)

I don't have strong feelings about whether or not to remove is_bounded_linear_map — I defaulted towards removal, I think, because of the zulip thread back when I started work on this. I'd be perfectly happy to keep both versions and settling on some naming convention that keeps things from being ambiguous and confusing.

sgouezel · 2019-04-09T18:28:41Z

I think it is better to keep the unbundled version is_bounded_linear_map.

As for the bundled version, we already have one, in the form of bounded_linear_maps (defined as a subspace, but still an element of this type is a bundled bounded linear map). You introduce another one. I don't have strong feelings on which one is better (or rather, I think they are essentially equivalent), but my point is that we should only have one bundled version, not two.

sgouezel · 2019-04-10T14:56:42Z

Would you mind if I try to rebase your branch on master and try some minor changes?

jlpaca · 2019-04-10T15:55:04Z

@sgouezel please go ahead with the rebase. Just so I don't be a doofus with duplicated work again, would you mind outlining what sort of changes you mean to exact?

Meanwhile, I'm working on the first of the two suggested refactor PRs as I speak. Expected changes are:

remove this branch's bounded_linear_map from bounded_linear_maps.lean, and refactor mathlib's linear-subspace implementation of is_bounded_linear_maps, renaming that to bounded_linear_map.
replicate all the additional miscellaneous lemmas in the branch for the refactored bounded_linear_map.
refactor most of operator_norm.

also possibly

refactor is_bounded_linear_map, changing the definition. The mathlib code has the existence of a positive bound (instead of just any bound) to be the defining property, and this seems to go against the idea that the code should be asking the user for proofs of a minimal amount of things. The statement of all the lemmas will remain unchanged, so I don't this would be a bad breaking change.

The actual PR should probably exist by tonight or tomorrow.

Does that sound alright?

sgouezel · 2019-04-10T16:28:48Z

Great to hear you're working on it. Since you're working on it, I won't do any refactor. What you propose sounds great.

As for the condition in is_bounded_linear_map that the bound is positive, there are two different things. When you use the definition, you are happy to know that the bound is positive. But when you check the definition, you don't want to check the positivity. So, if there is the positivity in the definition, there should be a constructor without the positivity. And if the positivity is not in the definition, there should be a lemma saying that a positive bound exists. I would say that one uses the definition more often than one checks it, so I would keep the positivity in the definition.

jcommelin · 2019-05-03T18:55:20Z

@jlpaca @sgouezel Is there anything left in this PR that hasn't been included in #927 or #955? Should this now be closed?

sgouezel · 2019-05-03T19:09:31Z

Yes, this should be closed.

jlpaca changed the title ~~Operator norm [WIP]~~ feat(analysis/normed_space/bounded_linear_maps) operator norm [WIP] Feb 14, 2019

kckennylau added the WIP Work in progress label Feb 14, 2019

kckennylau changed the title ~~feat(analysis/normed_space/bounded_linear_maps) operator norm [WIP]~~ feat(analysis/normed_space/bounded_linear_maps) operator norm Feb 14, 2019

cipher1024 requested a review from avigad February 14, 2019 21:31

cipher1024 assigned avigad Feb 14, 2019

jlpaca changed the title ~~feat(analysis/normed_space/bounded_linear_maps) operator norm~~ feat(analysis/normed_space) bundled bounded linear maps Feb 23, 2019

feat(src/analysis/normed_space): bundled bounded linear maps

3dadbb2

PatrickMassot reviewed Feb 23, 2019

View reviewed changes

jlpaca added 7 commits February 23, 2019 21:52

fix(analysis/normed_space): remove useless assumptions

8946ddc

feat(analysis/normed_space): add instances

8f29140

- bounded_linear_map is a k-vector space - bounded_linear_map together with op_norm are a normed space

feat(analysis/normed_space/bounded_linear_maps): add instance for the…

9f3e508

… endomorphism algebra

fix(analysis/normed_space): fix type class resolution issue

9a3cce0

feat(analysis/normed_space): bounded linear maps are lipschitz contin…

d429d04

…uous

style(analysis/normed_space): remove trailing whitespace

72d3124

Merge branch 'master' of https://github.com/leanprover-community/mathlib

91cc7c0

into operator-norm

jcommelin reviewed Mar 29, 2019

View reviewed changes

Merge branch 'master' of https://github.com/leanprover/mathlib into o…

4cfd242

…perator-norm - also some notation for bounded_linear_map

doc(analysis/normed_space): docstrings

a0369fd

jcommelin reviewed Mar 29, 2019

View reviewed changes

jlpaca added 2 commits April 6, 2019 17:30

refactor(analysis/normed_space): derivatives with bundled bounded lin…

9a54783

…ear maps - chain rule lemma & two results about real normed spaces work in progress

Merge branch 'master' of https://github.com/leanprover/mathlib into o…

8f37d10

…perator-norm

jlpaca requested a review from a team as a code owner April 6, 2019 17:14

jlpaca mentioned this pull request Apr 10, 2019

Refactor operator norm #919

Closed

6 tasks

jlpaca mentioned this pull request Apr 17, 2019

feat(analysis/normed_space): more facts about operator norm #927

Merged

6 tasks

sgouezel mentioned this pull request Apr 20, 2019

refactor(analysis/normed_space/operator_norm): replace subspace with … #955

Merged

sgouezel closed this May 3, 2019

	/-- the zero map is bounded. -/
	/-- The bounded map that is constantly zero. -/

	/-- the composition of two bounded linear maps is bounded. -/
	/-- Composition of bounded linear maps. -/

	/-- bounded linear maps are continuous. -/
	/-- Bounded linear maps are continuous. -/


		noncomputable instance : has_norm (bounded_linear_map k E F) := ⟨op_norm⟩

		-- so that invocations of real.Inf_le make sense: the set of

	/-- the image of the unit ball under a bounded linear map is bounded. -/
	/-- The image of the unit ball under a bounded linear map is bounded. -/

	/-- bounded linear maps themselves form a normed space w/ the op norm -/
	/-- Bounded linear maps form a normed space with respect to the operator norm -/

	/-- operator norm is submultiplicative. -/
	/-- The operator norm is submultiplicative. -/

	/-- bounded linear maps are lipschitz continuous. -/
	/-- Bounded linear maps are lipschitz continuous. -/

Conversation

jlpaca commented Feb 14, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

PatrickMassot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jlpaca commented Mar 29, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sgouezel commented Apr 9, 2019

Uh oh!

jlpaca commented Apr 9, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgouezel commented Apr 9, 2019

Uh oh!

sgouezel commented Apr 10, 2019

Uh oh!

jlpaca commented Apr 10, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgouezel commented Apr 10, 2019

Uh oh!

jcommelin commented May 3, 2019

Uh oh!

sgouezel commented May 3, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

jlpaca commented Feb 14, 2019 •

edited

Loading

jlpaca commented Mar 29, 2019 •

edited

Loading

jlpaca commented Apr 9, 2019 •

edited

Loading

jlpaca commented Apr 10, 2019 •

edited

Loading