[Merged by Bors] - refactor: redefine ProperCone as an abbrev for ClosedSubmodule#25204
[Merged by Bors] - refactor: redefine ProperCone as an abbrev for ClosedSubmodule#25204YaelDillies wants to merge 9 commits intomasterfrom
ProperCone as an abbrev for ClosedSubmodule#25204Conversation
PR summary 8024e6939a
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.Convex.Cone.Basic | 1601 | 1277 | -324 (-20.24%) |
| Mathlib.Analysis.Convex.Cone.InnerDual | 1993 | 1996 | +3 (+0.15%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Analysis.Convex.Cone.Basic |
-324 |
Mathlib.Analysis.Convex.Cone.InnerDual |
3 |
Declarations diff
+ coe_bot
+ instance : Coe (ProperCone R E) (PointedCone R E) := ⟨toPointedCone⟩
+ instance : SetLike (ProperCone R E) E
+ mem_bot
+ mem_toPointedCone
+ pointed_toConvexCone
+ smul_mem
+ toPointedCone_bot
+ toPointedCone_positive
- coe_positive
- instZero
- instance : Coe (ProperCone 𝕜 E) (PointedCone 𝕜 E)
- instance : Inhabited (ProperCone 𝕜 E)
- instance : SetLike (ProperCone 𝕜 E) E
- instance : Zero (ProperCone 𝕜 E)
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 script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
b-mehta
left a comment
There was a problem hiding this comment.
I don't think it's a good idea to change from k to R in this PR, especially since Analysis/Convex/Cone/Basic uses k everywhere, and the second half of this file does too, so this PR creates a weird situation where R is used in some middle chunk. My suggestion is to make that change file-wide (or folder-wide) in a separate PR.
| end T1Space | ||
|
|
||
| /-- The closure of image of a proper cone under a `ℝ`-linear map is a proper cone. We | ||
| use continuous maps here so that the comap of f is also a map between proper cones. -/ |
There was a problem hiding this comment.
If you didn't insist f was continuous, what do you get out instead? I presume just a convex cone or something? (Not an objection, just out of curiosity)
There was a problem hiding this comment.
Just a convex cone, yes, and no galois connection
| /-- The closure of image of a proper cone under a linear map is a proper cone. | ||
|
|
||
| We use continuous maps here to match `ProperCone.comap`. -/ | ||
| abbrev map (f : E →L[R] F) (C : ProperCone R E) : ProperCone R F := | ||
| ClosedSubmodule.map (f.restrictScalars R≥0) C |
There was a problem hiding this comment.
I don't really buy "it matches" as a good enough reason to have the input non-generalised...?
(But "it's how it was before" is a good enough reason, so this is not an objection :) )
There was a problem hiding this comment.
Yeah, just moving this around. I am not convinced myself of the design
|
This pull request has conflicts, please merge |
... and derive the `ProperCone` operations from `ClosedSubmodule` too. Also rename the scalar ring from `𝕜` to `R`. From Toric
53bd221 to
53ad1a7
Compare
The second part of the file has now been deleted (since we don't have Do you still want me to split the variable rename to another PR? |
| theorem mem_comap {f : E →L[ℝ] F} {S : ProperCone ℝ F} {x : E} : x ∈ S.comap f ↔ f x ∈ S := | ||
| Iff.rfl | ||
| @[simp] lemma mem_positive : x ∈ positive R E ↔ 0 ≤ x := .rfl | ||
| @[simp] lemma toPointedCone_positive : (positive R E).toPointedCone = .positive R E := rfl |
There was a problem hiding this comment.
Do you want the one about the coercion to ConvexCone too? or does that come for free in simp?
There was a problem hiding this comment.
Yes, comes for free in simp since the coercion is obtained by transitivity
|
Thanks! bors merge |
…25204) ... and derive the `ProperCone` operations from `ClosedSubmodule` too. Also rename the scalar ring from `𝕜` to `R`. From Toric
|
Pull request successfully merged into master. Build succeeded: |
ProperCone as an abbrev for ClosedSubmoduleProperCone as an abbrev for ClosedSubmodule
* master: (447 commits) chore(Data/Set): move very basic lemmas earlier (leanprover-community#25707) feat: preserve draft status when migrating PRs to fork (leanprover-community#25777) chore(Data/Set/Basic): deprecate lemmas that abuse the `Set α := α → Prop` defeq (leanprover-community#25669) refactor: redefine `ProperCone` as an `abbrev` for `ClosedSubmodule` (leanprover-community#25204) feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (leanprover-community#25564) fix: outdated docstring (leanprover-community#25717) feat(MeasureTheory): convolution of measures with densities (leanprover-community#25718) feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right (leanprover-community#25604) feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948) feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (leanprover-community#25333) fix: typo in labels_from_comment.yml (leanprover-community#25727) feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705) feat: check that the mathlib options exist (leanprover-community#25687) feat(Algebra/Group/Even): Add missing lemmas (leanprover-community#20818) refactor: make `Matrix.kroneckerTMulAlgEquiv` heterogeneous (leanprover-community#25693) feat: allow contributors to remove labels with comments (leanprover-community#25723) chore: disable build.yml and bors.yml on forks (leanprover-community#25722) feat: improvements to user_activity_report.py (leanprover-community#25721) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) ...
…eanprover-community#25204) ... and derive the `ProperCone` operations from `ClosedSubmodule` too. Also rename the scalar ring from `𝕜` to `R`. From Toric
…eanprover-community#25204) ... and derive the `ProperCone` operations from `ClosedSubmodule` too. Also rename the scalar ring from `𝕜` to `R`. From Toric
…eanprover-community#25204) ... and derive the `ProperCone` operations from `ClosedSubmodule` too. Also rename the scalar ring from `𝕜` to `R`. From Toric
... and derive the
ProperConeoperations fromClosedSubmoduletoo. Also rename the scalar ring from𝕜toR.From Toric