OAI/Combinatorics/Progressions/Estimates/ProductCutoffLipschitz.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteRectangleRefinement line 13
  2. theorem OAI.Erdos3.finiteRectangleRefinement_val line 24
  3. theorem OAI.Erdos3.expect_finiteRectangleRefinement line 29
  4. def OAI.Erdos3.progressionCellCorner line 46
  5. theorem OAI.Erdos3.finiteRectangleRefinement_affine line 50
  6. theorem OAI.Erdos3.progressionCell_dist_corner line 59
  7. theorem OAI.Erdos3.norm_weighted_cell_replacement line 83
  8. theorem OAI.Erdos3.exists_cell_of_weighted_bias line 105
  9. theorem OAI.Erdos3.exists_cell_of_lipschitz_weight line 142
  10. def OAI.Erdos3.scalarCubeCutoffLipschitzConstant line 168
  11. theorem OAI.Erdos3.scalarCubeBoundaryCutoff_lipschitz line 172
  12. theorem OAI.Erdos3.scalarCubeFace_lipschitz line 185
  13. theorem OAI.Erdos3.scalarCubeBoundaryCutoff_near_support line 194
  14. def OAI.Erdos3.scalarCubeCutoffWeight line 222
  15. theorem OAI.Erdos3.scalarCubeCutoffWeight_contDiff line 225
  16. theorem OAI.Erdos3.scalarCubeCutoffWeight_compact line 229
  17. theorem OAI.Erdos3.scalarCubeCutoffWeight_tsupport_subset line 233
  18. theorem OAI.Erdos3.scalarCubeCutoffWeight_integral line 237
  19. theorem OAI.Erdos3.scalarCubeCutoffWeight_abs_mass_le_one line 249
  20. theorem OAI.Erdos3.scalarCubeCutoffWeight_derivative_integral line 261
  21. theorem OAI.Erdos3.scalarCubeMean_derivative_le line 280
  22. theorem OAI.Erdos3.scalarCubeCutoffWeight_derivative_le line 297
  23. theorem OAI.Erdos3.scalarCubeCutoffWeight_coordinate_sum_le line 304
  24. theorem OAI.Erdos3.exists_interior_progression_cell line 325
  25. theorem OAI.Erdos3.scalarCube_cutoff_safe line 354
  26. theorem OAI.Erdos3.scalarCubeBoundaryCutoff_tsupport_domain line 376
  27. def OAI.Erdos3.scalarCubeBoundaryWeight line 384
  28. theorem OAI.Erdos3.scalarCubeBoundaryWeight_spec line 388
  29. theorem OAI.Erdos3.scalarCubeBoundaryWeight_mass_lower line 405
  30. theorem OAI.Erdos3.scalarCubeBoundaryWeight_derivative_budget line 421
  31. def OAI.Erdos3.scalarCubeProductWeight line 444
  32. theorem OAI.Erdos3.scalarCubeProductWeight_spec line 448
  33. theorem OAI.Erdos3.scalarCubeProductWeight_mass_lower line 463
  34. theorem OAI.Erdos3.scalarCubeProductWeight_derivative_budget line 477
  35. def OAI.Erdos3.scalarCubeProductCutoff line 503
  36. theorem OAI.Erdos3.scalarCubeProductCutoff_range line 508
  37. theorem OAI.Erdos3.scalarCubeProductCutoff_smooth line 513
  38. theorem OAI.Erdos3.scalarCubeProductCutoff_tsupport line 518
  39. theorem OAI.Erdos3.scalarCubeProductWeight_eq_mul line 524
  40. theorem OAI.Erdos3.scalarCubeProductWeight_integral_test line 532
  41. theorem OAI.Erdos3.scalarCubeProductCutoff_mass_loss line 546
  42. theorem OAI.Erdos3.tensor_cutoff_lipschitz line 569
  43. theorem OAI.Erdos3.scalarCubeProductCutoff_lipschitz line 589
  44. theorem OAI.Erdos3.scalarCubeProductCutoff_near_support line 597