OAI/Combinatorics/Progressions/Polynomial/PolynomialPatchProductBudget.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.earlierSlot line 12
  2. def OAI.Erdos3.patchVariableWeight line 15
  3. structure OAI.Erdos3.PolynomialSlots line 18
  4. def OAI.Erdos3.PolynomialSlots.slots line 26
  5. def OAI.Erdos3.PolynomialSlots.prefixSubstitution line 35
  6. theorem OAI.Erdos3.PolynomialSlots.prefixSubstitution_degree line 41
  7. def OAI.Erdos3.PolynomialSlots.freezePrefix line 63
  8. theorem OAI.Erdos3.PolynomialSlots.freezePrefix_center_eval line 71
  9. structure OAI.Erdos3.PolynomialPatch line 98
  10. def OAI.Erdos3.PolynomialPatch.value line 110
  11. theorem OAI.Erdos3.PolynomialPatch.value_mem_Icc line 113
  12. def OAI.Erdos3.PolynomialPatch.freezePrefix line 116
  13. def OAI.Erdos3.PolynomialSlots.ofCoordinates line 144
  14. theorem OAI.Erdos3.PolynomialSlots.ofCoordinates_center line 150
  15. def OAI.Erdos3.PolynomialPatch.ofCoordinates line 162
  16. theorem OAI.Erdos3.PolynomialPatch.ofCoordinates_residual line 173
  17. theorem OAI.Erdos3.PolynomialSlots.slots_freezePrefix line 196
  18. theorem OAI.Erdos3.PolynomialPatch.value_rank_zero line 211
  19. theorem OAI.Erdos3.PolynomialPatch.freezePrefix_value line 218
  20. theorem OAI.Erdos3.PolynomialPatch.freezePrefix_error line 228
  21. def OAI.Erdos3.shiftedParameterPolynomials line 244
  22. theorem OAI.Erdos3.shiftedParameterPolynomials_degree line 248
  23. theorem OAI.Erdos3.shiftedParameterPolynomials_eval line 258
  24. theorem OAI.Erdos3.PolynomialPatch.exists_freeze_affine_layer line 268
  25. def OAI.Erdos3.PolynomialSlots.parameterSubstitution line 321
  26. theorem OAI.Erdos3.PolynomialSlots.parameterSubstitution_degree line 325
  27. def OAI.Erdos3.PolynomialSlots.reparam line 339
  28. theorem OAI.Erdos3.PolynomialSlots.reparam_slots line 344
  29. def OAI.Erdos3.PolynomialPatch.reparam line 363
  30. theorem OAI.Erdos3.PolynomialPatch.reparam_value line 372
  31. def OAI.Erdos3.PolynomialPatch.affineLineParameters line 379
  32. theorem OAI.Erdos3.PolynomialPatch.affineLineParameters_degree line 382
  33. def OAI.Erdos3.PolynomialPatch.onAffineLine line 387
  34. theorem OAI.Erdos3.PolynomialPatch.onAffineLine_value line 390
  35. def OAI.Erdos3.PolynomialPatch.shiftedKernel line 410
  36. theorem OAI.Erdos3.PolynomialPatch.shiftedKernel_residual line 422
  37. theorem OAI.Erdos3.PolynomialPatch.shiftedKernel_value line 430
  38. def OAI.Erdos3.PolynomialSlots.placementSubstitution line 451
  39. theorem OAI.Erdos3.PolynomialSlots.placementSubstitution_degree line 456
  40. def OAI.Erdos3.PolynomialSlots.placeCenter line 473
  41. theorem OAI.Erdos3.PolynomialSlots.placeCenter_degree line 477
  42. theorem OAI.Erdos3.PolynomialSlots.placeCenter_eval line 483
  43. def OAI.Erdos3.PolynomialSlots.interleave line 498
  44. theorem OAI.Erdos3.PolynomialSlots.interleave_center_left line 512
  45. theorem OAI.Erdos3.PolynomialSlots.interleave_center_right line 517
  46. theorem OAI.Erdos3.PolynomialSlots.interleave_slots line 522
  47. def OAI.Erdos3.PolynomialPatch.constant line 554
  48. theorem OAI.Erdos3.PolynomialPatch.constant_value line 569
  49. theorem OAI.Erdos3.PolynomialPatch.constant_lip line 574
  50. def OAI.Erdos3.PolynomialPatch.product line 577
  51. theorem OAI.Erdos3.PolynomialPatch.product_lip line 589
  52. theorem OAI.Erdos3.PolynomialPatch.product_value line 592
  53. theorem OAI.Erdos3.PolynomialPatch.exists_finset_product line 599
  54. theorem OAI.Erdos3.PolynomialPatch.exists_fin_product line 618
  55. theorem OAI.Erdos3.PolynomialPatch.exists_background_product line 626
  56. theorem OAI.Erdos3.PolynomialPatch.exists_reparam_product line 649
  57. theorem OAI.Erdos3.PolynomialPatch.product_lip_exp_le line 659
  58. theorem OAI.Erdos3.PolynomialPatch.exists_fin_product_budget line 672
  59. theorem OAI.Erdos3.PolynomialPatch.exists_background_product_budget line 691