OAI/Analysis/MatrixSigning/Potential/VarianceH.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.State.varianceH line 19
2. lemma OAI.CurrentKS.State.varianceH_psd line 21
3. lemma OAI.CurrentKS.State.trace_each_le_one line 24
4. lemma OAI.CurrentKS.State.varianceH_le_one line 29
5. lemma OAI.CurrentKS.State.varianceH_pos line 38
6. lemma OAI.CurrentKS.State.S_bounds_hundred line 53
7. lemma OAI.CurrentKS.State.feasible_norm_le_objective line 64
8. def OAI.CurrentKS.State.jointObjective line 92
9. lemma OAI.CurrentKS.State.cube_zero line 95
10. lemma OAI.CurrentKS.State.S_zero line 97
11. lemma OAI.CurrentKS.State.initial_scalar_point line 99