OAI/Combinatorics/Progressions/Lattices/AffineModeratePlateauModel.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteResidueModeModel line 16
  2. theorem OAI.Erdos3.finiteResidueModeModel_norm line 19
  3. theorem OAI.Erdos3.finiteResidueModeModel_lipschitz line 28
  4. theorem OAI.Erdos3.finiteResidueModeModel_residue_card line 52
  5. def OAI.Erdos3.weightedAffineModerateIntegerBlock line 75
  6. theorem OAI.Erdos3.weightedAffineModerateGridCoefficient_eq_image line 82
  7. def OAI.Erdos3.weightedAffineModerateIntegerJetSum line 100
  8. theorem OAI.Erdos3.weightedAffineModerateIntegerJetSum_coefficient line 108
  9. theorem OAI.Erdos3.containedProgressionCoordinate_mem line 131
  10. theorem OAI.Erdos3.NormalizedScalarCubeSource.source_cube line 139
  11. theorem OAI.Erdos3.containedProgressionCoordinate_bound line 150
  12. theorem OAI.Erdos3.weightedAffineModerateIntegerJetSum_box_bound line 158
  13. theorem OAI.Erdos3.weightedAffineModerateProductSource_jet_sum_law line 226
  14. theorem OAI.Erdos3.weightedAffineModerateProductSource_affine_law line 246
  15. theorem OAI.Erdos3.affineWeightedCubeIntegerSum_box_bound line 278
  16. def OAI.Erdos3.weightedAffineModerateGridApproximation line 330
  17. theorem OAI.Erdos3.weightedAffineModerateGridDensity_fourier line 340
  18. theorem OAI.Erdos3.weightedAffineModerateGridDensity_error_of_tail line 356
  19. def OAI.Erdos3.weightedAffineModeratePlateauApproximation line 395
  20. theorem OAI.Erdos3.weightedAffineModeratePlateauApproximation_split_periods line 400
  21. theorem OAI.Erdos3.weightedAffineModeratePlateauMixture_expansion line 417
  22. def OAI.Erdos3.weightedAffinePlateauModeCoefficient line 441
  23. theorem OAI.Erdos3.weightedAffinePlateauModeCoefficient_sum_le line 447
  24. def OAI.Erdos3.weightedAffinePlateauModeModel line 460
  25. theorem OAI.Erdos3.weightedAffinePlateauModeModel_grid_value line 469