feat(analysis): seminorms and local convexity #1926
Conversation
- rename `smul_set` to `scale_set` for disambiguation - define `scale_set_action`, which subsumes `one_smul_set` - additional lemmas lemmas
- also add documentation
jcommelin
added
the
blocked-by-other-PR
jlpaca
changed the title
- subsume `pointwise_mul_action`
- also restore name of `smul_set`
- subsumed by `smul_set_action` with left-regular action.
* resolve updates in `analysis/convex` and `algebra/pointwise`.
jlpaca
removed
the
blocked-by-other-PR
src/analysis/seminorm.lean
Outdated
| -- TODO: this code compiles if it asks only for much weaker instances | ||
| -- [has_norm 𝕜] [has_scalar 𝕜 E] [has_add E], but that feels weird, | ||
| -- especially since this is not a class that extends something else | ||
| -- which contains additional hypotheses that make the maths sensible. |
There was a problem hiding this comment.
I think this is fine. I'd be happy with just removing the TODO.
| -- TODO: extract as lemmas the statements a • int A = int (a • A) and | ||
| -- a • cl A = cl (a • A) ? unless there's some sleek one-liner that | ||
| -- gives the result via `homeomorph` somehow. |
There was a problem hiding this comment.
Extracting those lemmas seems reasonably useful. Up to you.
src/analysis/seminorm.lean
Outdated
| @[simp] | ||
| lemma seminorm_sub_rev : p (x - y) = p (y - x) := |
There was a problem hiding this comment.
| @[simp] | |
| lemma seminorm_sub_rev : p (x - y) = p (y - x) := | |
| lemma seminorm_sub_rev : p (x - y) = p (y - x) := |
Should not be a simp lemma.
|
@jlpaca, what's your intention with this? Would you like it merged as is (if so can you remove the WIP label), or are you planning to add more? |
|
@semorrison thanks for the review! There were a few more results that I thought I wanted to have in this before I attempted to get it reviewed for merging, but I got buried by other stuff and never got back to it — sorry for the negligence. I will make an effort later today to clean this up (implement the changes from the review, resolve conflicts, remove spurious comments) and remove the WIP tag once it's ready; and present any additional results in separate PRs. |
|
Hi @jlpaca, what are your plans about this PR? My recommendation: resolve merge conflict, fix minor issues pointed by @semorrison , and get it merged. If you want to formalize more facts, you can always make another PR. Reason: as soon as a PR is merged, you can be sure that no other PR will break it. |
- also remove some TODO comments
|
@urkud hi, so sorry for having been bad about this. I do still wish to continue to work on this (unless the content here has been superseded by other work that's been done since I disappeared for a while.) But I've been encountering some problems with building lean/mathlib locally & I'm not sure how long those will take to eventually sort out, so I've tried to follow the recommendation & fixed the conflict/issues so that the parts that are already done would be ready to be reviewed for merging. |
fpvandoorn
added
the
please-adopt
|
It has to be pretty out of sync — I haven't touched it since I left the last message in May. I would attempt to bring the branch up to date again, but I think it may be easier to close this for now & I'll open a separate PR that supercedes this one for a version that's ready for review? |
An attempt at the beginning of some stuff about topological vector spaces.
Kept being indecisive about conventions and design choices, and eventually decided to put this out here with accompanied by copious amounts of
TODOcomments. I'm interested in developing this further if it hasn't been done somewhere already, and in that case I'd really appreciate some guidance from people who know the language & the library better so that things are set up in a sensible way.