[Merged by Bors] - feature(Analysis/Convex/Basic): Convexity and the algebra map#29248
[Merged by Bors] - feature(Analysis/Convex/Basic): Convexity and the algebra map#29248mans0954 wants to merge 18 commits intoleanprover-community:masterfrom
Conversation
PR summary 6549fa3760Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
The proof is inspired by |
|
c.f. #29075 |
|
CC: @Timeroot - any thoughts on this PR please? |
j-loreaux
left a comment
j-loreaux
left a comment
There was a problem hiding this comment.
Certainly this seems useful, but I'm a bit unclear about the supposed extra generality.
I would like to switch some statements about Hahn-Banach to use LocallyConvexSpace 𝕜 E instead of LocallyConvexSpace ℝ E with this.
j-loreaux
added
the
awaiting-author
@j-loreaux it's an artifact of me starting this PR before I was aware of #29075 - I've removed the unnecessary extra generality now.
You might also be interested in #29342 which sorts out an awkward work-around in the definition of |
mans0954
removed
the
awaiting-author
| variable {M : Type*} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] | ||
| variable [PartialOrder R] [PartialOrder A] | ||
|
|
||
| lemma convex_of_nonneg_surjective_algebraMap [FaithfulSMul R A] {s : Set M} |
There was a problem hiding this comment.
The name of this declaration is a little misleading as Function.Surjective does not appear, but I think it's a niche enough result that I'm not going to quibble further.
Let `R` and `A` be ordered rings, `A` an `R`-algebra and `R`, `A`, `M` a scalar tower. We provide sufficient conditions for an `R`-convex subset of `M` to be `A`-convex and for an `A`-convex subset of `M` to be `R`-convex. These are used to show that, when `K` is `RCLike` and `ℝ` `K` `E` is a scalar tower, a set is `K`-convex if and only if it is `ℝ`-convex. Used in #29258
ghost
added
the
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…over-community#29248) Let `R` and `A` be ordered rings, `A` an `R`-algebra and `R`, `A`, `M` a scalar tower. We provide sufficient conditions for an `R`-convex subset of `M` to be `A`-convex and for an `A`-convex subset of `M` to be `R`-convex. These are used to show that, when `K` is `RCLike` and `ℝ` `K` `E` is a scalar tower, a set is `K`-convex if and only if it is `ℝ`-convex. Used in leanprover-community#29258
…over-community#29248) Let `R` and `A` be ordered rings, `A` an `R`-algebra and `R`, `A`, `M` a scalar tower. We provide sufficient conditions for an `R`-convex subset of `M` to be `A`-convex and for an `A`-convex subset of `M` to be `R`-convex. These are used to show that, when `K` is `RCLike` and `ℝ` `K` `E` is a scalar tower, a set is `K`-convex if and only if it is `ℝ`-convex. Used in leanprover-community#29258
2 participants
Let
RandAbe ordered rings,AanR-algebra andR,A,Ma scalar tower. We provide sufficient conditions for anR-convex subset ofMto beA-convex and for anA-convex subset ofMto beR-convex.These are used to show that, when
KisRCLikeandℝKEis a scalar tower, a set isK-convex if and only if it isℝ-convex.Used in #29258