Complementary positive-semidefinite block forms

import Mathlib

set_option autoImplicit false

/-! Quadratic-form consequences of one complementary pair of PSD blocks. -/

namespace Conway99Formal.TwoSidedSchur

open Matrix

variable {g e : Type*} [Fintype g] [Fintype e]

def normSq (x : g → ℝ) : ℝ := ∑ i, x i * x i

def action (L : Matrix g e ℝ) (y : e → ℝ) : g → ℝ :=
  fun i => ∑ j, L i j * y j

def pairing (L : Matrix g e ℝ) (x : g → ℝ) (y : e → ℝ) : ℝ :=
  ∑ i, x i * action L y i

/-- The two complementary PSD block inequalities, evaluated on `(x,t*y)`.
The same `L`, `a`, and `q` occur in both blocks. -/
structure ComplementaryPSD (L : Matrix g e ℝ) where
  a : (g → ℝ) → ℝ
  q : (e → ℝ) → ℝ
  first : ∀ (x : g → ℝ) (y : e → ℝ) (t : ℝ),
    0 ≤ a x + t ^ 2 * q y - 2 * t * pairing L x y
  second : ∀ (x : g → ℝ) (y : e → ℝ) (t : ℝ),
    0 ≤ 28 * normSq x - a x + t ^ 2 * (28 * normSq y - q y) +
      2 * t * pairing L x y



















private def pairVector [DecidableEq e] (j k : e) (t : ℝ) : e → ℝ :=
  fun z => if z = j then t else if z = k then 1 else 0




section LiteralBlocks

variable {h : Type*} [Fintype h] [DecidableEq g] [DecidableEq h]

/-- The first full block, using one common checkerboard Gram, owner matrix,
and curvature matrix. -/
def firstBlock (K : Matrix (g ⊕ h) (g ⊕ h) ℝ)
    (W : Matrix (g ⊕ h) h ℝ) (R : Matrix h h ℝ) :
    Matrix ((g ⊕ h) ⊕ h) ((g ⊕ h) ⊕ h) ℝ :=
  Matrix.fromBlocks ((40 : ℝ) • 1 - K) (-W) (-Wᵀ) R

/-- The complementary block from exactly the same `K`, `W`, and `R`. -/
def secondBlock (K : Matrix (g ⊕ h) (g ⊕ h) ℝ)
    (W : Matrix (g ⊕ h) h ℝ) (R : Matrix h h ℝ) :
    Matrix ((g ⊕ h) ⊕ h) ((g ⊕ h) ⊕ h) ℝ :=
  Matrix.fromBlocks (K - (12 : ℝ) • 1) W Wᵀ ((28 : ℝ) • 1 - R)
















































































end LiteralBlocks

end Conway99Formal.TwoSidedSchur