Shared rank-one matrix corrections

Certificate families use these signed corrections to dominate their off-diagonal residuals.

noncomputable def LeanPool.Besicovitch.pairSign (r : ℝ) : ℝ

Sign used for the off-diagonal entry of a rank-one correction.

Equations

• LeanPool.Besicovitch.pairSign r = if 0 ≤ r then 1 else -1

noncomputable def LeanPool.Besicovitch.pairVector {ι : Type u_1} [DecidableEq ι] (r : ℝ) (i j : ι) : ι → ℝ

The two-coordinate vector for a signed matrix correction.

Equations

• LeanPool.Besicovitch.pairVector r i j k = if k = i then 1 else if k = j then LeanPool.Besicovitch.pairSign r else 0

noncomputable def LeanPool.Besicovitch.pairCorrection {ι : Type u_1} [DecidableEq ι] (r : ℝ) (i j : ι) : Matrix ι ι ℝ

A positive semidefinite rank-one correction.

Equations

• LeanPool.Besicovitch.pairCorrection r i j = |r| • Matrix.vecMulVec (LeanPool.Besicovitch.pairVector r i j) (LeanPool.Besicovitch.pairVector r i j)

theorem LeanPool.Besicovitch.pairCorrection_posSemidef {ι : Type u_1} [DecidableEq ι] [Finite ι] (r : ℝ) (i j : ι) : (pairCorrection r i j).PosSemidef

The correction matrix is positive semidefinite.

noncomputable def LeanPool.Besicovitch.fivePairCompletion (base : Matrix (Fin 5) (Fin 5) ℝ) (residual : Fin 5 → Fin 5 → ℝ) : Matrix (Fin 5) (Fin 5) ℝ

Complete a five-vector certificate with positive two-coordinate corrections.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Besicovitch.fivePairCompletion_posSemidef {base : Matrix (Fin 5) (Fin 5) ℝ} (hbase : base.PosSemidef) (residual : Fin 5 → Fin 5 → ℝ) : (fivePairCompletion base residual).PosSemidef

Pairwise completion preserves positive semidefiniteness.

theorem LeanPool.Besicovitch.abs_mul_pairSign (r : ℝ) : |r| * pairSign r = r

The signed absolute value recovers the original residual.

@[simp]

theorem LeanPool.Besicovitch.pairCorrection_apply_pair {ι : Type u_1} [DecidableEq ι] (r : ℝ) {i j : ι} (hij : i ≠ j) : pairCorrection r i j i j = r

The corrected off-diagonal entry.

@[simp]

theorem LeanPool.Besicovitch.pairCorrection_apply_pair_rev {ι : Type u_1} [DecidableEq ι] (r : ℝ) {i j : ι} (hij : i ≠ j) : pairCorrection r i j j i = r

The transposed corrected off-diagonal entry.

@[simp]

theorem LeanPool.Besicovitch.pairCorrection_apply_left_left {ι : Type u_1} [DecidableEq ι] (r : ℝ) {i j : ι} : pairCorrection r i j i i = |r|

The first diagonal entry is the residual magnitude.

@[simp]

theorem LeanPool.Besicovitch.pairCorrection_apply_right_right {ι : Type u_1} [DecidableEq ι] (r : ℝ) {i j : ι} (hij : i ≠ j) : pairCorrection r i j j j = |r|

The second diagonal entry is the residual magnitude.

@[simp]

theorem LeanPool.Besicovitch.pairCorrection_apply_zero_left {ι : Type u_1} [DecidableEq ι] (r : ℝ) {i j k l : ι} (hki : k ≠ i) (hkj : k ≠ j) : pairCorrection r i j k l = 0

Other rows of the correction vanish.

@[simp]

theorem LeanPool.Besicovitch.pairCorrection_apply_zero_right {ι : Type u_1} [DecidableEq ι] (r : ℝ) {i j k l : ι} (hli : l ≠ i) (hlj : l ≠ j) : pairCorrection r i j k l = 0

Other columns of the correction vanish.

theorem LeanPool.Besicovitch.matrix_inner_sum_nonneg {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {matrix : Matrix ι ι ℝ} (hmatrix : matrix.PosSemidef) (v : ι → E) : 0 ≤ ∑ i : ι, ∑ j : ι, matrix i j * inner ℝ (v i) (v j)

A positive semidefinite matrix has a nonnegative sum against vector inner products.