Skip to content

Latest commit

 

History

History
127 lines (107 loc) · 7.03 KB

README.md

File metadata and controls

127 lines (107 loc) · 7.03 KB

Sum-of-Squares proofs for the n-cycle

A logarithmic Sobolev inequality for the simple random walk on the n-cycle has the form

The best possible constant α for which the above holds is called the logarithmic Sobolev constant of the n-cycle. In order to find certifiable lower bounds on the log-Sobolev constant, we consider a stronger inequality, based on the Taylor series of (1+t)^2 log(1+t), which only involves polynomials. This directory contains exact sum-of-squares proofs that this stronger inequality holds with α = (1 - cos(2pi/n))/2, for modest values of n. This α is in fact the best possible constant, since it happens to be half of the spectral gap of this chain, which is known to upper bound the log-Sobolev constant. For more details, please refer to our paper

Sum-of-Squares proofs of logarithmic Sobolev inequalities on finite Markov chains (Oisín Faust and Hamza Fawzi, arXiv:2101.04988).

Here is a brief description of the files in this directory:

  • generate_proofs.jl is a Julia script which sets up and solves a sum-of-squares relaxation, and outputs a proof.
  • cycle_basis.jl contains some code used by generate_proofs.jl (in particular, it defines the polynomial basis we will use).
  • verify_cycle_proof.sage is a Sage script which verifies our claim, taking a number of proof files as input.

Some of this functionality is described in more depth below.

Verifying the proofs

This requires a working installation of SageMath, version >= 9.2.

The script verify_cycle_proof.sage should be run with an argument n, for which there exists a proof file proofs/sos_proof_{n}.sage (this path is relative to the directory verify_cycle_proof.sage). These files contain the data needed to obtain a sum-of-squares proof, in the form of an LDL^t decomposition and a polynomial basis.

$ sage verify_cycle_proof.sage 7
n = 7: Success - proof is valid

In this example n=7. The script accepts multiple arguments:

$ sage verify_cycle_proof.sage 7 9 11
n = 7: Success - proof is valid
n = 9: Success - proof is valid
n = 11: Success - proof is valid

When n is large, e.g. 17, 19, 21, expect this verification to take up many minutes or even several hours of CPU time.

Proofs may be obtained using the script generate_proofs.jl (as explained in Generating the proofs). Alternatively, a zipped proofs folder containing some precomputed sos_proof_{n}.sage files is available for download from here.

The verification process

Given an argument n, verify_cycle_proof.sage proceeds as follows.

  • K= is defined as the smallest number field containing the rational numbers as well as the real number theta = 2cos(2pi/n). This field is represented in Sage as the quotient of the space of rational polynomials Q[theta] modulo the ideal generated by the minimal polynomial of 2cos(2pi/n), together with an embedding to the reals that sends theta to the value 2cos(2pi/n) (which it is capable of computing to arbitrary precision when deciding inequalities).
  • Then the ring of polynomials in n variables over K, R = K[x_0, x_1, ..., x_{n-1}], is defined.
  • The 4 lines of Sage code in sos_proof_n.sage are executed, to load the proof. The file sos_proof_n.sage has the form
D = [...]
L = [[...], [...], ..., [...]]
B = [...]
h = ...

The idea is that D is a vector of positive(!) numbers in K, L is a (lower triangular) matrix of numbers in K, B is a vector of polynomials in R, and h is a single polynomial in K.

  • It is verified that the objects D, L, B, and h are indeed of the type claimed above.
  • The sum of squares polynomial sos is defined as n * B^t * L * diagm(D) * L^t * B (the n is just a scalar factor, here for convenience). Calculating this polynomial is what makes up the bulk of the processing for this procedure.
  • It is verified that sos is equal to the polynomial

    ,

    where is the Taylor series of 2t^2log(1+t) truncated to degree 5.

Generating the proofs

Note - installing required packages

The following assumes that certain necessary dependencies (a subset of those listed in examples/Project.toml) have already been added manually to your default Julia environment. Alternatively, you can download all dependencies into the examples environment in one step as follows:

$ julia --project=EXAMPLES_PATH -e "using Pkg; Pkg.instantiate()"

where EXAMPLES_PATH is a path to the LogSobolevRelaxations/examples folder. If you choose to do this, command line calls to Julia in the rest of this section should use the --project flag as follows:

$ julia --project=EXAMPLES_PATH ...

The script generate_proofs.jl takes one or more arguments:

$ julia generate_proofs.jl 7
Starting n = 7...
Finished n = 7!
$ julia generate_proofs.jl 7 9 11
Starting n = 7...
Finished n = 7!
Starting n = 9...
Finished n = 9!
Starting n = 11...
Finished n = 11!

For n = 5, 7, 9, 11, 13, 15, this should take on the order of minutes. For larger n = 17, 19, 21, ..., the process may take multiple hours, depending on your system, and will need a significant amount of RAM (~16GB for n=21).

The script includes the file cycle_basis.jl, which defines a module called OddCycleUtils.

The module OddCycleUtils

This module provides the following functionality:

  • A type to represent an element of the number field . The implementation is just a wrapper for an Antic nf_elem object accessed via Nemo.
    struct RealCyclotomicFieldElem{N} <: Real
        v::Nemo.nf_elem
    end
  • A function to round a relaxation containing an aprroximate floating-point solution onto the affine space of exact solutions to the linear constraints of its SDP. Our implementation of this step involves finding the RREF of the system.
round_sol!(relaxation::LSRelaxation{RealCyclotomicFieldElem{N}}) where N
  • A function to check whether a matrix of number field elements is positive semidefinite. Under the hood, this function calls Arb to carry out a Cholesky decomposition in interval arithmetic. This is not to be considered in any way part of a proof; it is only used to allow generate_proofs.jl to abort early if a Gram matrix has a negative eigenvalue.
check_pos_def(Q::Matrix{RealCyclotomicFieldElem{N}}) where N
  • A function which will return a carefully chosen symmetry-adapted polynomial basis. The return type will be a Vector of LogSobolevRelaxations.GramBasis{RealCyclotomicFieldElem{N}} objects. Each GramBasis corresponds to a block of the full block-diagonal Gram matrix. They also have a nontrivial sparsity pattern. For more details, please refer to our paper, and to the code itself.
get_cycle_basis(x::Vector{DynamicPolynomials.PolyVar{true}})