OAI/Combinatorics/Progressions/Estimates/JointBooleanGoodWeight.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.weightedCutoff_derivative_pointwise line 17
  2. theorem OAI.Erdos3.compact_weight_directional_integrable line 40
  3. theorem OAI.Erdos3.weightedCutoff_derivative_integral_le line 49
  4. theorem OAI.Erdos3.weightedCutoff_abs_mass_le line 67
  5. def OAI.Erdos3.blockCubeWeight line 96
  6. theorem OAI.Erdos3.blockCubeWeight_contDiff line 100
  7. theorem OAI.Erdos3.blockCubeWeight_compact line 104
  8. theorem OAI.Erdos3.blockCubeWeight_tsupport line 109
  9. theorem OAI.Erdos3.blockCubeWeight_integral line 114
  10. theorem OAI.Erdos3.blockCubeWeight_abs_integral line 120
  11. theorem OAI.Erdos3.blockCubeWeight_coordinate_fderiv line 125
  12. theorem OAI.Erdos3.blockCubeWeight_coordinate_integral line 137
  13. theorem OAI.Erdos3.blockCubeWeight_derivative_sum line 146
  14. def OAI.Erdos3.blockCubeMeasure line 163
  15. instance OAI.Erdos3.blockCubeMeasure_probability line 167
  16. theorem OAI.Erdos3.blockCubeMeasure_integral line 173
  17. theorem OAI.Erdos3.blockCubeMeasure_real_apply line 179
  18. theorem OAI.Erdos3.blockCubeFlatten_box line 187
  19. theorem OAI.Erdos3.blockCubeWeight_box line 192
  20. theorem OAI.Erdos3.blockCubeWeight_integral_test line 211
  21. def OAI.Erdos3.booleanCubeDeterminant line 232
  22. theorem OAI.Erdos3.booleanCubeDeterminant_contDiff line 239
  23. theorem OAI.Erdos3.booleanCubeDeterminant_fderiv_norm_le line 246
  24. theorem OAI.Erdos3.booleanCubeDeterminant_sublevel_probability line 270
  25. def OAI.Erdos3.blockCubeScale line 290
  26. theorem OAI.Erdos3.blockCubeScale_measurable line 294
  27. def OAI.Erdos3.scaledBlockCubeMeasure line 298
  28. theorem OAI.Erdos3.scaledBlockCubeMeasure_eq_map line 303
  29. theorem OAI.Erdos3.scaledBlockCubeMeasure_probability line 314
  30. def OAI.Erdos3.scalarCubeGoodWeight line 331
  31. theorem OAI.Erdos3.scalarCubeGoodWeight_spec line 336
  32. theorem OAI.Erdos3.scalarCubeGoodWeight_integral_test line 360
  33. theorem OAI.Erdos3.scalarCubeGoodWeight_mass_lower line 370
  34. theorem OAI.Erdos3.restrictBlockParameters_measurable line 406
  35. theorem OAI.Erdos3.restrictBlockParameters_cube_measurePreserving line 411
  36. theorem OAI.Erdos3.booleanMinorDeterminant_restrict line 436
  37. theorem OAI.Erdos3.booleanMinorDeterminant_sublevel_marginal line 445
  38. theorem OAI.Erdos3.scalarCubeGoodWeight_directional_le line 470
  39. theorem OAI.Erdos3.scalarCubeGoodWeight_derivative_budget line 495
  40. def OAI.Erdos3.booleanCubeGoodWeight line 537
  41. theorem OAI.Erdos3.booleanCubeGoodWeight_spec line 546
  42. theorem OAI.Erdos3.booleanCubeGoodWeight_mass_lower line 575
  43. def OAI.Erdos3.jointBooleanGoodWeight line 609
  44. theorem OAI.Erdos3.jointBooleanGoodWeight_spec line 616