OAI/Combinatorics/Progressions/Polynomial/PolynomialParameterContinuity.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.mvPolynomial_support_card_le_fintype line 20
  2. theorem OAI.Erdos3.mvPolynomial_unit_box_bound line 34
  3. theorem OAI.Erdos3.mvPolynomial_pderiv_degreeOf_le line 47
  4. theorem OAI.Erdos3.mvPolynomial_pderiv_coeff_bound line 60
  5. theorem OAI.Erdos3.mvPolynomial_pderiv_unit_box_bound line 74
  6. theorem OAI.Erdos3.mvPolynomial_second_pderiv_unit_box_bound line 83
  7. theorem OAI.Erdos3.polynomialOperator_fderiv_entry line 100
  8. theorem OAI.Erdos3.polynomialOperator_fderiv_norm_le line 117
  9. theorem OAI.Erdos3.mvPolynomial_mod_single_support line 141
  10. theorem OAI.Erdos3.mvPolynomial_eval_update_of_support_zero line 148
  11. theorem OAI.Erdos3.mvPolynomial_eval_sub_zero_coordinate line 162
  12. theorem OAI.Erdos3.mvPolynomial_div_single_degreeOf_le line 174
  13. theorem OAI.Erdos3.mvPolynomial_div_single_coeff_bound line 185
  14. def OAI.Erdos3.polynomialVectorMap line 203
  15. theorem OAI.Erdos3.polynomialVectorMap_contDiff line 207
  16. theorem OAI.Erdos3.polynomialVectorMap_fderiv_entry line 210
  17. theorem OAI.Erdos3.polynomialVectorMap_norm_bound line 220
  18. theorem OAI.Erdos3.polynomialVectorMap_fderiv_bound line 228
  19. theorem OAI.Erdos3.polynomialVectorMap_second_fderiv_bound line 238
  20. def OAI.Erdos3.polynomialBoxLip line 262
  21. theorem OAI.Erdos3.polynomialVectorMap_lipschitzOn_box line 265
  22. abbrev OAI.Erdos3.PolynomialParameter line 294
  23. def OAI.Erdos3.polynomialParameterPoint line 296
  24. def OAI.Erdos3.polynomialParameterInjection line 302
  25. theorem OAI.Erdos3.polynomialParameterPoint_affine line 309
  26. theorem OAI.Erdos3.polynomialParameterInjection_norm_le line 315
  27. theorem OAI.Erdos3.polynomialParameterPoint_unit_box line 327
  28. def OAI.Erdos3.parameterPolynomialMap line 335
  29. theorem OAI.Erdos3.parameterPolynomialMap_contDiff line 339
  30. theorem OAI.Erdos3.parameterPolynomialMap_sub_zero line 348
  31. theorem OAI.Erdos3.realPolynomialMass_pderiv_degreeOf line 372
  32. theorem OAI.Erdos3.polynomialVectorMap_mass_c2_bounds line 388
  33. def OAI.Erdos3.polynomialMassC2Budget line 421
  34. theorem OAI.Erdos3.polynomialMassC2Budget_nonneg line 424
  35. theorem OAI.Erdos3.polynomialMassC2Budget_dominates line 427
  36. theorem OAI.Erdos3.polynomialMassC2Budget_le_exp line 441
  37. theorem OAI.Erdos3.matrixSupCLM_sub line 467
  38. def OAI.Erdos3.polynomialColumns line 472
  39. theorem OAI.Erdos3.polynomialColumns_lipschitzOn_box line 476
  40. def OAI.Erdos3.centeredPolynomialVariable line 506
  41. def OAI.Erdos3.centeredPolynomial line 512
  42. theorem OAI.Erdos3.centeredPolynomialVariable_eval line 516
  43. theorem OAI.Erdos3.centeredPolynomial_eval line 522
  44. theorem OAI.Erdos3.centeredPolynomial_eval_zero line 535
  45. theorem OAI.Erdos3.centeredPolynomialVariable_mass_le line 541
  46. theorem OAI.Erdos3.centeredPolynomialVariable_totalDegree_le line 552
  47. theorem OAI.Erdos3.centeredPolynomial_mass_le line 562
  48. theorem OAI.Erdos3.centeredPolynomial_totalDegree_le line 569
  49. theorem OAI.Erdos3.polynomialParameterPoint_continuous line 582
  50. theorem OAI.Erdos3.parameterPolynomialMap_joint_continuous line 591