OAI/Combinatorics/Progressions/Sampling/MixedOutputGrid.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.norm_masked_density_sum_sub_le line 15
  2. def OAI.Erdos3.gridDensityTest line 31
  3. theorem OAI.Erdos3.gridDensityTest_l1_bound line 36
  4. theorem OAI.Erdos3.gridDensityTest_error line 55
  5. theorem OAI.Erdos3.frozen_gridDensityTest_error line 79
  6. theorem OAI.Erdos3.sigmaAxisCoordinates_norm line 119
  7. theorem OAI.Erdos3.sigmaAxisCoordinates_lipschitz line 129
  8. theorem OAI.Erdos3.grouped_gridDensityTest_error line 135
  9. theorem OAI.Erdos3.sliced_gridDensityTest_error line 170
  10. theorem OAI.Erdos3.partial_gridDensityTest_error line 196
  11. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_lipschitz line 225
  12. theorem OAI.Erdos3.gridDensityTest_mean line 236
  13. theorem OAI.Erdos3.partial_gridDensityTest_error_ae line 262
  14. theorem OAI.Erdos3.finiteSource_gridDensityTest_error line 306
  15. theorem OAI.Erdos3.partial_gridDensityTest_family_error_ae line 346
  16. theorem OAI.Erdos3.image_comparison_on_output_grid line 390
  17. theorem OAI.Erdos3.partial_image_comparison_on_output_grid line 420
  18. theorem OAI.Erdos3.mixed_output_grid_error line 457