GramSchur.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite Gram row-sum bound

This is the linear algebra step in the exceptional-moment argument: a symmetric absolute Gram kernel bounds its quadratic form by its largest row sum. Both variables are retained in the estimate.

theorem OAI.CubicFirstMoment.nonnegative_schur_bound line 18

theorem OAI.CubicFirstMoment.complex_schur_bound line 58

Source documentation

The complex Gram quadratic form is bounded using only absolute row sums and Hermitian symmetry of their norms.

theorem complex_schur_bound {ι : Type*} (P : Finset ι) (z : ι → ℂ)
    (K : ι → ι → ℂ) (R : ℝ)
    (hsym : ∀ p ∈ P, ∀ q ∈ P, ‖K p q‖ = ‖K q p‖)
    (hrow : ∀ p ∈ P, ∑ q ∈ P, ‖K p q‖ ≤ R) :
    ‖∑ p ∈ P, ∑ q ∈ P, z p * star (z q) * K p q‖ ≤
      R * ∑ p ∈ P, ‖z p‖^2 := by
…