OAI/RingTheory/Multiplicity/NumericalSupport.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.Numerical.H line 8
2. lemma OAI.Lech.Numerical.H_monic line 11
3. lemma OAI.Lech.Numerical.H_natDegree line 14
4. lemma OAI.Lech.Numerical.H_eval_zero_at line 19
5. lemma OAI.Lech.Numerical.H_eval_zero line 24
6. lemma OAI.Lech.Numerical.derivative_root_exists line 30
7. def OAI.Lech.Numerical.ρ line 45
8. lemma OAI.Lech.Numerical.ρ_spec line 48
9. lemma OAI.Lech.Numerical.ρ_strictAnti line 53
10. lemma OAI.Lech.Numerical.derivative_factorization line 60
11. def OAI.Lech.Numerical.roundedRoot line 79
12. lemma OAI.Lech.Numerical.roundedRoot_error line 82
13. lemma OAI.Lech.Numerical.roundedRoot_positions line 90
14. def OAI.Lech.Numerical.P line 110
15. lemma OAI.Lech.Numerical.derivative_eval line 112
16. lemma OAI.Lech.Numerical.integral_P line 117
17. lemma OAI.Lech.Numerical.abs_prod_sub_prod_le line 139
18. lemma OAI.Lech.Numerical.abs_ρ_le line 174
19. lemma OAI.Lech.Numerical.abs_mem_interval line 180
20. def OAI.Lech.Numerical.bound line 185
21. lemma OAI.Lech.Numerical.bound_nonneg line 187
22. lemma OAI.Lech.Numerical.P_lipschitz line 189
23. def OAI.Lech.Numerical.Ps line 208
24. lemma OAI.Lech.Numerical.scaledRoot_error line 211
25. lemma OAI.Lech.Numerical.Ps_error line 219
26. lemma OAI.Lech.Numerical.riemann_error line 253
27. def OAI.Lech.Numerical.normalizedLayer line 296
28. lemma OAI.Lech.Numerical.layer_error line 299
29. def OAI.Lech.Numerical.layer line 361
30. lemma OAI.Lech.Numerical.layer_eq line 365
31. lemma OAI.Lech.Numerical.normalized_layer_error line 382
32. theorem OAI.Lech.Numerical.root_layer_estimates line 391
33. lemma OAI.Lech.Numerical.weighted_error_bound line 412
34. lemma OAI.Lech.Numerical.layer_zero line 424
35. theorem OAI.Lech.Numerical.from_sum_estimate line 428
36. def OAI.Lech.Numerical.GoodRoots line 494
37. theorem OAI.Lech.Numerical.uniform_from_sum_estimate line 500