OAI/AlgebraicGeometry/Stability/NumericalWalls.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Numerical character, discriminant and fixed-branch wall-transport inequalities.

  1. structure OAI.PrescribedCharges.Numerical.Character line 11
  2. def OAI.PrescribedCharges.Numerical.Character.twist line 19
  3. def OAI.PrescribedCharges.Numerical.Character.discr line 25
  4. def OAI.PrescribedCharges.Numerical.Character.numerator line 27
  5. def OAI.PrescribedCharges.Numerical.Character.defect line 29
  6. theorem OAI.PrescribedCharges.Numerical.Character.twist_zero line 31
  7. theorem OAI.PrescribedCharges.Numerical.Character.twist_twist line 34
  8. theorem OAI.PrescribedCharges.Numerical.Character.discr_twist line 38
  9. theorem OAI.PrescribedCharges.Numerical.Character.discr_at_zero line 43
  10. theorem OAI.PrescribedCharges.Numerical.Character.rank_bound line 50
  11. theorem OAI.PrescribedCharges.Numerical.Character.hasDerivAt_twist_z line 58
  12. def OAI.PrescribedCharges.Numerical.comparison line 70
  13. def OAI.PrescribedCharges.Numerical.excess line 72
  14. theorem OAI.PrescribedCharges.Numerical.comparison_eq_discr_div line 74
  15. theorem OAI.PrescribedCharges.Numerical.comparison_factorization line 80
  16. theorem OAI.PrescribedCharges.Numerical.comparison_sub_excess line 86
  17. theorem OAI.PrescribedCharges.Numerical.two_excess_sub_comparison line 92
  18. theorem OAI.PrescribedCharges.Numerical.comparison_bounds line 99
  19. theorem OAI.PrescribedCharges.Numerical.excess_estimate_to_comparison line 115
  20. theorem OAI.PrescribedCharges.Numerical.comparison_add_gap line 120
  21. theorem OAI.PrescribedCharges.Numerical.comparison_superadditive line 129
  22. theorem OAI.PrescribedCharges.Numerical.sum_comparison_le line 139
  23. theorem OAI.PrescribedCharges.Numerical.exists_violating_factor line 157
  24. theorem OAI.PrescribedCharges.Numerical.discriminant_split_two line 168
  25. theorem OAI.PrescribedCharges.Numerical.cross_term_nonneg line 173
  26. theorem OAI.PrescribedCharges.Numerical.cross_term_zero line 184
  27. theorem OAI.PrescribedCharges.Numerical.discriminant_strict_drop line 208
  28. theorem OAI.PrescribedCharges.Numerical.no_infinite_discrete_descent line 217
  29. def OAI.PrescribedCharges.Numerical.Character.branchD line 246
  30. def OAI.PrescribedCharges.Numerical.Character.branchB line 248
  31. def OAI.PrescribedCharges.Numerical.Character.branchDefect line 250
  32. def OAI.PrescribedCharges.Numerical.Character.branchComparison line 253
  33. theorem OAI.PrescribedCharges.Numerical.Character.branch_radicand_pos line 255
  34. theorem OAI.PrescribedCharges.Numerical.Character.branchD_pos line 260
  35. theorem OAI.PrescribedCharges.Numerical.Character.branchD_sq line 264
  36. theorem OAI.PrescribedCharges.Numerical.Character.twist_branchB_d line 268
  37. theorem OAI.PrescribedCharges.Numerical.Character.numerator_branch line 274
  38. theorem OAI.PrescribedCharges.Numerical.Character.branchComparison_nonneg line 287
  39. theorem OAI.PrescribedCharges.Numerical.Character.branch_rate_le line 296
  40. theorem OAI.PrescribedCharges.Numerical.Character.hasDerivAt_branchD line 304
  41. theorem OAI.PrescribedCharges.Numerical.Character.hasDerivAt_branchB line 314
  42. theorem OAI.PrescribedCharges.Numerical.Character.hasDerivAt_branchDefect line 323
  43. theorem OAI.PrescribedCharges.Numerical.Character.hasDerivAt_branchComparison line 339
  44. theorem OAI.PrescribedCharges.Numerical.Character.hasDerivAt_branch_difference line 351
  45. theorem OAI.PrescribedCharges.Numerical.Character.hasDerivAt_defect_rank_zero line 360
  46. theorem OAI.PrescribedCharges.Numerical.Character.hasDerivAt_comparison_rank_zero line 368
  47. def OAI.PrescribedCharges.Numerical.belowCoefficient line 374
  48. def OAI.PrescribedCharges.Numerical.tailCoefficient line 376
  49. def OAI.PrescribedCharges.Numerical.aboveCoefficient line 378
  50. theorem OAI.PrescribedCharges.Numerical.hasDerivAt_belowCoefficient line 380
  51. theorem OAI.PrescribedCharges.Numerical.hasDerivAt_tailCoefficient line 387
  52. theorem OAI.PrescribedCharges.Numerical.hasDerivAt_aboveCoefficient line 394
  53. theorem OAI.PrescribedCharges.Numerical.belowCoefficient_nonneg line 399
  54. theorem OAI.PrescribedCharges.Numerical.below_derivative_nonneg line 405
  55. theorem OAI.PrescribedCharges.Numerical.tail_derivative_nonpos line 412
  56. theorem OAI.PrescribedCharges.Numerical.above_derivative_nonpos line 425
  57. theorem OAI.PrescribedCharges.Numerical.endpoint_le_of_nonneg_derivative line 438
  58. theorem OAI.PrescribedCharges.Numerical.endpoint_le_of_nonpos_derivative line 448
  59. theorem OAI.PrescribedCharges.Numerical.Character.below_endpoint line 460
  60. theorem OAI.PrescribedCharges.Numerical.Character.tail_endpoint line 474
  61. theorem OAI.PrescribedCharges.Numerical.Character.above_endpoint line 489
  62. theorem OAI.PrescribedCharges.Numerical.Character.below_endpoint_rank_zero line 504
  63. theorem OAI.PrescribedCharges.Numerical.Character.tail_endpoint_rank_zero line 510
  64. theorem OAI.PrescribedCharges.Numerical.Character.above_endpoint_rank_zero line 517
  65. def OAI.PrescribedCharges.Numerical.tailThreshold line 535
  66. def OAI.PrescribedCharges.Numerical.globalCorrection line 537
  67. theorem OAI.PrescribedCharges.Numerical.tailThreshold_pos line 540
  68. theorem OAI.PrescribedCharges.Numerical.apex_le_tailThreshold line 545
  69. theorem OAI.PrescribedCharges.Numerical.globalCorrection_nonneg line 549
  70. theorem OAI.PrescribedCharges.Numerical.belowCoefficient_le_globalCorrection line 553
  71. theorem OAI.PrescribedCharges.Numerical.aboveCoefficient_le_globalCorrection line 559
  72. theorem OAI.PrescribedCharges.Numerical.tailCoefficient_at_apex_gt line 565
  73. theorem OAI.PrescribedCharges.Numerical.exists_nonnegative_rational_ge line 572
  74. theorem OAI.PrescribedCharges.Numerical.unnormalize_iff line 578
  75. theorem OAI.PrescribedCharges.Numerical.rescale_correction_iff line 582
  76. theorem OAI.PrescribedCharges.Numerical.rescale_threshold_iff line 589
  77. theorem OAI.PrescribedCharges.Numerical.numerical_conditions_insufficient line 593