OAI/Computability/MinUncut/Estimates/LiftedVectors.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncut.GaussianBudget.Coordinates line 14
2. def OAI.MinUncut.GaussianBudget.liftVector line 16
3. lemma OAI.MinUncut.GaussianBudget.liftVector_norm_sq line 21
4. lemma OAI.MinUncut.GaussianBudget.liftVector_base_norm line 28
5. lemma OAI.MinUncut.GaussianBudget.liftVector_norm_pos line 35
6. lemma OAI.MinUncut.GaussianBudget.liftVector_perturb_sq line 42
7. lemma OAI.MinUncut.GaussianBudget.liftVector_perturb_le line 50
8. lemma OAI.MinUncut.GaussianBudget.delta_distance_le line 57
9. lemma OAI.MinUncut.GaussianBudget.liftVector_distance_sq line 66
10. lemma OAI.MinUncut.GaussianBudget.liftVector_distance_le line 75
11. lemma OAI.MinUncut.GaussianBudget.lift_sign_first line 86
12. lemma OAI.MinUncut.GaussianBudget.lift_sign_second line 95