139 lines
3.9 KiB
Julia
139 lines
3.9 KiB
Julia
function augment_columns!(Q::AbstractMatrix)
|
|
for c in eachcol(Q)
|
|
c .-= sum(c) ./ length(c)
|
|
end
|
|
return Q
|
|
end
|
|
|
|
function __sos_via_sqr!(
|
|
res::StarAlgebras.AlgebraElement,
|
|
P::AbstractMatrix;
|
|
augmented::Bool
|
|
)
|
|
StarAlgebras.zero!(res)
|
|
A = parent(res)
|
|
b = basis(A)
|
|
@assert size(A.mstructure) == size(P)
|
|
e = b[one(b[1])]
|
|
|
|
for i in axes(A.mstructure, 1)
|
|
x = StarAlgebras._istwisted(A.mstructure) ? StarAlgebras.star(b[i]) : b[i]
|
|
for j in axes(A.mstructure, 2)
|
|
p = P[i, j]
|
|
xy = b[A.mstructure[i, j]]
|
|
# either result += P[x,y]*(x*y)
|
|
res[xy] += p
|
|
if augmented
|
|
# or result += P[x,y]*(1-x)*(1-y) == P[x,y]*(2-x-y+xy)
|
|
y = b[j]
|
|
res[e] += p
|
|
res[x] -= p
|
|
res[y] -= p
|
|
end
|
|
end
|
|
end
|
|
|
|
return res
|
|
end
|
|
|
|
function __sos_via_cnstr!(res::StarAlgebras.AlgebraElement, Q²::AbstractMatrix, cnstrs)
|
|
StarAlgebras.zero!(res)
|
|
for (g, A_g) in cnstrs
|
|
res[g] = dot(A_g, Q²)
|
|
end
|
|
return res
|
|
end
|
|
|
|
function compute_sos(A::StarAlgebras.StarAlgebra, Q::AbstractMatrix; augmented::Bool)
|
|
Q² = Q' * Q
|
|
res = StarAlgebras.AlgebraElement(zeros(eltype(Q²), length(basis(A))), A)
|
|
res = __sos_via_sqr!(res, Q², augmented=augmented)
|
|
return res
|
|
end
|
|
|
|
function sufficient_λ(residual::StarAlgebras.AlgebraElement, λ; halfradius)
|
|
L1_norm = norm(residual, 1)
|
|
suff_λ = λ - 2.0^(2ceil(log2(halfradius))) * L1_norm
|
|
|
|
eq_sign = let T = eltype(residual)
|
|
if T <: Interval
|
|
"∈"
|
|
elseif T <: Union{Rational,Integer}
|
|
"="
|
|
else # if T <: AbstractFloat
|
|
"≈"
|
|
end
|
|
end
|
|
|
|
info_strs = [
|
|
"Numerical metrics of the obtained SOS:",
|
|
"ɛ(elt - λu - ∑ξᵢ*ξᵢ) $eq_sign $(StarAlgebras.aug(residual))",
|
|
"‖elt - λu - ∑ξᵢ*ξᵢ‖₁ $eq_sign $(L1_norm)",
|
|
" λ $eq_sign $suff_λ",
|
|
]
|
|
@info join(info_strs, "\n")
|
|
|
|
return suff_λ
|
|
end
|
|
|
|
function sufficient_λ(
|
|
elt::StarAlgebras.AlgebraElement,
|
|
order_unit::StarAlgebras.AlgebraElement,
|
|
λ,
|
|
sos::StarAlgebras.AlgebraElement;
|
|
halfradius
|
|
)
|
|
|
|
@assert parent(elt) === parent(order_unit) == parent(sos)
|
|
residual = (elt - λ * order_unit) - sos
|
|
|
|
return sufficient_λ(residual, λ; halfradius=halfradius)
|
|
end
|
|
|
|
function certify_solution(
|
|
elt::StarAlgebras.AlgebraElement,
|
|
orderunit::StarAlgebras.AlgebraElement,
|
|
λ,
|
|
Q::AbstractMatrix{<:AbstractFloat};
|
|
halfradius,
|
|
augmented=iszero(StarAlgebras.aug(elt)) && iszero(StarAlgebras.aug(orderunit))
|
|
)
|
|
|
|
should_we_augment = !augmented && StarAlgebras.aug(elt) == StarAlgebras.aug(orderunit) == 0
|
|
|
|
Q = should_we_augment ? augment_columns!(Q) : Q
|
|
@time sos = compute_sos(parent(elt), Q, augmented=augmented)
|
|
|
|
@info "Checking in $(eltype(sos)) arithmetic with" λ
|
|
|
|
λ_flpoint = sufficient_λ(elt, orderunit, λ, sos, halfradius=halfradius)
|
|
|
|
if λ_flpoint ≤ 0
|
|
return false, λ_flpoint
|
|
end
|
|
|
|
λ_int = @interval(λ)
|
|
Q_int = [@interval(q) for q in Q]
|
|
|
|
check, sos_int = @time if should_we_augment
|
|
@info("Projecting columns of Q to the augmentation ideal...")
|
|
Q_int = augment_columns!(Q_int)
|
|
@info "Checking that sum of every column contains 0.0..."
|
|
check_augmented = all(0 ∈ sum(c) for c in eachcol(Q_int))
|
|
check_augmented || @error(
|
|
"Augmentation failed! The following numbers are not certified!"
|
|
)
|
|
sos_int = compute_sos(parent(elt), Q_int; augmented=augmented)
|
|
check_augmented, sos_int
|
|
else
|
|
true, compute_sos(parent(elt), Q_int, augmented=augmented)
|
|
end
|
|
|
|
@info "Checking in $(eltype(sos_int)) arithmetic with" λ_int
|
|
|
|
λ_certified =
|
|
sufficient_λ(elt, orderunit, λ_int, sos_int, halfradius=halfradius)
|
|
|
|
return check && inf(λ_certified) > 0.0, inf(λ_certified)
|
|
end
|