[Merged by Bors] - feat(analysis/seminorm): The norm as a seminorm, balanced and absorbent lemmas #11487
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
YaelDillies
added
the
awaiting-review
leanprover-community-bot-assistant
added
the
blocked-by-other-PR
8 tasks
mcdoll
reviewed
Jan 16, 2022
src/analysis/seminorm.lean
Outdated
Comment on lines
587
to
591
| def norm_seminorm : seminorm 𝕜 E := | ||
| { to_fun := norm, | ||
| smul' := norm_smul, | ||
| triangle' := norm_add_le } | ||
|
|
There was a problem hiding this comment.
I feel like this should belong into analysis/normed_space/basis, but that would cause problems because that files contains the definition of normed_field, which we need for seminorm. But if that were not a problem, we could transfer quite a few lemmas from normed_space to seminorm.
There was a problem hiding this comment.
Also we have the following code to make a seminorm into a semi_normed_space:
instance (s : seminorm 𝕜 E) : has_norm s.domain := ⟨s.to_fun⟩
lemma is_core (s : seminorm 𝕜 E) : semi_normed_group.core s.domain :=
⟨s.zero, s.triangle, s.neg⟩
instance (s : seminorm 𝕜 E) : semi_normed_group s.domain :=
semi_normed_group.of_core s.domain s.is_core
lemma smul_le (s : seminorm 𝕜 E) (c : 𝕜) (x : E) : s (c • x) ≤ ∥c∥ * s x := by rw s.smul
instance (s : seminorm 𝕜 E) : semi_normed_space 𝕜 s.domain := {norm_smul_le := s.smul_le}
which implies that the two definitions are equivalent after #8218 is merged.
There was a problem hiding this comment.
There is a greater refactor to be done here, by making seminorm the primitive thing. The original problem is that @riccardobrasca didn't know about seminorm when first writing semi_normed_group.
But I think this is out of scope for this PR.
There was a problem hiding this comment.
I totally agree that sooner or later we have to do the refactor to have only one notion of seminormed stuff.
eric-wieser
reviewed
Jan 16, 2022
leanprover-community-bot-assistant
added
the
merge-conflict
leanprover-community-bot-assistant
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
leanprover-community-bot-assistant
removed
the
merge-conflict
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
Thanks for reviewing! bors merge |
bors bot
pushed a commit
that referenced
this pull request
Jan 26, 2022
…nt lemmas (#11487) This * defines `norm_seminorm`, the norm as a seminorm. This is useful to translate seminorm lemmas to norm lemmas * proves many lemmas about `balanced`, `absorbs`, `absorbent` * generalizes many lemmas about the aforementioned predicates. In particular, `one_le_gauge_of_not_mem` now takes `(star_convex ℝ 0 s) (absorbs ℝ s {x})` instead of `(convex ℝ s) ((0 : E) ∈ s) (is_open s)`. The new `star_convex` lemmas justify that it's a generalization. * proves `star_convex_zero_iff` * proves `ne_zero_of_norm_ne_zero` and friends * makes `x` implicit in `convex.star_convex` * renames `balanced.univ` to `balanced_univ`
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
ericrbg
pushed a commit
that referenced
this pull request
Jan 28, 2022
…nt lemmas (#11487) This * defines `norm_seminorm`, the norm as a seminorm. This is useful to translate seminorm lemmas to norm lemmas * proves many lemmas about `balanced`, `absorbs`, `absorbent` * generalizes many lemmas about the aforementioned predicates. In particular, `one_le_gauge_of_not_mem` now takes `(star_convex ℝ 0 s) (absorbs ℝ s {x})` instead of `(convex ℝ s) ((0 : E) ∈ s) (is_open s)`. The new `star_convex` lemmas justify that it's a generalization. * proves `star_convex_zero_iff` * proves `ne_zero_of_norm_ne_zero` and friends * makes `x` implicit in `convex.star_convex` * renames `balanced.univ` to `balanced_univ`
bors bot
pushed a commit
that referenced
this pull request
Mar 12, 2022
…12624) Move `balanced`, `absorbs`, `absorbent` to a new file. For `analysis.seminorm`, I'm crediting * Jean for #4827 * myself for * #9097 * #11487 * Moritz for * #11329 * #11414 * #11477 For `analysis.locally_convex.basic`, I'm crediting * Jean for #4827 * Bhavik for * #7358 * #9097 * myself for * #9097 * #10999 * #11487
laurentbartholdi
pushed a commit
that referenced
this pull request
Mar 17, 2022
…12624) Move `balanced`, `absorbs`, `absorbent` to a new file. For `analysis.seminorm`, I'm crediting * Jean for #4827 * myself for * #9097 * #11487 * Moritz for * #11329 * #11414 * #11477 For `analysis.locally_convex.basic`, I'm crediting * Jean for #4827 * Bhavik for * #7358 * #9097 * myself for * #9097 * #10999 * #11487
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This
norm_seminorm, the norm as a seminorm. This is useful to translate seminorm lemmas to norm lemmasbalanced,absorbs,absorbentone_le_gauge_of_not_memnow takes(star_convex ℝ 0 s) (absorbs ℝ s {x})instead of(convex ℝ s) ((0 : E) ∈ s) (is_open s). The newstar_convexlemmas justify that it's a generalization.star_convex_zero_iffne_zero_of_norm_ne_zeroand friendsximplicit inconvex.star_convexbalanced.univtobalanced_univ@mcdoll, this might be of interest