Peierls and Klein inequalities

TheoremConvex differentiable functions lie above their tangent lines#✓fully proved

The first-order (tangent-line) characterization of a convex differentiable function: the graph lies above every tangent line.

theorem add_deriv_mul_sub_le_of_convexOn {f : ℝ → ℝ} {s : Set ℝ} {x y : ℝ} (hf : ConvexOn ℝ s f)
    (hf' : DifferentiableAt ℝ f x) (hx : x ∈ s) (hy : y ∈ s) :
    f x + deriv f x * (y - x) ≤ f y

Used by 1

Used byKlein's inequality

TheoremPeierls' inequality#✓fully proved

The diagonal of a self-adjoint operator in any orthonormal basis is majorized by its eigenvalues, as measured by any convex function.

theorem peierls_inequality {n : ℕ} (hn : Module.finrank ℂ E = n)
    {T : E →ₗ[ℂ] E} (hT : T.IsSymmetric)
    {f : ℝ → ℝ} {s : Set ℝ} (hf : ConvexOn ℝ s f)
    (hμ : ∀ j, hT.eigenvalues hn j ∈ s)
    (b : OrthonormalBasis (Fin n) ℂ E) :
    ∑ i, f (RCLike.re (inner (𝕜 := ℂ) (b i) (T (b i))))
      ≤ ∑ j, f (hT.eigenvalues hn j)

Uses 1 · Used by 2

Proof usesSchur's theorem on diagonals of self-adjoint operators

Used byKlein's inequality · Peierls' inequality for the exponential

TheoremKlein's inequality#✓fully proved

Klein's inequality (sum form): for a convex function f differentiable at the eigenvalues of S, the tangent-line sum at the eigenvalues of S evaluated on the diagonal of T is at most the sum of f over the eigenvalues of T.

theorem klein_inequality {n : ℕ} (hn : Module.finrank ℂ E = n)
    {T S : E →ₗ[ℂ] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric)
    {f : ℝ → ℝ} {s : Set ℝ} (hf : ConvexOn ℝ s f)
    (hf' : ∀ i, DifferentiableAt ℝ f (hS.eigenvalues hn i))
    (hμT : ∀ j, hT.eigenvalues hn j ∈ s)
    (hμS : ∀ j, hS.eigenvalues hn j ∈ s)
    (b : OrthonormalBasis (Fin n) ℂ E)
    (hd : ∀ i, RCLike.re (inner (𝕜 := ℂ) (b i) (T (b i))) ∈ s) :
    ∑ i, (f (hS.eigenvalues hn i) + deriv f (hS.eigenvalues hn i) *
        (RCLike.re (inner (𝕜 := ℂ) (b i) (T (b i))) - hS.eigenvalues hn i))
      ≤ ∑ j, f (hT.eigenvalues hn j)

Uses 2 · Used by 2

Proof usesConvex differentiable functions lie above their tangent lines · Peierls' inequality

Used byEntropy tangent bound in an arbitrary orthonormal basis · Klein's inequality for the square function

TheoremPeierls' inequality for the exponential#✓fully proved

Peierls' inequality for the exponential function.

theorem peierls_exp {n : ℕ} (hn : Module.finrank ℂ E = n)
    {T : E →ₗ[ℂ] E} (hT : T.IsSymmetric)
    (b : OrthonormalBasis (Fin n) ℂ E) :
    ∑ i, Real.exp (RCLike.re (inner (𝕜 := ℂ) (b i) (T (b i))))
      ≤ ∑ j, Real.exp (hT.eigenvalues hn j)

Uses 1

Proof usesPeierls' inequality

TheoremKlein's inequality for the square function#✓fully proved

Klein's inequality for f x = x ^ 2.

theorem klein_sq {n : ℕ} (hn : Module.finrank ℂ E = n)
    {T S : E →ₗ[ℂ] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric)
    (b : OrthonormalBasis (Fin n) ℂ E) :
    ∑ i, ((hS.eigenvalues hn i) ^ 2 + 2 * hS.eigenvalues hn i *
        (RCLike.re (inner (𝕜 := ℂ) (b i) (T (b i))) - hS.eigenvalues hn i))
      ≤ ∑ j, (hT.eigenvalues hn j) ^ 2

Uses 1

Proof usesKlein's inequality

TheoremEigenvalues of a positive semidefinite operator are nonnegative#✓fully proved

Eigenvalues of a positive semidefinite symmetric operator are nonnegative: an eigenvalue is the Rayleigh quotient at a unit eigenvector.

theorem eigenvalues_nonneg_of_forall_nonneg_inner {n : ℕ} (hn : Module.finrank ℂ E = n)
    {T : E →ₗ[ℂ] E} (hT : T.IsSymmetric)
    (hTpos : ∀ x, 0 ≤ RCLike.re (inner (𝕜 := ℂ) x (T x))) (j : Fin n) :
    0 ≤ hT.eigenvalues hn j

Used by 1

Used byEntropy tangent bound in an arbitrary orthonormal basis

TheoremEigenvalues of a positive definite operator are positive#✓fully proved

Eigenvalues of a positive definite symmetric operator are positive.

theorem eigenvalues_pos_of_forall_pos_inner {n : ℕ} (hn : Module.finrank ℂ E = n)
    {T : E →ₗ[ℂ] E} (hT : T.IsSymmetric)
    (hTpos : ∀ x, x ≠ 0 → 0 < RCLike.re (inner (𝕜 := ℂ) x (T x))) (j : Fin n) :
    0 < hT.eigenvalues hn j

Used by 1

Used byEntropy tangent bound in an arbitrary orthonormal basis

TheoremEntropy tangent bound in an arbitrary orthonormal basis#✓fully proved

The entropy tangent bound in an arbitrary orthonormal basis. Its diagonal entries need not align with the eigenvalues of S; klein_entropy supplies the aligned quantum-relative-entropy form.

theorem klein_entropy_tangent {n : ℕ} (hn : Module.finrank ℂ E = n)
    {T S : E →ₗ[ℂ] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric)
    (hTpos : ∀ x, 0 ≤ RCLike.re (inner (𝕜 := ℂ) x (T x)))
    (hSpos : ∀ x, x ≠ 0 → 0 < RCLike.re (inner (𝕜 := ℂ) x (S x)))
    (b : OrthonormalBasis (Fin n) ℂ E) :
    ∑ i, (hS.eigenvalues hn i * Real.log (hS.eigenvalues hn i) +
        (Real.log (hS.eigenvalues hn i) + 1) *
        (RCLike.re (inner (𝕜 := ℂ) (b i) (T (b i))) - hS.eigenvalues hn i))
      ≤ ∑ j, hT.eigenvalues hn j * Real.log (hT.eigenvalues hn j)

Uses 3 · Used by 1

Proof usesEigenvalues of a positive semidefinite operator are nonnegative · Eigenvalues of a positive definite operator are positive · Klein's inequality

Used byKlein's entropy inequality

TheoremKlein's entropy inequality#✓fully proved

Klein's entropy inequality in the eigenbasis of S. The eigenvalue at index i is paired with its eigenvector, so this is the quantum-relative-entropy form up to the trace terms. In particular, its tangent correction vanishes when T = S.

theorem klein_entropy {n : ℕ} (hn : Module.finrank ℂ E = n)
    {T S : E →ₗ[ℂ] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric)
    (hTpos : ∀ x, 0 ≤ RCLike.re (inner (𝕜 := ℂ) x (T x)))
    (hSpos : ∀ x, x ≠ 0 → 0 < RCLike.re (inner (𝕜 := ℂ) x (S x))) :
    ∑ i, (hS.eigenvalues hn i * Real.log (hS.eigenvalues hn i) +
        (Real.log (hS.eigenvalues hn i) + 1) *
        (RCLike.re (inner (𝕜 := ℂ) (hS.eigenvectorBasis hn i)
          (T (hS.eigenvectorBasis hn i))) - hS.eigenvalues hn i))
      ≤ ∑ j, hT.eigenvalues hn j * Real.log (hT.eigenvalues hn j)

Uses 1

Proof usesEntropy tangent bound in an arbitrary orthonormal basis

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.