OAI/Combinatorics/Progressions/Estimates/WeightedPatchReparam.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.aeval_eq_of_weightedSupport line 11
  2. def OAI.Erdos3.weightedPatchVariableWeight line 26
  3. structure OAI.Erdos3.WeightedParameterSlots line 30
  4. def OAI.Erdos3.WeightedParameterSlots.slots line 38
  5. structure OAI.Erdos3.WeightedParameterPatch line 50
  6. def OAI.Erdos3.WeightedParameterPatch.value line 62
  7. theorem OAI.Erdos3.WeightedParameterPatch.value_mem_Icc line 65
  8. def OAI.Erdos3.PolynomialPatch.weightedParameters line 74
  9. theorem OAI.Erdos3.PolynomialPatch.weightedParameters_value line 83
  10. theorem OAI.Erdos3.SlotInterleaving.sorted_left_lt_right line 99
  11. def OAI.Erdos3.WeightedParameterSlots.insertSubstitution line 113
  12. theorem OAI.Erdos3.WeightedParameterSlots.insertSubstitution_degree line 120
  13. def OAI.Erdos3.WeightedParameterSlots.insertCenter line 137
  14. theorem OAI.Erdos3.WeightedParameterSlots.insertCenter_degree line 142
  15. theorem OAI.Erdos3.WeightedParameterSlots.insertCenter_eval line 148
  16. def OAI.Erdos3.PolynomialSlots.insertLifts line 175
  17. theorem OAI.Erdos3.PolynomialSlots.insertLifts_center_left line 188
  18. theorem OAI.Erdos3.PolynomialSlots.insertLifts_center_right line 197
  19. theorem OAI.Erdos3.PolynomialSlots.insertLifts_residual_left line 207
  20. theorem OAI.Erdos3.PolynomialSlots.insertLifts_residual_right line 214
  21. def OAI.Erdos3.WeightedParameterSlots.parameterSubstitution line 238
  22. theorem OAI.Erdos3.WeightedParameterSlots.parameterSubstitution_degree line 242
  23. def OAI.Erdos3.WeightedParameterSlots.reparam line 254
  24. theorem OAI.Erdos3.WeightedParameterSlots.reparam_slots line 259
  25. def OAI.Erdos3.WeightedParameterPatch.reparam line 278
  26. theorem OAI.Erdos3.WeightedParameterPatch.reparam_lip line 287
  27. theorem OAI.Erdos3.WeightedParameterPatch.reparam_value line 291