OAI/Geometry/Convex/GeneralMahler/MatrixBox.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GeneralMahler.specBox line 12
2. lemma OAI.GeneralMahler.op_scalar line 15
3. lemma OAI.GeneralMahler.form_scalar line 19
4. lemma OAI.GeneralMahler.scalar_le' line 22
5. lemma OAI.GeneralMahler.mem_box_form line 26
6. lemma OAI.GeneralMahler.specBox_compact line 34
7. lemma OAI.GeneralMahler.specBox_convex line 54
8. lemma OAI.GeneralMahler.specBox_nonempty line 72
9. def OAI.GeneralMahler.clip line 75
10. lemma OAI.GeneralMahler.cont_clip line 77
11. lemma OAI.GeneralMahler.clip_mem line 80
12. lemma OAI.GeneralMahler.clip_eq line 89

    Source documentation

    If the projection update B ↦ clip(B+M) is fixed and neither kind of extreme eigenvector with wrong outward sign exists, then no clipping occurs and M=0.

    lemma clip_eq {a b:ℝ} (hab:a ≤ b) {B M:Mat m}
        (he : clip a b (B+M)=B) (h : (B+M).IsHermitian)
        (h₁ : ∀ v : Rn m, ‖v‖=1 → op B v=a • v → 0 ≤ ⟪v,op M v⟫)
        (h₂ : ∀ v : Rn m, ‖v‖=1 → op B v=b • v → ⟪v,op M v⟫ ≤ 0) : M=0 := by
    …

    Mentions: OAI.GeneralMahler.Mat, OAI.GeneralMahler.clip, OAI.GeneralMahler.Rn, OAI.GeneralMahler.op

13. lemma OAI.GeneralMahler.form_posDef line 125