OAI/Analysis/MatrixSigning/Potential/ParameterCube.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.State.ParameterCube line 15
2. def OAI.CurrentKS.State.etaTheta line 17
3. lemma OAI.CurrentKS.State.etaTheta_apply line 20
4. lemma OAI.CurrentKS.State.etaTheta_psi line 24
5. lemma OAI.CurrentKS.State.parameterCube_psi line 27
6. lemma OAI.CurrentKS.State.etaTheta_positive line 30
7. lemma OAI.CurrentKS.State.etaTheta_one_bound line 36
8. lemma OAI.CurrentKS.State.sandwich_mono_order line 48
9. lemma OAI.CurrentKS.State.etaTheta_difference_le line 53
10. lemma OAI.CurrentKS.State.etaTheta_shift_feasible line 81
11. lemma OAI.CurrentKS.State.objective_shift line 97
12. lemma OAI.CurrentKS.State.etaTheta_minimizer line 100
13. lemma OAI.CurrentKS.State.etaTheta_value_le line 127
14. lemma OAI.CurrentKS.State.sum_parameter_difference_le line 156
15. lemma OAI.CurrentKS.State.etaTheta_value_perturbation line 163