OAI/Combinatorics/Progressions/Linear/WeightedParameterPatchRankPadding.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.localTentKernel line 11
  2. theorem OAI.Erdos3.localTentKernel_ge_half line 42
  3. theorem OAI.Erdos3.localTentKernel_support line 49
  4. theorem OAI.Erdos3.WeightedParameterSlots.placementSubstitution_degree line 73
  5. def OAI.Erdos3.WeightedParameterSlots.placeCenter line 90
  6. theorem OAI.Erdos3.WeightedParameterSlots.placeCenter_degree line 94
  7. theorem OAI.Erdos3.WeightedParameterSlots.placeCenter_eval line 100
  8. def OAI.Erdos3.WeightedParameterSlots.interleave line 115
  9. theorem OAI.Erdos3.WeightedParameterSlots.interleave_center_left line 129
  10. theorem OAI.Erdos3.WeightedParameterSlots.interleave_center_right line 134
  11. theorem OAI.Erdos3.WeightedParameterSlots.interleave_slots line 139
  12. def OAI.Erdos3.WeightedParameterPatch.product line 163
  13. theorem OAI.Erdos3.WeightedParameterPatch.product_lip line 175
  14. theorem OAI.Erdos3.WeightedParameterPatch.product_value line 178
  15. def OAI.Erdos3.WeightedParameterPatch.castRank line 185
  16. theorem OAI.Erdos3.WeightedParameterPatch.castRank_value line 188
  17. theorem OAI.Erdos3.WeightedParameterPatch.castRank_kernel_lip line 193
  18. def OAI.Erdos3.WeightedParameterPatch.unitRank line 198
  19. theorem OAI.Erdos3.WeightedParameterPatch.unitRank_value line 207
  20. theorem OAI.Erdos3.WeightedParameterPatch.unitRank_lip line 220
  21. def OAI.Erdos3.WeightedParameterPatch.padRank line 224
  22. theorem OAI.Erdos3.WeightedParameterPatch.padRank_value line 229
  23. theorem OAI.Erdos3.WeightedParameterPatch.padRank_lip line 234
  24. theorem OAI.Erdos3.WeightedParameterPatch.padRank_score line 239
  25. def OAI.Erdos3.WeightedParameterPatch.padRankFamily line 246
  26. theorem OAI.Erdos3.WeightedParameterPatch.padRankFamily_value line 251
  27. theorem OAI.Erdos3.WeightedParameterPatch.padRankFamily_lip_bound line 257