Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

#605 - Function for checking boundedness #956

Merged
merged 6 commits into from
Dec 27, 2018
Merged

#605 - Function for checking boundedness #956

merged 6 commits into from
Dec 27, 2018

Conversation

schillic
Copy link
Member

@schillic schillic commented Dec 24, 2018

Closes #605.

This PR adds isbounded(::Set).
There is a default implementation (that uses isbounded_unit_dims), but only the implementations of ExponentialProjectionMap, HPolyhedron, Intersection(Array), and LinearMap may fall back to that default if some sufficient/necessary checks fail. For the other set types, the check is trivial (or recursive for operations).

Some tests do not work before merging #940, so they currently throw an error. Whatever gets merged last has to update those tests.

@mforets: Can you please check the implementations for LinearMap, ExponentialMap, and ExponentialProjectionMap if they are correct or if they can be improved?

@schillic schillic requested a review from mforets December 24, 2018 10:42
@mforets
Copy link
Member

mforets commented Dec 27, 2018

May i suggest to rename isbounded_unit_dims -> isbounded_unit_dimensions ?

(Comparing to constrained_dimensions.)

src/LazySet.jl Outdated Show resolved Hide resolved
src/ExponentialMap.jl Outdated Show resolved Hide resolved
src/LazySet.jl Outdated Show resolved Hide resolved
Copy link
Member

@mforets mforets left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM 👏 👏 👏

@schillic
Copy link
Member Author

schillic commented Dec 27, 2018

Do you agree that for ExponentialMap the condition isbounded(em.X) is sufficient and necessary?
If X is unbounded in only one dimension, can it happen that a matrix exponential is zero in that dimension? I was thinking that in 1D this cannot happen (e^x > 0 for all x), but I am lost in higher dimensions.

mforets and others added 2 commits December 27, 2018 19:55
Co-Authored-By: schillic <schillic@informatik.uni-freiburg.de>
@schillic schillic merged commit 3493f51 into master Dec 27, 2018
@schillic schillic deleted the schillic/605 branch December 27, 2018 20:12
@mforets
Copy link
Member

mforets commented Dec 27, 2018

Do you agree that for ExponentialMap the condition isbounded(em.X) is sufficient and necessary?

Yes, it follows from the invertibility of M := exp(A) for any matrix A, see the properties of the matrix exponential.

Indeed, suppose by contradiction that the set Y = MX is bounded but the set X is unbounded. Then there exists a sequence of elements of X, x^j for j=1,2,... such that ||x^j|| -> oo. Let y^j = Mx^j for all j. Then since M is invertible, x^j = inv(M) * y^j and thus ||x^j|| <= ||inv(M)|| ||y^j||, and the right-hand side is bounded by hypothesis, thus the sequence ||x^j|| is bounded, a contradiction.

We can use this condition in LinearMap and ExponentialProjectionMap as well.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants