[Merged by Bors] - feat(linear_algebra/affine_space/ordered): define slope
#4669
Conversation
* `prod.left_cancel_semigroup`; * `prod_right_cancel_semigroup`; * `prod.ordered_cancel_comm_monoid`; * `ordered_comm_group`.
|
@dupuisf could you have a look? |
| @@ -189,44 +189,20 @@ ext' $ preimage_comp.symm | |||
| @[simp] lemma mem_comap {f : E →ₗ[ℝ] F} {S : convex_cone F} {x : E} : | |||
| x ∈ S.comap f ↔ f x ∈ S := iff.rfl | |||
|
|
|||
| -- We use `{ to_semimodule := ‹_›, .. }` to avoid making this definition noncomputable | |||
There was a problem hiding this comment.
This comment seems inscrutable to me.
There was a problem hiding this comment.
How can I improve it? If I write := ordered_semimodule.mk' _, then Lean thinks that the definition is noncomputable. We can avoid this by taking only proof fields from ordered_semimodule.mk' _. I'm not sure that it's worth it because there are no computable (in the sense "useful for computation", not in the sense computable) modules over real anyway.
| def units.smul_perm_hom : units α →* equiv.perm β := | ||
| { to_fun := λ u, ⟨λ x, (u:α) • x, λ x, (↑u⁻¹:α) • x, u.inv_smul_smul, u.smul_inv_smul⟩, | ||
| map_one' := equiv.ext $ one_smul α, | ||
| map_mul' := λ u₁ u₂, equiv.ext $ mul_smul (u₁:α) u₂ } |
There was a problem hiding this comment.
Is this meant to be used directly or only as in the following two lemmas? Should it have some @[simp] ..._apply lemma?
There was a problem hiding this comment.
After pending improvements to @[simps], we'll be able to tell it to use _apply instead of to_fun, and the first person who'll need these simp lemmas will add @[simps]. I don't want to add unused code that will become obsolete in a few days.
| left_inv := inv_smul_smul g, | ||
| right_inv := smul_inv_smul g } | ||
| def to_perm : α →* equiv.perm β := | ||
| units.smul_perm_hom.comp to_units.to_monoid_hom |
There was a problem hiding this comment.
Same question about a potentially missing simp lemma.
PatrickMassot
added
awaiting-author
urkud
added
awaiting-review
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
|
bors merge |
github-actions
bot
added
ready-to-merge
* Review API of `ordered_semimodule`:
- replace `lt_of_smul_lt_smul_of_nonneg` with `lt_of_smul_lt_smul_of_pos`;
it's equivalent but is easier to prove;
- add more lemmas;
- add a constructor for the special case of an ordered semimodule over
a linearly ordered field; in this case it suffices to verify only
`a < b → 0 < c → c • a ≤ c • b`;
- use the new constructor in `analysis/convex/cone`;
* Define `units.smul_perm_hom`, reroute `mul_action.to_perm` through it;
* Add a few more lemmas unfolding `affine_map.line_map` in special cases;
* Define `slope f a b = (b - a)⁻¹ • (f b -ᵥ f a)` and prove a handful
of monotonicity properties.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
slopeslope
ordered_semimodule:lt_of_smul_lt_smul_of_nonnegwithlt_of_smul_lt_smul_of_pos;it's equivalent but is easier to prove;
a linearly ordered field; in this case it suffices to verify only
a < b → 0 < c → c • a ≤ c • b;analysis/convex/cone;units.smul_perm_hom, reroutemul_action.to_permthrough it;affine_map.line_mapin special cases;slope f a b = (b - a)⁻¹ • (f b -ᵥ f a)and prove a handfulof monotonicity properties.
These properties are not yet used in
analysis/convex/basic, mostlyto keep this PR from becoming too large to review.