OAI/Combinatorics/Progressions/Probability/MixedDensityInterpolation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.mixedCoefficientDensity line 12
  2. def OAI.Erdos3.mixedCoefficientLaw line 16
  3. theorem OAI.Erdos3.mixedCoefficientLaw_probability line 21
  4. theorem OAI.Erdos3.mixedCoefficientDensity_nonneg line 29
  5. theorem OAI.Erdos3.mixedCoefficientDensity_integrable line 35
  6. theorem OAI.Erdos3.mixedCoefficientLaw_density line 42
  7. theorem OAI.Erdos3.mixedCoefficientDensity_integral line 58
  8. theorem OAI.Erdos3.mixedCoefficientDensity_support line 70
  9. def OAI.Erdos3.constantCoefficientDensity line 95
  10. theorem OAI.Erdos3.constantCoefficientDensity_support line 100
  11. theorem OAI.Erdos3.constantCoefficientDensity_cap line 110
  12. theorem OAI.Erdos3.constantCoefficientDensity_buffer line 141
  13. def OAI.Erdos3.mixedDensityInterpolation line 170
  14. theorem OAI.Erdos3.mixedDensityInterpolation_grid line 174
  15. theorem OAI.Erdos3.mixedDensityInterpolation_bounds line 182