OAI/Combinatorics/Progressions/Estimates/SelectedCoefficientEvaluation.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.splitFreeColumns line 16
  2. theorem OAI.Erdos3.splitFreeColumns_apply line 22
  3. def OAI.Erdos3.splitFreeProfile line 26
  4. theorem OAI.Erdos3.splitFreeProfile_continuous line 31
  5. theorem OAI.Erdos3.splitFreeProfile_nonneg line 38
  6. theorem OAI.Erdos3.splitFreeProfile_zero_outside line 42
  7. theorem OAI.Erdos3.splitFreeProfile_slice_integrable line 64
  8. theorem OAI.Erdos3.normalizedIntegerColumns_entry line 101
  9. theorem OAI.Erdos3.normalizedIntegerColumns_fromCols line 105
  10. theorem OAI.Erdos3.matrixSupCLM_fromCols line 113
  11. theorem OAI.Erdos3.normalizedIntegerColumns_split line 120
  12. theorem OAI.Erdos3.splitFreeCoordinates_norm_le line 139
  13. theorem OAI.Erdos3.splitFreeProfile_lipschitz line 150
  14. theorem OAI.Erdos3.normalizedIntegerColumns_entry_div line 196
  15. theorem OAI.Erdos3.normalizedIntegerColumns_entry_bound line 204
  16. theorem OAI.Erdos3.normalizedIntegerColumns_norm_bound line 213
  17. theorem OAI.Erdos3.normalizedIntegerColumns_displacement line 221
  18. def OAI.Erdos3.smoothSplitProfile line 246
  19. theorem OAI.Erdos3.smoothSplitProfile_join line 250
  20. theorem OAI.Erdos3.smoothSplitProfile_contDiff line 255
  21. theorem OAI.Erdos3.smoothSplitProfile_range line 260
  22. theorem OAI.Erdos3.smoothSplitProfile_norm_le line 266
  23. theorem OAI.Erdos3.sumElim_norm line 271
  24. theorem OAI.Erdos3.smoothSplitProfile_zero_outside line 275
  25. theorem OAI.Erdos3.smoothSplitProfile_integral line 280
  26. theorem OAI.Erdos3.smoothSplitProfile_lipschitz line 286
  27. theorem OAI.Erdos3.splitFreeProfile_smooth line 301
  28. def OAI.Erdos3.selectedFreeFirstEquiv line 324
  29. def OAI.Erdos3.selectedCoefficientEquiv line 328
  30. theorem OAI.Erdos3.selectedCoefficientEquiv_apply line 333
  31. theorem OAI.Erdos3.selectedCoefficientEquiv_norm line 338
  32. theorem OAI.Erdos3.selectedCoefficientEquiv_lipschitz line 345
  33. def OAI.Erdos3.selectedCoefficientProfile line 357
  34. theorem OAI.Erdos3.selectedCoefficientProfile_nonneg line 361
  35. theorem OAI.Erdos3.selectedCoefficientProfile_norm_le line 365
  36. theorem OAI.Erdos3.selectedCoefficientProfile_lipschitz line 369
  37. theorem OAI.Erdos3.selectedCoefficientProfile_zero_outside line 374
  38. theorem OAI.Erdos3.selectedCoefficientProfile_integral line 381
  39. theorem OAI.Erdos3.selectedCoefficientEquiv_on_selected line 405
  40. theorem OAI.Erdos3.selectedCoefficientEquiv_on_unselected line 412
  41. theorem OAI.Erdos3.selectedCoefficientEquiv_eq_of_coordinates line 419