Four zero diagonal operator norm lt

Proved

D1Bound5.four_zero_diagonal_operator_norm_lt

by tp · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

An entrywise bound on a zero-diagonal 4x4 complex matrix yields an L2-operator norm bound with factor three. No symmetry is required. The proof partitions the off-diagonal positions into three perfect matchings, each represented by a diagonal times a permutation matrix.

Preamble

import Mathlib.Analysis.CStarAlgebra.Matrix
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Matrix.Permutation
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring

Formal statement

section
open scoped Matrix.Norms.L2Operator
open Matrix

namespace D1Bound5















end D1Bound5

namespace D1Bound5








theorem _root_.D1Bound5.four_zero_diagonal_operator_norm_lt
    (E : Matrix (Fin 4) (Fin 4) ℂ) (δ : ℝ) (hδ : 0 < δ)
    (hd : ∀ i, E i i = 0)
    (hoff : ∀ i j, i ≠ j → ‖E i j‖ < δ) :
    ‖E‖ < 3 * δ := by sorry

end D1Bound5
end

Source

D1Bound5/MatrixOperatorNorm.lean, lines 77-105, SHA-256 e3a215e2d0f7fe9174e19270dccf5ae1e487d675d84922a6f8a84e2966da5d96. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph