OAI/Analysis/AffineBernstein/RadialAdjugate.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.adjugate_block_radial line 14
2. def OAI.AffineBernstein.radialShear line 48
3. lemma OAI.AffineBernstein.radialShear_det line 51
4. lemma OAI.AffineBernstein.radialShear_last line 56
5. lemma OAI.AffineBernstein.mul_radialShear_left line 60
6. lemma OAI.AffineBernstein.transpose_radialShear_mul_left line 65
7. lemma OAI.AffineBernstein.mul_radialShear_last line 71
8. lemma OAI.AffineBernstein.radialShear_conjugate line 76
9. theorem OAI.AffineBernstein.radial_adjugate line 103

   Source comment

   A symmetric form with radial null vector has its full adjugate equal to its transverse principal minor times the radial outer product. This includes all empty transverse blocks and needs no invertibility of the full matrix.

   theorem radial_adjugate {A : Matrix (ι ⊕ Unit) (ι ⊕ Unit) ℝ}
       (hA : A.IsSymm) (e : ι ⊕ Unit → ℝ) (he : e (Sum.inr ()) = 1)
       (hz : A *ᵥ e = 0) (i j : ι ⊕ Unit) :
       A.adjugate i j = (A.submatrix Sum.inl Sum.inl).det * e i * e j := by
   …

10. lemma OAI.AffineBernstein.radial_adjugate_trace line 132