OAI/Analysis/MatrixSigning/Optimization/RealExtendCube.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.RationalFace.real_extend_cube line 16
2. lemma OAI.CurrentKS.RationalFace.norm_psd_le_trace_h line 24
3. lemma OAI.CurrentKS.RationalFace.norm_atoms_le_one line 31
4. lemma OAI.CurrentKS.RationalFace.fixedPart_norm_le_one line 37
5. lemma OAI.CurrentKS.RationalFace.face_order_bounds line 52
6. lemma OAI.CurrentKS.RationalFace.face_eta_one_bound line 61
7. lemma OAI.CurrentKS.RationalFace.strip_nearby line 72
8. theorem OAI.CurrentKS.RationalFace.face_smooth_and_derivatives line 83