OAI/Combinatorics/HoneycombChords/MatrixPencils.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Congruence normal forms and Schur bounds for positive real matrix pencils.

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hermitian_det_shift line 11
  2. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_gram_pencil_real_factorization line 29
  3. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_pencil_normal_form line 68
  4. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.affineSchur line 117

    Source documentation

    The affine oblique Schur complement after diagonalizing the shared positive symmetric pencil.

    noncomputable def affineSchur {n : ℕ} (e a b c d : Fin n → ℝ) (D E u : ℝ) : ℝ :=
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.D

  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.affineSchur_decomposition line 119
  6. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.affineSchur_ratio_bounds line 133

    Source documentation

    A positive constant, nonnegative linear term and positive Stieltjes residues give exactly the bounded-factor comparison needed in the first oblique chain.

    theorem affineSchur_ratio_bounds {n : ℕ} (e a b c d : Fin n → ℝ) (D E : ℝ)
    (he : ∀ i,0<e i) (hres : ∀ i,0 ≤ (a i-e i*b i)*(c i-e i*d i))
    (hzero : 0<affineSchur e a b c d D E 0) (hlin : 0 ≤ E-∑ i,b i*d i)
    {u v : ℝ} (hu : 0<u) (huv : u ≤ v) :
    u/v ≤ affineSchur e a b c d D E u/affineSchur e a b c d D E v ∧
      affineSchur e a b c d D E u/affineSchur e a b c d D E v ≤ 1 := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.D, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.affineSchur

  7. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.blockBorder line 184
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.blockBorder_det line 187
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.blockBorder_diagonal_det line 202
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.blockBorder_affine_schur line 217
  11. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendCorner line 229

    Source documentation

    Extension of the corner change of basis to the actual bordered pencil.

    noncomputable def extendCorner {n : ℕ} (P : Matrix (Fin n) (Fin n) ℝ) :
    Matrix (Fin n ⊕ Fin 1) (Fin n ⊕ Fin 1) ℝ := Matrix.fromBlocks P 0 0 1
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendCorner_det line 231
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.blockBorder_congruence line 233
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.blockBorder_congruence_det line 240
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_pencil_normal_form_pos line 253
  16. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalRow line 262
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalRow_apply line 264
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalRow_ne_zero line 266
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalRow_kernel line 274
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalRow_dot line 290
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.vecMul_normalRow line 293
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalForm_add line 307
  23. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.border_pencil_ratio line 314
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finBorder_submatrix line 388
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finBorder_det line 405
  26. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.lastPairing line 417
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.lastPairing_dot line 419
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.lastPairing_sub_smul line 424
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fin_pencil_ratio line 427
  30. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.bordered_det_nonzero line 472