OAI/Analysis/MatrixSigning/Potential/Drift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Progress.drift line 13
2. lemma OAI.CurrentKS.Progress.drift_cancel line 15
3. lemma OAI.CurrentKS.Progress.drift_abs line 21
4. lemma OAI.CurrentKS.Progress.drift_size line 29
5. lemma OAI.CurrentKS.Progress.drift_penalty_bound line 38
6. lemma OAI.CurrentKS.Progress.weighted_drift_nonpositive line 65
7. lemma OAI.CurrentKS.Progress.penalty_drift_quantitative line 79
8. lemma OAI.CurrentKS.Progress.combine_progress line 98