OAI/Analysis/MatrixSigning/Optimization/EliminationWitnessHeight.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W17.CommonHeight line 14
2. theorem OAI.KS.W17.CommonHeight.mono line 18
3. theorem OAI.KS.W17.CommonHeight.parts_bound line 24
4. theorem OAI.KS.W17.commonHeight_single line 36
5. theorem OAI.KS.W17.CommonHeight.cons_zero line 44
6. theorem OAI.KS.W17.schurWitnessLift_eq_prependLinear line 53
7. theorem OAI.KS.W17.DenseEliminationCall.lift_coefficient_parts line 69
8. theorem OAI.KS.W17.CommonHeight.schurWitnessLift line 85
9. def OAI.KS.W17.witnessHeightBudget line 95
10. theorem OAI.KS.W17.DenseEliminationCall.dimension_le line 98
11. theorem OAI.KS.W17.denseNegativeWitness_commonHeight line 104
12. theorem OAI.KS.W17.denseNegativeWitness_output_parts line 177