Please have a look into e.g. this [test](https://github.com/kalmarek/PropertyT.jl/blob/master/test/1712.07167.jl#L87) to see how this package can be used to prove Kazdhan Property (T) for a finitely presented group. For an example applications have a look at our papers:
* M. Kaluba and P.W. Nowak _Certifying numerical estimates for spectral gaps_ [1703.09680](https://arxiv.org/abs/1703.09680)
* M. Kaluba, P.W. Nowak and N. Ozawa *$Aut(F₅)$ has property (T)* [1712.07167](https://arxiv.org/abs/1712.07167), and
* M. Kaluba, D. Kielak and P.W. Nowak *On property (T) for $Aut(Fₙ)$ and $SLₙ(Z)$* [1812.03456](https://arxiv.org/abs/1812.03456).
* [`Groups.jl`](https://github.com/kalmarek/Groups.jl) for computations with finitely presented groups,
* [`SymbolicWedderburn.jl`](https://github.com/kalmarek/SymbolicWedderburn.jl) for symmetrizing the sum of squares relaxations of positivity problems,
* [`JuMP.jl`](https://github.com/JuliaOpt/JuMP.jl) for formulating the optimization problems, and
* [`SCS.jl`](https://github.com/JuliaOpt/SCS.jl) wrapper for the [`scs` solver](https://github.com/cvxgrp/scs), or
* [`COSMO.jl`](https://github.com/oxfordcontrol/COSMO.jl) solver to solve the problems.
Certification of the results is done via `ℓ₁`-convexity of the sum-of-squares cone and our knowledge of its interior points. The certified computations use
As proven by N. Ozawa [here](https://arxiv.org/abs/1312.5431) (Main Theorem), property (T) for `SL` is equivalent to a sum of (hermitian) squares decomposition for $\Delta^2 - \lambda\Delta$ for some $\lambda > 0$. Let's find such decomposition using semi-definite optimization:
This problem tries to find maximal `λ` as long as an internal matrix `P` defines a sum of squares decomposition for `Δ² - λΔ` (you may consult the docstring of `sos_problem_primal` for more information).
## Solving the optimization problem
To solve the problem we need a solver/optimizer - a software to numerically find a solution using e.g. iterative procedures. There are two solvers predefined in `test/optimizers.jl`:
*`scs_optimizer` and
*`cosmo_optimizer`.
These are just thin wrappers around `JuMP` (or actually `MathOptInterface`) optimizers.
```julia
julia> include("test/optimizers.jl");
```
Now we have everything what we need to solve the problem!
The solver didn't manage to solve the problem but it got quite close! (duality gap is ~`1.63e-6`). Let's try once again this time warmstarting the solver:
This time solver was successful in reaching the desired accuracy (`1e-9`). Lets query the solution:
```julia
julia> λ = JuMP.value(opt_problem[:λ])
0.28040750495076683
julia> P = JuMP.value.(opt_problem[:P]); size(P)
(121, 121)
julia> Q = real.(sqrt(P));
julia> maximum(abs, Q'*Q - P)
7.951418690144152e-11
```
## Certifying the result
Thus we obtained a matrix `Q` which defines elements `ξᵢ ∈ ℝSL` (coefficents read by columns of `Q`) whose sum of squares is close to `Δ²-λΔ` in `ℓ₁`-norm. Let's check it out.
```julia
julia> sos = PropertyT.compute_sos(RSL, Q, augmented=true);
julia> using LinearAlgebra
julia> norm(Δ²-λ*Δ - sos, 1)
2.948008083982383e-7
```
We'd like to conclude from this that since the norm of the residual is much larger than `λ` we obtain (by `ℓ₁`-convexity of sum of squares cone in `ℝSL`) a proof of the existence of an **exact** sum of squares decomposition of `Δ² - λ₀Δ` for some `λ₀` not far from the numerical `λ` above. To be able to do so we'd need to provide a certified bound on the magnitude of the norm. Here's how to do it in an automated fashion:
```julia
julia> _, λ_cert = PropertyT.certify_solution(Δ², Δ, λ, Q, halfradius=2, augmented=true)
0.070032 seconds (4.11 k allocations: 400.047 KiB)
┌ Info: Checking in Float64 arithmetic with
└ λ = 0.28040750495076683
┌ Info: Numerical metrics of the obtained SOS:
│ ɛ(elt - λu - ∑ξᵢ*ξᵢ) ≈ -3.3119650146808302e-12
│ ‖elt - λu - ∑ξᵢ*ξᵢ‖₁ ≈ 2.948008083982383e-7
└ λ ≈ 0.2804063257475332
5.393452 seconds (15.30 M allocations: 581.181 MiB, 3.08% gc time, 83.70% compilation time)
┌ Info: Checking in IntervalArithmetic.Interval{Float64} arithmetic with
The true returned means that the result is certified to be correct and the value `0.28040632499038354` is the certified lower bound on the spectral gap of `Δ`.
### Lower bound on the Kazhdan constant
Together with estimate for the Kazhdan constant of $(G,S)$:
