OAI/Combinatorics/Progressions/Estimates/NormalizedSampledHistogram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.sampledWeightSum_bounds line 14
  2. theorem OAI.Erdos3.sampledWeightSum_pos line 33
  3. theorem OAI.Erdos3.sampledWeightSum_scale_ratio line 39
  4. theorem OAI.Erdos3.compactProfile_integral_pos line 47
  5. def OAI.Erdos3.sampledWeightMass line 64
  6. def OAI.Erdos3.sampledWeightInterpolant line 67
  7. theorem OAI.Erdos3.sampledWeightMass_sum line 70
  8. theorem OAI.Erdos3.sampledWeightMass_nonneg line 76
  9. theorem OAI.Erdos3.sampledWeightInterpolant_at_lattice line 80
  10. theorem OAI.Erdos3.sampledWeightInterpolant_contDiff line 86
  11. theorem OAI.Erdos3.iteratedDeriv_affine line 92
  12. theorem OAI.Erdos3.sampledWeightInterpolant_deriv line 98
  13. def OAI.Erdos3.normalizedWeightHistogram line 124
  14. theorem OAI.Erdos3.normalizedWeightHistogram_integrable line 127
  15. theorem OAI.Erdos3.normalizedWeightHistogram_integral line 131
  16. theorem OAI.Erdos3.normalizedWeightHistogram_on_cell line 137
  17. theorem OAI.Erdos3.normalizedWeightHistogram_nonneg line 147
  18. theorem OAI.Erdos3.normalizedWeightHistogram_l1 line 153